First of all congratulations, I do believe that this is good step forwards.
I took a look at the tamarin model, and at least for me it looks pretty much impenetrable (no surprise there). Is it realistic to think that (any?) implementors can use the proven model as the primary reference when implementing the protocol? Especially if you'd strip away the comments, which are not proven to be correct and as such might be misleading?
However, if you actually read the Tamarin manual -- the documentation is really terrific -- I think you'll find that the spthy code quickly comes into focus as something very straight-forward.
So much so, in fact, that I'd really recommend fluency with something like Tamarin as an essential thing for anybody working on crypto things, even if they're not in academia. It should be accessible to folks who describe themselves as "crypto engineers." Next time you find yourself having to work on or analyze a custom crypto protocol, give it a shot.
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.
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.
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).
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.
There are quite a few other tools for protocol verification (ProVerif, Maude-NPA, etc.) and I haven't used all of them myself, but I think Tamarin is particularly easy to read and understand even when starting out. The rules are roughly written in terms of inputs to outputs along with some labels to refer to what happened, and the properties are essentially just plain first-order logic. (Disclaimer: I'm biased, I've worked with Tamarin more than other tools and also contributed some to its codebase.)
Also I think part of the power in using Tamarin is that if it's having trouble proving something automatically, it's easy to jump in and try to prove it manually with a relatively straightforward graphical representation of the trace sets. That also helps you spot any potential interim properties you might need to prove as helper lemmas, etc.
It's gotten some recent popularity for the work on TLS 1.3 as well [0], and with that an effort to improve the materials available for people to pick it up themselves [1, 2]. Some of the things we did to nudge Tamarin's heuristic in the right direction when autoproving the WireGuard model (documented in the .m4 file) are getting baked in to Tamarin soon.
(For what it's worth, you don't actually have to deal with any Haskell unless you're planning on modifying the prover, the protocol models are in their own language.)
I've tested WireGuard against kernel 4.2.8 with success. It should work for the latest of each minor kernel version from 3.10 up to present. (Probably you should not be using 4.2.0 for anything at all, considering the 4.2 branch wasn't even a longterm stable branch and is already quite old and filled with bugs and vulns. But I just tested on 4.2.0 and it worked too with WireGuard.)
Yes, WireGuard uses Noise, plus other things. For more information, there's the WireGuard paper [1].
Thanks for your reply! I will try to build a newer kernel.
jfyi, that is the error the build is failing on: /tmp/WireGuard-0.0.20170706/src/receive.c:225:4: error: too few arguments to function ‘IP6_ECN_set_ce’
IP6_ECN_set_ce(skb, ipv6_hdr(skb));
I didn't want to discredit the WireGuard protocol - it was just something that came to my mind when looking at the primitives. Thanks for your work
Sounds like you're using some Frankenstein kernel. But asking for tech support and posting random errors on hacker news comments is nearly always fruitless. You can write to the mailing list [1], or ask in #wireguard on Freenode. We'll be happy to help you there. Alternatively, if you're in a sensitive environment, you can always write directly to team {at] wireguard ^d0t^ com.
"Just" noise is a bit reductive. I recommend reading the paper/code. There's a lot of thought put into the higher levels of the protocol to make it an excellent VPN protocol, and not just a secure socket.
Regarding building on 4.2.0; you should make sure it's a real 4.2.0 and not your distro's 4.2.0. I was shocked to see how many non-stability, non-security patches are backported by distro kernels. The package could say 4.2.0, but since 4.2 was never an upstream LTS release, it's likely that it's a frankenkernel. Because distro kernels often misrepresent the version, it seems like a real pain to keep DKMS working on them.
I took a look at the tamarin model, and at least for me it looks pretty much impenetrable (no surprise there). Is it realistic to think that (any?) implementors can use the proven model as the primary reference when implementing the protocol? Especially if you'd strip away the comments, which are not proven to be correct and as such might be misleading?