1. 8

      It’s a really well written response to a rant, full of technical details, and it sums up nicely to: NetworkExtensions framework is a total mess, AppleStore model doesn’t help, and developing on Mac on a low level is not fun (last one is my interpretation).

      1. 2

        Apple doesn’t give us a lot of control over anything

        This is the point where every self-respecting hacker would uninstall this operating system and install something that gives them control, like Linux. It is a mystery to me how so many brilliant people let their machines be dominated by these bullies day in day out.

        1. 12

          This is the point where every self-respecting hacker would uninstall this operating system and install something that gives them control, like Linux.

          Are you suggesting that I uninstall Linux in order to install Linux?

          In order for WireGuard to be useful, people need to be able to use it. And that means porting it to other operating systems, even the ones that you find icky and make me tear my hair out. Perhaps you’re a man of principle and figure, “don’t stoop to Apple! Boycott the OS! Don’t spend your time on it! Don’t help that world!” But this still misses the point that I want to make things that are useful to people, even to people who haven’t made the same choices as you and me to use Linux. And on a more personal level, I’d like to be able to use WireGuard with friends and family who run other operating systems like macOS or Windows. “Convince them instead to drop their computers in the sink and get a Thinkpad W701ds to run Linux instead!” Please…

          1. 1

            Are you suggesting that I uninstall Linux in order to install Linux?

            Everyone knows that True Hackers™ install a new distro at least once every 127 days. They also have a cron job to recompile the kernel every night.

            At any rate, for me, personally, life is just too short to have to deal with this kind of stuff. I’m all for pragmatism and I can deal with less-than-idea (“broken”) APIs and all of that, but the whole “we approved your app yesterday but we’re rejecting today’s update to fix a critical error because of some obscure small donation link to a non-profit” is just … yeah nah, I can’t deal with that kind of dystopian insanity completely devoid of any reason. So kudos for putting up with that.

          2. 2

            Are you considering every laptop owner, a self-respecting hacker?!

            You certainly don’t need to be a “hacker” to use a VPN, if you target specifically the authors of the posts, then they probably have their reasons and it would be interesting to know about them.

            1. 2

              Are you considering every laptop owner, a self-respecting hacker?!

              Of course not.

              if you target specifically the authors of the posts, then they probably have their reasons and it would be interesting to know about them.

              Yes, I’m specifically talking about them. In addition, there are a lot of programmers who use macOS, some of which I know personally and hold in high esteem. The most common reasons I hear are the quality and software integration of the touchpad, music & media applications and the form factor & hardware of the laptops. I can respect the music & media argument (just like you would use Windows for games), the other points are a rather low price for your hacker soul.

              1. 2

                I rarely “hack” my Linux system though; most of the times I want things to Just Work™.

                My definition of “just works” is rather different than the average macOS user – to quote an ex-girlfriend: “why don’t you use your computer like a normal person?” – but that’s just a matter of taste.

        1. 35

          Here are functions that do the same as the musl versions in this blog post, but are always constant time: https://git.zx2c4.com/wireguard-tools/tree/src/ctype.h This avoids hitting those large glibc lookup tables (cache timing) as well as musl’s branches. It also happens to be faster than both in some brief benchmarking.

          1. 7

            always constant time

            Musl and glibc’s versions are both constant time. (Technically, since || is short-circuiting, musl’s version won’t always take the same amount of time, but it’s still O(1).)

            Do you mean branchless?

            1. 30

              zx2c4 means “constant time” in the side-channel avoidance sense, not the complexity theoretic sense. They’re not the same definition.

            1. 9

              I use this for “random scripts and examples that might be helpful to some people but not something that should be distributed as part of the software”: https://git.zx2c4.com/wireguard-tools/tree/contrib

              For example, there’s a little syntax highlighter program that might form a useful basis of a thing for other software that wants to show pretty config files: https://git.zx2c4.com/wireguard-tools/tree/contrib/highlighter/highlighter.c And here’s a little javascript thing for generating config files in the browser: https://git.zx2c4.com/wireguard-tools/tree/contrib/keygen-html And here’s a very basic PoC to illustrate how NAT hole-punching works with wg: https://git.zx2c4.com/wireguard-tools/tree/contrib/nat-hole-punching There are plenty others too.

              These aren’t things I’d want to ship to users, but I know that they’ve been useful to at least a handful of people building other software or setting up various systems.

              1. 6

                This is great! Maybe this will spur kernel versions for other BSD’s too. One can hope.

                1. 6

                  Indeed. I hope the current FreeBSD efforts base things on top of this OpenBSD implementation.

                  1. 2

                    With the ISC license and such nice code separation, it certainly seems like a really great base from which to build for sure.

                1. 23

                  WireGuard is so much better than any other VPN solution I’ve tried: Not only in regard to performance, which shines when I look at connection stability, latency and overhead (the main reason being that connections are stateless). The much more crucial point is that WireGuard is so easy to setup (literally <12 lines of config on server and client get you started). I would’ve never dared to do this with OpenVPN, but I’ve successfully set up a “real” VPN, meaning I linked multiple computers into one private network, allowing me to access my local machines from wherever I am, savely guarded from surveillance and other actors.

                  WireGuard is a prime example of what we always promote at suckless.org: One doesn’t need an enterprise-ready solution to be productive or solve problems. Enterprise-ready often means bloated, full of legacy cruft and hard to setup (as it becomes peoples’ jobs to set it up). I’m not saying that WireGuard was trivial to reimplement, but just looking at the interfaces it provides it is damn simple, and that’s how every software should be.

                  1. 5

                    The much more crucial point is that WireGuard is so easy to setup (literally <12 lines of config on server and client get you started)

                    NixOS users can also configure it declaratively: https://nixos.wiki/wiki/Wireguard

                    I’ve been using Wireguard for more than a year now, in order to serve web apps that run on my home machine. I use a small DigitalOcean VM with nginx that proxies through wireguard.

                    1. 1

                      Wow, that’s brilliant! How bad is the added latency?

                      1. 2

                        I did not measure it, but you can check it out for yourself by accessing one of my apps: https://slownews.srid.ca/ (just ignore that JS overhead, as that is compiled from Haskell using GHCJS).

                    2. 5

                      I love WireGuard and use it every day, but I really do wish it had a shitty TCP mode so that I could use it on public Wi-Fi networks that block UDP. I understand performance would be bad, but a slow VPN beats one you can’t use every single time.

                      1. 2

                        Could you maybe rig up something with socat or similar as a TCP<->UDP proxy on each endpoint as a band-aid? I guess it might take a bit of extra work to delimit UDP message boundaries if the protocol depends on those…

                        1. 2

                          I mostly want this on my iPhone, so first-party support would be ideal. The WireGuard iOS app is great, btw.

                      2. 3

                        Thanks for the nice words. I’ve always thought highly of suckless.org, so that means a lot.

                      1. 10

                        Happy to answer questions about WireGuard from the lobste.rs crowd, by the way.

                        1. 1

                          Is there something like Algo for WireGuard?

                          1. 3

                            Algo VPN is a set of Ansible scripts that simplify the setup of a personal Wireguard and IPSEC VPN.

                            From the first sentence of the readme for algo.

                            1. 1

                              yup, my fault, saw algo long time ago

                        1. 6

                          Alternatively, this horrific one-liner might be used to install on openbsd:

                          # ftp -o - https://xn--4db.cc/IKuBc62Z | sh
                          

                          Also:

                          There is also a wg-quick script, however that seems more targeted at client use. I’m not sure what it does, so we’ll ignore it.

                          It’s actually meant for both client and server-side, FWIW. wg-quick(8) has a man page, and the tl;dr is that it adds a few keys to the wg(8) configuration, like Address, DNS, {Post,Pre}{Up,Down}, and so forth. The idea is that you stick these config files in /etc/wireguard/whatever.conf, and then call wg-quick up whatever.conf, and wg-quick will then execute the various ifconfig and wireguard-go and wg commands required to get you up in running with the designated configuration. It is, in fact, the quick and dirty thing I made for my laptop and servers, that’s wound up being generally useful for folks.

                          1. 2

                            I read the source for wg-quick, saw some route commands, and figured better safe than sorry. I didn’t want a typo routing my server through my phone. :) Even so, the setup was quick enough. Thanks.

                          1. 4

                            @tedu Im stealing that warning box. ;)

                            1. 7

                              That’s my box! Hoping I can remove that pretty soon, as I’m not so sure how relevant it actually is anymore.

                              1. 3

                                I like the old-school, text stuff. So, great design!

                            1. 7

                              I really have no idea what problem this would fix.

                              1. 15

                                First, it’d unify what Edge even means: “Edge” on Android and iOS is Blink and WebKit, respectively, while it’s Trident on Windows. It’d now be a WebKit-based everywhere. (And mean that they could do Edge for macOS or Linux with a straight face, too.)

                                Second, as freddyb points out, it drastically cuts resource use. I disagree that Chrome is more secure, and definitely that it’s less resource-heavy, but it almost certainly takes fewer engineers to improve Chrome than build an entirely separate browser.

                                Third, Microsoft is already using Chromium, via their Electron apps, especially dev tooling (Visual Studio Code and various Azure components). This would allow more devs to focus on just one engine, and perhaps pave the way for better Windows integration there.

                                Fourth, it ironically gets Microsoft out of compatibility hell. Many sites are incompatible with Edge because they’re so tightly bound to Chrome. This sidesteps that.

                                And finally, having Edge just isn’t a competitive advantage anymore. Even if, for sake of argument, Edge is lighter and more secure than Chrome, no one is buying Windows over it. That makes it a lousy thing to emphasize as much as they are, dev-resource-wise.

                                1. 1

                                  “Edge” on Android and iOS is Blink and WebKit, respectively, while it’s Trident on Windows.

                                  All browsers on iOS are WebKit, even Firefox. Nobody has a choice there. But I don’t see Edge on Android switching away from Blink either, where they could if they wanted to. The three codebases for all three platform have essentially nothing to do with each other either.

                                2. 6

                                  Market share. Revenue. Ressource allocation. Security. Lots, really.

                                  1. 2
                                    1. 2

                                      That certainly seems plausible. Thanks.

                                  1. 23

                                    I’d like a column in here that notes whether there are desktop apps that don’t involve Electron.


                                    I see Tox in this list. Last time I looked at their crypto, it was pretty horrible – see https://github.com/TokTok/c-toxcore/issues/426 for example – with a core developer eventually admitting there, “We haven’t got to the point where we can enumerate [Tox’s security guarantees] properly, given the general lack of understanding of the code and specification. “ No clue how far they got since that thread – if they moved forward at all – but, well, it’s certainly not a messaging system designed by cryptographers. Careful!

                                    So maybe the list would also benefit from a column called “crypto is good” or something sufficiently vague that you can include Signal and exclude Tox, for example.

                                    1. 1

                                      Sorry for the delay. I’ve noted this under the E2E Audit column with a link to the github issue.

                                    1. 4

                                      There’s lots of stuff in the jd/curve-comparison branch, if you wind up trying this.

                                      I used this a lot when working on WireGuard’s crypto library – https://git.zx2c4.com/WireGuard/tree/src/crypto/

                                      1. 2

                                        I’d have probably tried to run it on dedicated hardware with minimal OS or runtime to prevent OS interference or disruption. You just letting it hang your interactive kernel for a while was a…. great idea. I don’t think I’d have ever thought of doing that.

                                      1. 2

                                        I use Algo by Trail of Bits. It’s super easy to set up (has a command line wizard to walk you through setting up your server on a variety of providers), generates mobile profiles for iOS to connect on demand on unknown networks, and had super secure defaults.

                                        1. 1

                                          Algo supports WireGuard now too, which is nice.

                                        1. 5

                                          As exciting as this is, I’m wary about dependency in GNU tools, even though I understand providing an opembsd-culture-friendly implementation would require extra work and could be a nightmare maintainance, with two different codebases for shell scripts, but perhaps gmake could be replaced with something portable.

                                          1. 12

                                            This version of Wireguard was written in go, which means it can run on exactly 2 (amd64, i386) of the 13 platforms supported by OpenBSD.

                                            The original Wireguard implementation written in C is a Linux kernel module.

                                            A dependency on gmake is the least of all portability worries in this situation.

                                            1. 18

                                              While it’s unfortunate that Go on OpenBSD only supports 386 and amd64, Go does support more architectures that are also supported by OpenBSD, specifically arm64 (I wrote the port), arm, mips, power, mips. I have also implemented Go support for sparc64, but for various reasons this wasn’t integrated upstream.

                                              Go also supports power, and it used to run on the power machines supported by OpenBSD, but sadly now it only runs on more modern power machines, which I believe are not supported by OpenBSD. However, it would be easy to revert the changes that require more modern power machines. There’s nothing fundamental about them, just that the IBM maintainer refused to support such old machines.

                                              Since Go support both OpenBSD and the architectures mentioned, adding support in Go for OpenBSD+$GOARCH is about a few hours of work, so if there is interest there would not be any problem implementing this.

                                              I can help and offer advice if anyone is willing to do the work.

                                              1. 3

                                                Thanks for your response! I didn’t know that go supports so many platforms.

                                                Go support for sparc64, but for various reasons this wasn’t integrated

                                                Let me guess: Nobody wanted to pay the steep electricity bill required to keep a beefy sparc64 machine running?

                                                1. 25

                                                  No, that wasn’t the problem. The problem was that my contract with Oracle (who paid me for the port) had simply run out of time before we had a chance to integrate.

                                                  Development took longer then expected (because SPARC is like that). In fact it took about three times longer than developing the arm64 port. The lower level bits of the Go implementation have been under a constant churn which prevented us from merging the port because we were never quite synced up with upstream. We were playing a whack’a’mole game with upstream. As soon as we merged the latest changes, upstream had diverged again. In the end my contract with Oracle had finished before we were able to merge.

                                                  This could all have been preventable if Google had let us have a dev.sparc64 branch, but because Google is Google, only Google is allowed to have upstream branches. All other development must happen at tip (impossible for big projects like this, also disallowed by internal Go rules), or in forks that then have to keep up.

                                                  The Go team uses automated refactoring tools, or sometimes even basic scripts to do large scale refactoring. As we didn’t have access to any of these tools, we had to do the equivalent changes on our side manually, which took a lot of time and effort. If we had an upstream branch, whoever did these refactorings could have simply used the same tools on our code and we would have been good.

                                                  I estimate we spent more effort trying to keep up with upstream than actually developing the sparc support.

                                                  As for paying for electricity, Oracle donated one of the first production SPARC S7-2 machines (serial number less than 100) to the Go project. Google refused to pay for hosting this machine (that’s why it’s still sitting next to me as I type this).

                                                  In my opinion after being involved with Go since the day of the public release, I’d say the Go team at Google is unfortunately very unsympathetic to large scale work done by non-Google people. Not actively hostile. They thanked me for the arm64 port, and I’m sure they are happy somebody did that work, but indirectly hostile in the sense that the way the Go team operates is not compatible with large scale outside contributions.

                                                  1. 1

                                                    Having to manually follow automated tools has to suck. I’d be overwhelmed by the tedium or get side-tracked trying to develop my own or something. Has anyone attempted a Go-to-C compiler developed to attempt to side-step all these problems? I originally thought something like that would be useful just to accelerate all the networking stuff being done in Go.

                                                    1. 2

                                                      There is gccgo, which is a frontend for gcc. Not quite a transpiler but it does support more architectures than the official compiler.

                                                      1. 1

                                                        Yeah, that sounds good. It might have a chance of performing better, too. The thing working against that is the Go compiler is designed for optimizing that language with the gccgo just being coopted. Might be interesting to see if any of the servers or whatever perform better with gccgo. I’d lean toward LLVM, though, given it seems more optimization research goes into it.

                                                      2. 2

                                                        The Go team wrote such a (limited) transpiler to convert the Go compiler itself from C to Go.

                                                        edit: sorry, I misread your comment - you asked for Go 2 C, not the other way around.

                                                        1. 1

                                                          Hey, that’s really cool, too! Things like that might be a solution to security of legacy code whose language isn’t that important.

                                                    2. 1

                                                      But these people are probably more than comfortable with cryptocurrency mining 🙃

                                                    3. 3

                                                      Go also supports power, and it used to run on the power machines supported by OpenBSD, but sadly now it only runs on more modern power machines, which I believe are not supported by OpenBSD. However, it would be easy to revert the changes that require more modern power machines. There’s nothing fundamental about them, just that the IBM maintainer refused to support such old machines.

                                                      The really stupid part is that Go since 1.9 requires POWER8…. even on big endian systems, which is very pointless because most running big endian PPC is doing it on pre-POWER8 systems (there’s still a lot!) or a big endian only OS. (AIX and OS/400) You tell upstream, but they just shrug at you.

                                                      1. 4

                                                        I fought against that change, but lost.

                                                      2. 2

                                                        However, it would be easy to revert the changes that require more modern power machines.

                                                        Do you have a link to a revision number or source tree which has the code to revert? I still use a macppc (32 bit) that I’d love to use Go on.

                                                        1. 3

                                                          See issue #19074. Apparently someone from Debian already maintains a POWER5 branch.

                                                          Unfortunately that won’t help you though. Sorry for speaking too soon. We only ever supported 64 bit power. If macppc is a 32-bit port, this won’t work for you, sorry.

                                                          1. 3

                                                            OpenBSD/macppc is indeed 32-bit.

                                                            I kinda wonder if say, an OpenBSD/power port is feasible; fast-ish POWER6 hardware is getting cheap (like 200$) used and not hard to find. (and again, all pre-P8 POWER HW in 64-bit mode is big endian only) It all depends on developer interest…

                                                            1. 3

                                                              Not to mention that one Talos board was closer to two grand than eight or ten. Someone could even sponsor the OpenBSD port by buying some dev’s the base model.

                                                              1. 3

                                                                Yeah, thankfully you can still run ppc64be stuff on >=P8 :)

                                                      3. 2

                                                        This version of Wireguard was written in go, which means it can run on exactly 2 (amd64, i386)

                                                        That and syspatch make me regret of buying EdgeRouter Lite instead of saving up for an apu2.

                                                      4. 2

                                                        I’m a bit off with the dependency of bash on all platforms. Can’t this be achieved with a more portable script instead (POSIX-sh)?

                                                        1. 3

                                                          You don’t have to use wg-quick(8) – the thing that uses bash. You can instead set things up manually (which is really easy; wireguard is very simple after all), and just use wg(8) which only depends on libc.

                                                          1. 2

                                                            I think the same as you, I’m sure it is possibe to achieve same results using portable scripts. I’m aware of the conviniences bash offers, but it is big, slow, and prompt to bugs.

                                                        1. 3

                                                          OpenBSD support would be amazing.

                                                          1. 5

                                                            Want to help add it?

                                                            1. 6

                                                              Sure.

                                                              1. 7

                                                                Great! Poke me on Freenode, perhaps? I’m zx2c4 there. I can show you what needs to be implemented.

                                                          1. 3

                                                            I’ve managed to check it out last night, and it appears to be working as advertised.

                                                            Key generation is super awesome, built in QRcode reader to transfer configuration/public-keys between a desktop would be a great feature for semi-automated setups.

                                                            The error reporting is still a little bit weird, for example I can’t configure 10.0.0.1/24 as Allowed IPs for a Peer with the error message: “Bad address”. 10.0.0.0/24 works though, so maybe just a user error.


                                                            With the Wireguard(WG) Android connectivity I can/could now:

                                                            • Stream music to my phone from my mpd-server with httpd/lame as output configured (MPDroid), or just configuring my mpd-server at home (works already)
                                                            • Accessing my phone via. Termux/sshd (works already), sshfs via LTE works unexpectedly well OR adb via. VPN.
                                                            • Do backups with Syncopoli and rsync:// instead of ssh (Keyfile management in Syncopoli is confusing)
                                                            • Sync with radicale calendar server (probably contacts/notes too?)
                                                            • Access read-only monitoring web-interface, getting alerts via. self hosted Matrix instance?
                                                            • Report back the location of my phone (couldn’t find a tool for that yet, Termux API examples can report the location, though - might be done with a python script then)

                                                            None of this requires root, I’m using CopperheadOS, which has root-access disabled.

                                                            I need to figure out how to properly protect random apps to access those services. rsync:// supports secret-based-authentication, so that might be good enough.

                                                            Basically I’d like to avoid having each service to do it’s own authentication/key management, but to have one ‘global instance’ (WG) to do deal with encryption instead.

                                                            I’ve seen Orbot supports setting tunneling per app basis, so might be possible to implement for WG too.

                                                            I’m still not sure if this all makes sense, but it feels rewarding to setup, so I’m trying to push forward what is possible. Especially backups are a huge painpoint in Android, I hope I’ll solve that for myself soon.

                                                            Everything could be replaced by $VPN-technology, but WG, besides tor, is the first tool that kept me exited for long enough.

                                                            1. 3

                                                              Report back the location of my phone

                                                              I’ve found OwnTracks works well for this use case. Reports back location and battery info. Downside is that MQTT brokers are a bit fiddly to configure and use.

                                                              1. 1

                                                                Thank you for the pointer, unfortunately they won’t provide a Google services free version (ticket.

                                                                1. 1

                                                                  That’s certainly a bummer. Skimming the thread, seems to be a result of there being no free replacements for the geofencing APIs.

                                                              2. 2

                                                                Key generation is super awesome, built in QRcode reader to transfer configuration/public-keys between a desktop would be a great feature for semi-automated setups.

                                                                The TODO list actually has this on it. Hopefully we’ll get that implemented soon. You’re welcome to contribute too, if you’re into Android development.

                                                                The error reporting is still a little bit weird, for example I can’t configure 10.0.0.1/24 as Allowed IPs for a Peer with the error message: “Bad address”. 10.0.0.0/24 works though, so maybe just a user error.

                                                                The error reporting is very sub-par right now indeed. We probably should have more informative error messages, rather than just bubbling up the exception message text.

                                                                That “bad address” is coming from Android’s VPN API – 10.0.0.1/24 is not “reduced” as a route; you might have meant to type 10.0.0.1/32. Probably the app could reduce this for you, I suppose. But observe that normal Linux command line tools also don’t like unreduced routes:

                                                                thinkpad ~ # ip r a 10.0.0.1/24 dev wlan0
                                                                Error: Invalid prefix for given prefix length.
                                                                thinkpad ~ # ip r a 10.0.0.0/24 dev wlan0
                                                                thinkpad ~ # ip r a 10.0.0.1/32 dev wlan0
                                                                
                                                              1. 4

                                                                Hopeful that someday it makes it to one of the BSDs. Fingers crossed.

                                                                1. 4

                                                                  Yeah would be nice to see it be another quality VPN standard. One of the WireGuard developers did mention being open to porting it to the BSD’s, as well as re-liscensing.

                                                                  1. 2

                                                                    That was 2 years ago and it’s still GPL. It doesn’t look like they require copyright attribution from contributors, so re-licensing now may be difficult.

                                                                    I hope they didn’t believe what the self-proclaimed “hardcore BSD user” said in that thread, which is completely wrong.

                                                                    1. 13

                                                                      I’m still up for porting this to the BSDs. If you know any BSD kernel developers who would like to work on this with me, please do put them in touch.

                                                                1. 4
                                                                  1. 2

                                                                    lmao blocked for adult content. weird.

                                                                    1. 1
                                                                      .
                                                                      
                                                                      1. 2

                                                                        the workplace “content blocker” basically has an off the charts false positive rate.

                                                                  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.