top | item 19896760

A Mechanised Cryptographic Proof of the WireGuard VPN Protocol

200 points| colinprince | 6 years ago |hal.inria.fr | reply

44 comments

order
[+] rahimnathwani|6 years ago|reply
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

[+] brohee|6 years ago|reply
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.
[+] blocke|6 years ago|reply
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.

[+] stock_toaster|6 years ago|reply
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.

[+] tptacek|6 years ago|reply
Just use something like udptunnel, which is all WireGuard would be doing to get this "feature".
[+] bblipp|6 years ago|reply
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.
[+] nickpsecurity|6 years ago|reply
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.

[+] fuklief|6 years ago|reply
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)

[+] henearkr|6 years ago|reply
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.
[+] Jonnax|6 years ago|reply
What's the current status of WireGuard?

Is it usable?

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

[+] cyphar|6 years ago|reply
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...

[+] kdtsh|6 years ago|reply
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).
[+] mercora|6 years ago|reply
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.

[+] Down_n_Out|6 years ago|reply
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.
[+] KenanSulayman|6 years ago|reply
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.
[+] geolgau|6 years ago|reply
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.
[+] KaiserPro|6 years ago|reply
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.

[+] Hamuko|6 years ago|reply
It's usable, but not audited. Likewise, Cloudflare's BoringTun has also not been audited properly.
[+] dispat0r|6 years ago|reply
Yes it's usable but you need to install external packages.
[+] ryanlol|6 years ago|reply
Wireguard has been perfectly usable for years now.