1. 3

    Here’s my post from the mailing list, on the paper:


    Two researchers – Ben Dowling and Kenny Paterson, who you might know from their work on Signal and TLS 1.3, among other research areas – have written up a by-hand game hopping proof in the computational model of the WireGuard protocol. The paper is worth a read; the findings are very interesting.

    One design goal of WireGuard is to simplify the state machine as much as possible, by keeping the handshake portion of the protocol as only two messages – there (message 1) and back (message 2) – so that if something goes wrong, the state machine can just start over at the beginning again, without having to take into account intermediate states. The original WireGuard paper [1] writes that after the initiator receives message 2 from the responder, the initiator must send the first transport data message to the responder, not the other way around, to act as a handshake confirmation message. By putting the confirmation message as part of the transport layer, it means that any transport message that arrives will suffice as confirmation, as opposed to relying on a special handshake-layer message, which could be dropped (we’re UDP remember), thereby complicating the state machine. This is a fairly nifty trick that allows us to write simpler and more reliable implementations, and it’s specified as part of how the Noise Protocol Framework [2] works.

    It turns out, however, that traditional computational security models, such as the eCK model used in this paper, were designed for a different era of protocols, where the handshake was one thing, and the transport was another, and different handshakes could be put together with different transports, in a nicely stackable fully modular way. Certainly IPsec-era protocols, for example, were interested in this kind of layer-separation – IKE is a good example. These computational security models simply don’t take into account what it means when a transport message is used as an essential part of ensuring the handshake security properties.

    Other protocols have had similar traits – TLS 1.2, for example – and researchers came up with a different security model called ACCE [3], in order to prove (or disprove!) things about them. But generally speaking, the go-to model for researchers interested in trying to do computational proofs is eCK.

    Thus, Dowling and Paterson tried to fit the verbatim protocol into this computational model, and were not able to, due to WireGuard’s reliance on the first transport message as part of its handshake properties (which we consider a feature, not a bug). Fortunately, the authors didn’t stop there. They then went on to modify their description of the WireGuard protocol to put that confirmation message essentially as part of the handshake layer, which would not be feasible for real WireGuard, but is a sufficiently interesting modification to prove things about. Finally, they showed that that modified construction is secure.

    I interpret this as further positive confirmation of WireGuard and the Noise Protocol Framework, as it is easy to argue that their modified WireGuard protocol – which fits into their security model – is “morally equivalent” to the real WireGuard protocol. I also look forward to advancements in the tools and models available to computational proof researchers.

    Enjoy the papers!

    1. 1

      Is this the same HACL X25519 implementation as NSS uses, or are there two distinct implementations on the same formal verification tooling?

      Does it make sense to have a cryptography library (in the style of OpenSSL’s libcrypto) to ease distribution and use of formally verified algorithm implementations?

      1. 2

        Is this the same HACL X25519 implementation as NSS uses, or are there two distinct implementations on the same formal verification tooling?

        NSS and I both used the same project to generate our implementations, but our C code is slightly different, due to kernel constraints. For example, the kernel doesn’t like C99 declarations-after-statements, so a special option must be passed to HACL* to have output that is suitable for C89.

        Does it make sense to have a cryptography library (in the style of OpenSSL’s libcrypto) to ease distribution and use of formally verified algorithm implementations?

        I’m pretty sure this is what HACL* is trying to do, in general. They have a lot of different primitives verified and available. Impressive project.

        1. 2

          They spent who knows what amount of time and money specifying and verifying this stuff down to imperative code. Then, they casually mention this afterward:

          “For convenience, C code for our verified primitives has already been extracted and is available in snapshots/hacl-c. To build the library, you need a modern C compiler.”

          McCoy: “You want me to get trustworthy assembly by running verified C through a modern C compiler? My God, man, I’m not Xavier Leroy!”

          1. 3

            INRIA also makes compcert – http://compcert.inria.fr – which you’ve probably heard about. HACL* appears to have a mode meant for targeting the compcert compiler. So you can do it this way if you’re feeling anxious.

            1. 2

              Oh yeah. I was mostly kidding. Note that CompCert is proprietary software. They currently allow non-commercial usage of it. Depending on one’s circumstances, the verified C might be available but CompCert might not. It’s why I recommend where possible to add verified assembly using free tools like Simpl/C or x86/Proved. The users can pick what level of risk they want when choosing either the C or whatever assembly was included.

      1. 3

        I was already recommending people turn your WireGuard work into a stand-alone library for making tunnels we can run all sorts of other stuff through. Now you’re including verified ECC implementations? That’s awesome! Keep at it!

        1. 4

          I’m actually working on turning that into the kernel’s second generation crypto API. Stay tuned for more on that.

        1. 52

          I am on fastmail for my domain. Works fine, does everything I need.

          1. 7

            I am also a happy fastmail.com customer since about 2 years now. I used mailbox.org before, a german email provider, which is quite cheap (1€ per month) and allowed to use custom email domains but their spam filter sucked. Fastmail’s spam filter is also not perfect, in fact Gmail has still by far the best filtering, but their service is great and I can use custom email domain’s too. They also develop JMAP a JSON based IMAP replacement.

            1. 7

              I’d say the fact that JMAP is JSON based is only marginally-relevant; it’s got several significant design improvements over IMAP - e.g:

              • Folder renames no longer munge mail IDs (usually forces clients to re-download all messages).
              • No persistent connection (IMAP keeps your mobiles radio awake).
              • Flood control (some IMAP commands can send millions of identical lines in response).
              • Saving a draft with an attachment doesn’t make you re-send the attachment.
              • Subscribe to all changes in your mailbox via a single connection (vs one connection per folder)
              1. 1

                It’s more than IMAP replacement too, possibly better described as an alternative to Exchange ActiveSync.

              2. 3

                I’m with mailbox.org myself, with the 2.5EUR/month plan and a private domain. Mostly happy, I don’t have issues with spam. They seem to be quite opinionated on how to handle spam: https://www.heinlein-support.de/vortrag/spam-quarantaene-und-tagging-der-grosse-irrtum. But it seems classical spam tagging has been added recently, though I haven’t tested it: https://mailbox.org/update-des-webportals-bringt-nuetzliche-zusatzfunktionen-fuer-ihr-e-mail-postfach/

                I’m not that happy with the web interface though, it seems to be https://en.wikipedia.org/wiki/Open-Xchange.

                1. 1

                  Is JMAP even supported anywhere? Does anybody use it? Last I checked, not even Fastmail actually used this for anything. Seems like the project started with some energy but is mostly dead now? What a shame, as I’d love to use it somewhere… Please do correct me if I’m wrong.

                  1. 4

                    Hi, I’m some engineering guy at FastMail.

                    JMAP is currently going through the standardisation process at the IETF to become an RFC. Several companies have built or are building client and server implementations based on those drafts. We’re putting a lot of work into JMAP support in Cyrus.

                    At FM, we use it internally for some (but not yet all) of our UI-server interactions, and we’re working on converting the UI to use JMAP natively (once the standardisation work has stablised).

                    Finally, we’re just about to launch a new product that uses JMAP from top to bottom - Cyrus, Ix (a JMAP API generator) and Overture (a UI framework with a JMAP-backed storage layer).

                    So there’s lots happening on JMAP at FastMail and elsewhere.

                    1. 1

                      That’s really wonderful to hear. Once a year I email FastMail tech support asking them if there’s a JMAP thing, but the answer is always something like “no, and we don’t know when if ever.” And then I’m sad. This here is the first positive confirmation I’ve received, and I’m quite happy to hear it!

                      Hopefully once you release a fully JMAP designed system, you’ll have auto-exporters from existing tag-based systems like Gmail? Something like this would probably net you a massive user base.

                2. 7

                  I switched to fastmail last month and I am very happy with it. Before that, I had been self-hosting for 10 years, but I started seeing my emails listed as spam after I switched VPS providers (despite correct SPF etc), and I wasn’t motivated enough to fight for my IP reputation again.

                  1. 5

                    Also Fastmail, moved from Google Apps for domains 2 or 3 years ago. Besides the advantages others mentioned, subdomain addressing is also a cool feature. Some mail providers support plus addressing

                    me+foobarbaz@mydomain.com

                    subdomains addressing is a bit nicer. You can make disposable addresses in the form of:

                    me@foobarbaz.mydomain.com

                    makes it easier to write rules and to drop mail when the address is sold to some spammer.

                    Also their support is pretty good. I had a small feature/refinement request twice, in both cases they had the feature implemented in their beta site in a couple of days.

                    1. 5

                      I went to fastmail two years ago when the server on which I’d hosted my own email for about eight years died. I was happy to give a great company about $60 a year to host my family’s email. I was probably spending $60 a month of my own time just to administer the damn thing.

                      1. 4

                        I’m on Fastmail too, with my own domain, for about ten years. The web UI is focused and fast, and the iOS app is just a webview, but a decent one that’s quick. I use Fastmail aliases and inbox rules to send to multiple external addresses, like a basic private listserve. Tons of advanced features for mail users, DFA, and no advertising or shenanigans with your inbox.

                        They went through a purchase by Opera a while ago, then a few years later Opera sold the business back to the original Fastmail employees – not a single hiccup or business misstep the whole time. They are laser focused. They contribute back to the open source mail server community.

                        The only issue on my wishlist is that they still don’t support the full CardDAV protocol, which means I cannot fully sync my Fastmail addressbook with iOS, Mac, Windows, or *nix apps, but they’re working on it, and it’s due soon (early 2018?).

                        I think it’s cheap for what you get, if you’re into that sort of thing.

                        1. 1

                          What exactly is missing from CardDAV support? I’m happily using it to sync contacts to my iOS/Android devices.

                        2. 2

                          Same here. I use fastmail for every new domain that I need email for and it’s pretty great.

                          1. 1

                            Another vote for fastmail. Been a user for several years now. Has by far the best webui out of any provider. Very stable, and quick restoration of backups if you ever need them.

                            1. 1

                              Another +1 for Fastmail. I’ve used them for 3 years and have been pleased with all their services. Their documentation is clear, the system is not hard to use, and they answer questions promptly.

                              The only thing I’m waiting for is HTTPS support on their web hosting. But if you need serious web hosting, Fastmail probably shouldn’t be yout first choice.

                              1. 1

                                Yep, fastmail here too, it’s superb.

                              1. 5

                                Linux has network namespaces and capabilities, both of which could move the author a bit closer to what he’s after.

                                However, in reality the Linux kernel is probably not something you’d want to rely upon for security between users who can execute code. That’s why folks move toward hypervisors – not that they’re a panacea (hypervisor attacks aren’t uncommon), but they at least have a somewhat smaller TCB.

                                1. 8

                                  Here’s a plug for the thing I’m working on. If you want a VPN in less than 4k lines of code – small enough that you can read and understand it in a single sitting – then you might want to checkout WireGuard. It’s a relatively new project, but considerably less scary than big behemoths like OpenVPN or IPsec.

                                  1. 1

                                    Would I be able to use wireguard with something like Mullvad?

                                    1. 1

                                      Yes. If you Google those two keywords, you’ll find what you’re looking for.

                                      1. 1

                                        \o/

                                  1. 1

                                    Any link to the source?

                                    1. 1

                                      “authored by”, perhaps? (Seems a bit self-promote-y…)

                                      1. 4

                                        Sorry, didn’t mean to be “self-promote-y”. Just thought it was sort of interesting and others might be curious about it, in addition to being a general PSA for anyone using this bit of code.

                                        1. 2

                                          Maybe ‘show’ :-)

                                          Good catch nevertheless!