3 ms·

I'm not extremely experienced in formal verification methods, but isn't usually an implementation that's formally verified? I understand that verifying the prot

by shock 9y ago

I'm not extremely experienced in formal verification methods, but isn't usually an implementation that's formally verified? I understand that verifying the protocol is a big deal but if the protocol is not correctly implemented you can't count on any of the promises the protocol makes.

Jtsummers 9y ago
You can do both. I want to describe (at a more abstract level) a protocol (this allows anyone to implement a specific instance of it in their language or platform of choice). For that you use a formal specification language (Z Notation, Event-B, TLA+, etc.). These lend themselves to formal analysis (evaluation of the specification via standard logic or temporal logic; modeling of the specification for violations of invariants and constraints). If the protocol specification has been verified, you can then be more confident that an implementation of that protocol specification is correct (in principle) and then set about verifying the implementation via either more formal methods (static analysis tools, SPARK, Eiffel's contracts, Frama-C, etc.) or testing (more likely some degree of both). And if you have a formal specification you may be able to construct a better test set than the ad hoc test set usually constructed by developers and testers for systems (that is, it'll be constructed systematically and thoroughly; not haphazardly or just by collecting all the previous PR tests together for regression testing). If, for instance, you have a set of invariants for your system and guards for all your actions, you can construct tests which specifically attempt to violate these (or do violate them and see how your system reacts).
wyager 9y ago
If the specification of the protocol isn't verified, it doesn't matter if the implementation of the protocol is verified to match the spec.
- naasking 9y ago
  Or to be more specific: verify that the protocol satisfies the properties you want from it (i.e security, robustness, what-have-you), then verify the implementation correctly implements the protocol.
zx2c4 9y ago
One step is making sure that the crypto isn't bogus. That's what this formal verification is about here. The next step would be writing an implementation in a language that's verifiable -- such as F* [1] -- and then using that to output actually verified binaries. People are indeed working on this kind of thing, to the point where even the primitives are being generated in this way, such as the HACL* and Vale projects [2] [3]. These are in service of making a verified TLS stack. It's nicely modularized and some of this might, at some point in time, be used for a verified WireGuard implementation. Or, alternatively, other unrelated methods for that. These are exciting times in the formal methods space. In any case, this paper is about the first -- and incredibly important -- step of that kind of journey: making sure the crypto constructions WireGuard uses are top notch and actually has the super strong security properties we want it to have. [1] https://www.fstar-lang.org/ https://www.fstar-lang.org/ [2] https://github.com/mitls/hacl-star https://github.com/mitls/hacl-star [3] https://github.com/project-everest/vale https://github.com/project-everest/vale

by shock 9y ago

Jtsummers 9y ago

You can do both. I want to describe (at a more abstract level) a protocol (this allows anyone to implement a specific instance of it in their language or platform of choice). For that you use a formal specification language (Z Notation, Event-B, TLA+, etc.). These lend themselves to formal analysis (evaluation of the specification via standard logic or temporal logic; modeling of the specification for violations of invariants and constraints). If the protocol specification has been verified, you can then be more confident that an implementation of that protocol specification is correct (in principle) and then set about verifying the implementation via either more formal methods (static analysis tools, SPARK, Eiffel's contracts, Frama-C, etc.) or testing (more likely some degree of both). And if you have a formal specification you may be able to construct a better test set than the ad hoc test set usually constructed by developers and testers for systems (that is, it'll be constructed systematically and thoroughly; not haphazardly or just by collecting all the previous PR tests together for regression testing). If, for instance, you have a set of invariants for your system and guards for all your actions, you can construct tests which specifically attempt to violate these (or do violate them and see how your system reacts).

wyager 9y ago

If the specification of the protocol isn't verified, it doesn't matter if the implementation of the protocol is verified to match the spec.

naasking 9y ago
Or to be more specific: verify that the protocol satisfies the properties you want from it (i.e security, robustness, what-have-you), then verify the implementation correctly implements the protocol.

zx2c4 9y ago

One step is making sure that the crypto isn't bogus. That's what this formal verification is about here. The next step would be writing an implementation in a language that's verifiable -- such as F* [1] -- and then using that to output actually verified binaries. People are indeed working on this kind of thing, to the point where even the primitives are being generated in this way, such as the HACL* and Vale projects [2] [3]. These are in service of making a verified TLS stack. It's nicely modularized and some of this might, at some point in time, be used for a verified WireGuard implementation. Or, alternatively, other unrelated methods for that. These are exciting times in the formal methods space. In any case, this paper is about the first -- and incredibly important -- step of that kind of journey: making sure the crypto constructions WireGuard uses are top notch and actually has the super strong security properties we want it to have. [1] https://www.fstar-lang.org/ https://www.fstar-lang.org/ [2] https://github.com/mitls/hacl-star https://github.com/mitls/hacl-star [3] https://github.com/project-everest/vale https://github.com/project-everest/vale