A Mechanised Cryptographic Proof of the WireGuard VPN Protocol | Hacker News Reader

A Mechanised Cryptographic Proof of the WireGuard VPN Protocol

hal.inria.fr

200 pointscolinprince44 comments

WireGuard is awesome once you have it set up, but I find user management a little fiddly due to the need to generate a key pair and assign an IP address for each client.

The last time I set up a WireGuard server, I used this script (with minor modifications) to create the users:

https://github.com/adrianmihalko/wg_config

But, the next time I set up a WireGuard server, I'll use this web-based admin UI, which displays a QR code to easily configure a mobile client:

https://github.com/subspacecloud/subspace

Algo can be used to configure WireGuard also: https://github.com/trailofbits/algo

It automatically handles server provisioning, creating users, and can also generate QR codes.

From the INRIA team (https://prosecco.gforge.inria.fr) that did a lot of work on formal proofs of TLS implementation, leading to a host of CVE, and whose input was very influential on TLS 1.3.

I setup Wireguard and was pleased with the setup. Unfortunately I tried to use it over the next week only to quickly realize I should have kept my OpenVPN install instead.

Outbound port filtering is incredibly common on public and guest wifi networks and I found three use cases in my first week where OpenVPN on 443/tcp would have worked fine. The inability to use Wireguard over TCP and bypass most outbound port filtering by using tcp 443/etal makes it unusable in my daily life. I can understand why TCP isn't performant but my choice isn't performance vs non-performant. It's works somewhat vs GFY.

And yes I've seen the udp over tcp forwarding hacks. They don't work on iOS and some look outright dangerous (hello open proxy).

Hopefully this can be addressed before Wireguard hits 1.0.

Have you tried setting up Wireguard to use a different port?

I use port 4500, which is typically used for ipsec nat traversal, and have found it available/worked on most networks where the default wireguard port was filtered.

I'll give 4500 a whirl to see if it increases the success rate. It's a good idea. However it's not inconceivable to have sites like cafes that only allow 80/tcp and 443/tcp because that was an option in the UI on their wifi router for guest networks.

At this point if I was designing a VPN for client devices I'd have a mode that looked at as close to HTTPS as possible. There is one tool to tunnel over websocket but this was already sucking up too much of my play time. :)

Cisco AnyConnect, while expensive and bloated, works great as it initially connects on 443/tcp and then tries to setup UDP. If UDP fails it just sticks with the TCP connection and "just works".

See https://news.ycombinator.com/item?id=19765074 for a bit more context from author of Wireguard.

Just use something like udptunnel, which is all WireGuard would be doing to get this "feature".

I am one of the authors of the paper. Feel free to ask questions about our work, I'll try to monitor this thread and come back to answer.

The abstract says cryptoverif is a proof assistant, but the cryptoverif page says it's an automatic protocol prover.

Which is it ? (my understanding is that a proof assistant is interactive, like Coq, Agda, etc)

CryptoVerif [1] is called “automatic” because

1) it generates intermediate games automatically during the proof [see footnote1 for a brief explanation of “games”]. This is in contrast to the other major tool that works in the computational model, EasyCrypt [2], where the user has to write down these games manually.

2) it has an automatic mode in which the tool is able to perform certain proof steps on its own, using a built-in proof strategy. For “simple” protocols in “simple” attacker models, it can even finish the entire proof automatically, where “simple” depends on the capabilities of CryptoVerif.

CryptoVerif also has an interactive mode that allows the user to guide the proof. This is necessary for more complex protocols and attacker models like the one we developed for WireGuard. Once you found the necessary proof steps in interactive mode, you put them into your proof/model file. Then, CryptoVerif can re-check the entire proof in one go.

As CryptoVerif only works with protocols, it's not a general proof assistant like for example Coq, and that's why it's sometimes called “protocol prover”.

[1] CryptoVerif https://cryptoverif.inria.fr

[2] EasyCrypt https://www.easycrypt.info/

