11 ms·

A Mechanised Cryptographic Proof of the WireGuard VPN Protocol

• brohee 8y ago
  From the INRIA team (https://prosecco.gforge.inria.fr 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.
• henearkr 8y ago
  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 8y ago
  What's the current status of WireGuard? Is it usable? I remember reading that Cloudfare is implementing it on their VPN product.
  • geolgau 8y ago
    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.
  • dispat0r 8y ago
    Yes it's usable but you need to install external packages.
  • ryanlol 8y ago
    Wireguard has been perfectly usable for years now.
  • KenanSulayman 8y ago
    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.
  • getsimon 8y ago
    Windows client (pre-alpha) has just been released too. https://lists.zx2c4.com/pipermail/wireguard/2019-May/004126.html https://lists.zx2c4.com/pipermail/wireguard/2019-May/004126....
    • jszymborski 8y ago
      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.
  • Down_n_Out 8y ago
    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.
    • amirmasoudabdol 8y ago
      Is there any guide that you can recommend to set this up?
      • mayamatrix 8y ago
        https://drexl.me/guides/wireguard-pihole-vpn-setup.html https://drexl.me/guides/wireguard-pihole-vpn-setup.html should get you there.
      • isatty 8y ago
        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.
  • KaiserPro 8y ago
    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.
    • dewey 8y ago
      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/ 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.
      • deleted 8y ago
        [deleted]
      • cyphar 8y ago
        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-enroll https://github.com/cyphar/dotfiles/blob/master/.local/bin/wg...
        • 8y ago
  • cyphar 8y ago
    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/ https://www.wireguard.com/install/ [2]: https://github.com/cyphar/dotfiles/blob/master/.local/bin/wg-enroll https://github.com/cyphar/dotfiles/blob/master/.local/bin/wg...
  • kdtsh 8y ago
    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 8y ago
    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.
  • Hamuko 8y ago
    It's usable, but not audited. Likewise, Cloudflare's BoringTun has also not been audited properly.
• rahimnathwani 8y ago
  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 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 https://github.com/subspacecloud/subspace
  • withzombies 8y ago
    Algo can be used to configure WireGuard also: https://github.com/trailofbits/algo https://github.com/trailofbits/algo It automatically handles server provisioning, creating users, and can also generate QR codes.
• bblipp 8y ago
  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.
  • fuklief 8y ago
    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)
    • bblipp 8y ago
      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 https://cryptoverif.inria.fr [2] EasyCrypt https://www.easycrypt.info/ 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.
      • 8y ago
• blocke 8y ago
  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 8y ago
    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.
    • blocke 8y ago
      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".
  • pferde 8y ago
    See https://news.ycombinator.com/item?id=19765074 https://news.ycombinator.com/item?id=19765074 for a bit more context from author of Wireguard.
  • tptacek 8y ago