[footnote1] “Games” are a concept of the proof technique, which is used to prove cryptographic security: security properties are expressed as a game; if the adversary wins the game, the security property would be broken. We prove that the adversary wins the game only with a negligible probability. We do this by transforming the game more and more, until we reach a game where we can easily prove that the adversary cannot win it, or only with a small (negligible) probability.

   “Games” are a ...

I think the terminology of games is a bit misleading. A better term would be program but in a (probabilistic) programming language that specifies interaction by message passing (such as process calculi).

CryptoVerif outputs what might be seen as program transformations:

   P = Q

such that the probability that a polynomially bounded adversary can 'crack' P is only negligibly different from the probability for Q. This can be seen as a probabilistic generalisation of e.g. the program transformations that an optimising compiler does, except that in compilation you need that P and Q have exactly the same (observable) behaviour.

Verifying crypto protocols is essentially the production of a chain

   P1 = P2 = ... = Pn

where P1 is the protocol in question, and Pn is some "obviously secure" protocol (e.g. existence of one-way functions). Note that Pn might be doing something different from P1. What's important is that the probabilities remain 'similar' (this can be made precise). This proves that P1 is as secure as Pn, so we can break the latter if we can break the former.

The reason for the "game" terminology is historical. Von Neumann's theory of economic games [1] preceeds the development of programming languages for interactive behaviour [2] by many decades.

[1] https://en.wikipedia.org/wiki/Theory_of_Games_and_Economic_B...

[2] https://en.wikipedia.org/wiki/Process_calculus

Games is the terminology of cryptographers, that's why we use it in our work; we need it to interface with this community. The reason this term is used in cryptography might be historical, but also, speaking of an adversary that should not be able to win a security game stays intuitive and thus useful for the definition of security properties.

The language of CryptoVerif is a probabilistic process calculus with interaction by message passing.

Your description of CryptoVerif's output and the proof technique is accurate, thanks that you detailed it for fellow readers. I like the comparison to optimising compilers. In our case, we look at the distribution of messages that are observable by the adversary, and prove that these distributions are only distinguishable with negligible probability. The computations done are actually changed such that they would no longer be useful in a real-world protocol. Like, in one proof step we replace the result of an encryption by a randomly generated bitstring. And if the encryption scheme is secure, the adversary is not able to distinguish these two cases.

BTW, has CryptoVerif been proven sound? I.e. has it been shown that the game transformations CryptoVerif produces really only amount to negligible probability transformations?

Yes, there are hand-written (i.e. not mechanised) proofs that the transformations are sound. But there are no proofs about CryptoVerif's actual code.

Have those handwritten proofs been published?

Yes, the proofs have been published at peer-reviewed conferences. Let me look for the exact references tomorrow.

The proofs are in this paper [1], see Section 3 “Game Transformations” and Appendix E.

[1] https://prosecco.gforge.inria.fr/personal/bblanche/publicati...

Thanks.

Interestingly, that paper uses a variant of pi-calculus, i.e. an idealised programming language for message passing, as 'games'.

Props to your team's great work doing useful analysis on an important protocol. I appreciate it. :)

I do have some questions about the assurance CryptoVerif provides. I'm a non-mathematician that does research in high-assurance security that tracks formal verification results. What I've read indicates problems can kick in at places like this:

1. The logic or modelling used isn't proven sound. There's been tons of analysis into things like set theory or HOL Light. Is CryptoVerif using a proven logic?

2. Recent designs favor kernelized models where about every step or transition can be proven consistent or just not mess up to begin with. Does CryptoVerif do this or is there a lot of complexity in it?

3. The solvers might themselves make mistakes. One mitigation was them simply driving the steps in 2 that were easy to check and/or providing a log of work for a trusted checker. Any risks on automated part to worry about?

4. Small, verifiable TCB. HOL Light and Milawa were explicitly designed for this. Does CryptoVerif have a trusted checker? Are the design and implementation of above done in a tiny, easy-to-verify fashion? The EasyCrypt paper's comparisons to CryptoVerif and CertiCrypt made me think it doesn't.

5. Verification activities on the code itself, source and/or binary, from static analysis to property-based testing. Empirical evidence suggests these catch problems proofs sometimes miss, esp due to specification errors. Even CompCert had a few. Any of this on CryptoVerif's building blocks?

The answers to these questions might be helpful to people interested in boosting the assurance of this or other tools in the future. After all, the proofs can only be as strong as the foundations they're built on.

Thanks for your appreciation :) These are excellent questions, let me come back to them tomorrow.

- CryptoVerif uses a probabilistic process calculus adapted to its use case, detailed in [1];

- There is no verified kernel. All algorithms, including an equational prover for simplification of games, are implemented in ~30k to 40k LOC of OCaml. The correctness of CryptoVerif’s game transformations has been proved manually [1]. A formal link between these proofs and the OCaml code is not established;

- During a proof, after each game transformation, CryptoVerif checks a list of invariants. This already allowed to find implementation errors in the past.

- There are regression tests using proofs that have been done before with CryptoVerif, with both proofs that are supposed to succeed and proofs that are supposed to fail.

To conclude, CryptoVerif has no high-assurance guarantees on its code like Coq and others, but is the only tool that is capable to treat complex real-world protocols.

[1] https://prosecco.gforge.inria.fr/personal/bblanche/publicati...

Ok, thanks! Sounds more like the assurance level of running model checkers on protocol code with user-supplied specs. It can catch lots of problems but no guarantees on all inputs/paths.

Note: just append "/en" to the URL to get the English version. Or you can manually click on the small "fr en" switch on the upper left side of the text description.

What's the current status of WireGuard?

Is it usable?

I remember reading that Cloudfare is implementing it on their VPN product.

I've been using it for almost a year without any problems at all. But I have just a simple connection to my home network. No internet routing or anything complicated. Debian server / fedora & android clients.

Yes it's usable but you need to install external packages.

Wireguard has been perfectly usable for years now.

It hasn't been merged into Linux 5.0 (4.20), so it's not available as part of the kernel without installing additional software. That said, there are several user-land implementations of Rust written in Go & Rust, one of which was written by the author of Wireguard and one by Cloudflare.

Windows client (pre-alpha) has just been released too. https://lists.zx2c4.com/pipermail/wireguard/2019-May/004126....

I've been waiting for the Windows client to get finished off before switching to WireGuard.

I've been using SoftEther in the mean time, and man is it flexible. Punches through NATs with wild abandon, doesn't get blocked since it communicates through 443 (if you should so config it), is super portable, and offers solid security and performance as far as I can tell.

I'm using WireGuard in combination with Pi-Hole on a VPS and connecting to it on my mobile phone to have far better ad blocking. Works as a charm. Rock solid.

Is there any guide that you can recommend to set this up?

I have the same setup too, but with my own infrastructure running on my own "LAN" through Wireguard.

I'll think about writing up a guide on doing this.

https://drexl.me/guides/wireguard-pihole-vpn-setup.html should get you there.

it is usable.

For ubuntu/debian there is a package that installs everything. The config is very simple, more simple than openvpn.

For mobile there are "official" clients, that use QR codes for config.

I'm probably not the target audience but I'd say that it's usable but still not very straight forward to set up. Yes it has less options than OpenVPN but with a bunch of tutorials I was usually able to get OpenVPN set it up and have my traffic flow through it in 30 min.

Following tutorials like this https://www.stavros.io/posts/how-to-configure-wireguard/ (which seems like a good one from a fellow HN user) always seems to work that I'm able to connect to the server but my internet doesn't work after running it. Probably something related to the IP tables rules or firewall I assume?

I'm using the official mac client and Ubuntu 18.10 running on a server at OVH.

I have a script that will generate the server config and auto-generate the client configurations for you[1]. In short, the primary thing you need to remember to add is:

    PostUp   = iptables -A FORWARD -i %i -j ACCEPT
    PostUp   = iptables -A FORWARD -o %i -j ACCEPT
    PostUp   = iptables -t nat -A POSTROUTING -o $HOST_NIC -j MASQUERADE
    PostDown = iptables -D FORWARD -i %i -j ACCEPT
    PostDown = iptables -D FORWARD -o %i -j ACCEPT
    PostDown = iptables -t nat -D POSTROUTING -o $HOST_NIC -j MASQUERADE

To your server's .conf file (using wg-quick). HOST_NIC is eth0 or whatever your server gets its internet from. You also need to enable IP forwarding:

    sysctl -w net.ipv4.ip_forward=1

(If you want to use IPv6 too, make sure to add the corresponding ip6tables and net.ipv6.conf.all.forwarding=1 bits.)

[1]: https://github.com/cyphar/dotfiles/blob/master/.local/bin/wg...

That is very slick.

I'm still working on getting ipv6 working correctly configured when I'm on work wifi, which is both ipv4/ipv6. Traffic flows fine on my personal iphone X with wireguard from home.

Our IT has reddit.com blocked and somehow my connection to reddit is being blocked still even though wireguard and 1.1.1.1 are setup on my VPS/wireguard setup.

Something you may want to look into is the client MTU setting.

When I was setting up WireGuard on macOS Mojave it would connect but I wouldn't be able to load pages. Other devices didn't have any issues so the server config was fine. Turns out the autodetected MTU was too large and the packets were getting dropped. A dead giveaway that this is happening is that pages will (mostly) load over HTTP, but get stuck negotiating a secure connection over HTTPS. I'm guessing this is because of the larger packet sizes required to do the handshake.

Try setting to something really low like 100 to see if things start working and adjust from there.

It is possibly the most usable VPN I've used (in terms of resilience -- configuration is pretty easy but could be made more out-of-the-box ready).

Almost every distribution has packages for it[1] and it's just a matter of copying the example wg-quick configurations from the internet. Personally I've written a more complete script[2] that allows you to dynamically add new devices to a server (and generate a QR code for the Android client).

Yes, it's not mainline yet but it appears to be getting quite close and people still use VirtualBox even though its drivers are out-of-tree. Even though Donenfeld hasn't started tagging releases that are CVE-eligible I'm willing to bet that WireGuard is more secure than its alternatives (has anyone even attempted a formal proof of OpenVPN or IPSec?).

There are a few userspace implementations too.

[1]: https://www.wireguard.com/install/ [2]: https://github.com/cyphar/dotfiles/blob/master/.local/bin/wg...

I’m not sure how much the installation and configuration process has changed in the last 6-8 months, but when I set it up as a call-to-home VPN, it was extremely easy to install (it’s in most package managers, although I recall I was trying to run it on Debian Jessie on ARM and I just couldn’t get the prerequisite kernel version installed for some reason I can’t recall - an upgrade to Stretch fixed this). It was a bit fiddly to set up though, mainly because a basic idea of how network admin works (subnets, default routes, ports, firewalls) is assumed. You don’t need to work with interfaces directly anymore though, since WireGuard now has the wg-quick tool. There are also fairly foolproof user guides and walkthroughs now, e.g. for how to set up a basic VPN and forward all traffic to the server to the Internet, which is a use case for users who want WireGuard to be their glorified web proxy (full disclosure: like me).

I use wireguard daily in a somewhat complex setup and it works beautifully for me. I used ipsec before for everything and don't miss it much. It appears to be a lot simpler and setting it up is certainly a lot easier. It has been stable for me since its in use for like half a year or so.

That said i miss being able to use a trusted CA for provisioning. Every new client needs to be setup at the server which is annoying. I would also like to see the possibility to do Ethernet style virtual interfaces instead of raw ip interfaces in order to be able to bridge those. However, ipsec did not allow me to do that either. Allowing non unicast traffic would also be huge benefit for some applications.

I think all or some of this could be done by a different implementation using the same protocol. Maybe something like ipsec's IKE daemon but for wireguard could handle key exchange and dynamic routing allowing dynamic clients and probably fully meshed networks easily.

It's usable, but not audited. Likewise, Cloudflare's BoringTun has also not been audited properly.

Reply on news.ycombinator.com