Hey, a new episode! We had a fantastic conversation with Jason Donenfeld, creator of our favorite modern VPN protocol: WireGuard! We touched on kernel hacking, formal verification, post-quantum cryptography, developing with disassemblers, and more!

---

This rough transcript has not been edited and may have errors.

Deirdre: Hello! Welcome to Security Cryptography Whatever. I am Deirdre. We are here with David. How are you doing David?

David: I’m doing pretty good.

Deirdre: I liked your talk yesterday. If anyone didn’t see, David’s talk. Were you at Michigan or were you at…Berkeley?

David: Wasn’t anywhere, I was in my house, doing a video call lecture for Zakir’s course, which I don’t know the number of, but— that’s roughly, “here’s how the internet actually works” at Stanford. But all of my slides were branded as Michigan because, many of them were adapted from my PhD defense that I did for Michigan a few years ago.

So despite, currently wearing a Michigan shirt while we’re recording this and despite the block M’s all over the slides actually had nothing to do with the University of Michigan.

Deirdre: That’s why I was confused. I was like, "is Zakir at Michigan? Nah, he’s not at Michigan", but anyway, we also have Thomas, how are you doing Thomas?

Thomas: I live.

Deirdre: Okay, good. Very good. And today our special guest is Jason Donenfeld, creator of WireGuard. Hi, Jason.

Jason: Hey, happy to be here.

Deirdre: Good. Awesome. for those that don’t know WireGuard is the VPN everyone should be using nowadays, if they have a choice, uh, on using a VPN. And not VPN, as a service, but VPN as a protocol, as to be contrasted with things like IPSec.

For cryptography nerds and for… nice protocol aficionados, who appreciate a nice, simple protocol design, WireGuard is a breath of fresh air compared to things like IPSec. So we are big fans of WireGuard here, and it emerged into the, from the ether into the world via Jason’s brain. So we are very excited to have Jason on our podcast.

cause someone else, fan girl besides me right now,

Thomas: I can, I think, um, and Jason, I’m going to wait for you to shoot me down on this, but I think, uh, I think that WireGuard might be one of the more important things ever to happen to internet security. Not because VPN protocols by themselves are that critically important, although they are very important, but because the process that brought WireGuard, you know, kind of into the market, uh, it was so different than the process that brought other VPN protocols before it. In particular IPSec.

Right? So a huge diff— there’s a number of differences between, you know, WireGuard and previous VPN protocols, but, um, a huge difference between IPSec and WireGuard is that WireGuard is kind of one person’s design, um, kind of free from standards committee, you know, interference. you know, you got to learn from what happened with previous protocols.

And come up with something that’s kind of pure and not compromised. I have a very low opinion of internet standards, cryptography and internet standards, you know, kind of security protocols in general. And I think WireGuard is one of the first times in my career I’ve seen, you know, something get this much adoption without having to, you know, get through the filter of, you know, the IETF.

Uh, am I crazy to think that?

Jason: I mean I’m flattered you think it’s so important. I mean, I guess time will tell there, but, uh, certainly the process that’s brought it about is very atypical, in that WireGuard came about just me putting it out and it’s been successful. I mean, a lot of people have made different pieces of VPN software themselves And put out there, but it doesn’t gain adoption.

it’s the crazy thing about WireGuard is it actually worked, um, which I didn’t really even intend to do when I began, uh, I just wanted the thing to exist because I needed it.

Deirdre: and

what did you need it for specifically? Because I love this origin story.

Jason: yeah, I, I guess, uh, a couple things, um, the, kind of the initial impetus as I, I moved to France and, uh, 2020. And, uh, I wanted to be able to use us internet and, um, I was, you know, familiar with OpenVPN and IPSec and spent a long time kind of finding bugs in that.

And I didn’t want to run that. and at the same time I was working on some, some root kit exfiltration software, uh, or I needed a good kind of minimal tunnel to get information out. And I started thinking, well, you know, I can already channel packets through this. Why don’t I just kind of make that into something?

And the, the plan at the time was to run, my American exit point on my parents’ computer back at home, to get US internet. And, uh, if you’re like, well putting on our route kit, my parents’ computer, that’s probably not a good idea. So I started taking out the nasty code and separate. Uh, WireGuard.

and then it just kind of turned into a thing on its own and seemed viable. And, a couple of friends wanted to use it. So I, you know, made a, uh, a git repo, right.

I kept thinking, okay, I finally got it. Now it’s done. And I would squashed down the git history to a single commit called ‘initial scaffolding’.

And so there’s like the one initial scaffolding commit for so long. and then even, even after that, um, I, you know, I was fine sharing it with two, three friends, but I didn’t want to put some crap code out there with bad crypto or anything else. So I really spent a lot of time writing and rewriting and working through every algorithm over and over and over, uh, just kind of a process of iteration.

Every time I went to fix one part B you know, 10 more ideas would spring up for other parts and so the whole thing got written a million times. And then around the same time, Trevor was getting, going with, uh, his Noise project. and, uh, very early on, I had sent Trevor an email. I think I had read his thing on 3DH or something.

and he said, Hey, by the way, I got this new Noise mailing list. and I, at the time, I mean, Noise had really just begun. It was very, very far from what eventually turned into. Um, and so some of the things I was working on with WireGuard then went back into Noise and vice-versa where I wound up actually implementing, uh, nearly every revision of Noise that we did on the mailing list.

Every time there would be a change, we all right, well implementing that. And then I’d play around with the kernel design, see what needed to be changed. And we kind of went in this feedback loop for a long time there.

Deirdre: So, were you trying out, basically every, every permutation that the Noise framework was coming up with to see if kind of, that was the one that you wanted to use for WireGuard or whether you could just do it in WireGuard as an option.

Jason: not, not quite every, uh, every different Noise handshake pattern. I mean, there are a lot of them and they don’t all have the same cryptographic properties and state machine properties. uh, but even the handshake language evolved over time. So when I say implement every revision, I mean, like every time we made a change to what Noise is, I implemented that. As far as the actual handshake, um, it was pretty clear to me what the kernel requirements for that were early on needs to be, you know, one round trip as possible, minimal state.

Uh, I had kind of the basic idea of what things needed to look like in the code. And then it was questioning. All Right. how can I make the crypto work there?

Deirdre: So you were, you were working within some pretty specific constraints from the beginning. One of them was, one) you were trying. It evolved out of a need to exfiltrate data. And you needed a very small payload for the tunnel to run, right? Just the, the software to make it run, which ruled out like all this IPSec stuff, because it’s pretty heavy in terms of communication on the wire, but it’s also like a bunch of code to actually make the thing go.

Is that correct?

Jason: Yeah. Code needed to be small, but that’s also kind of an aspect of just the security of the whole thing is I want to be able to keep the whole code base in my head at once. And, um, it’s something I apply for, you know, writing code that would be used defensively, but also it’s something that matters to me a lot offensively too.

I’m going to be running some spooky code on a weird system. That’s not mine in a strange environment where it’s not supposed to be run, you know, it in some corrupt memory context or whatever. I really want to understand every bit of that code.

Deirdre: Yeah.

Jason: so yeah, keeping things small and, and just, that I could keep it all in my head at once was a, was a big important part, which kind of goes back to what Thomas was saying about, IETF designs, uh, versus kind of me just doing it.

You know IPSec is big and complicated and it does a lot of stuff. And some of the stuff it does, it does very well. It’s tons of different use cases, uh, kind of, you know, everyone got their, a little part of it and it’s extremely useful. but as a result, keeping that all in your head at once is really complicated.

And, you know, maybe you can keep a couple general ideas of RFCs in your mind, but then what about all the implementation details? And, um, you know, maybe eventually you can get a whole implementation in your head, but then how much kind of fades away from what you’re able to think about all at once? It’s

Thomas: It’s like it’s presumably the case that no root kit author has ever embedded IPSec into their, you know, cleanroom IPSec implementation into their root kit.

Jason: Yeah, I don’t think so.

Thomas: Like this— size is one, you know, huge comparison between, you know, WireGuard and IPSec and OpenVPN. for, I guess there have to be people hearing this that aren’t really already read into why WireGuard is so great.

So if you were going to give me like a couple of more reasons, um, a couple more distinctions is a better way to put it between WireGuard and kind of classic IPSec. Like what would be your like top three there?

Jason: Top three. I don’t know about top three, but I can give you just a couple as they occur to me. so, uh, another thing WireGuard focuses on is stealth, uh, and, and, um, kind of a silent state machine where if you’re not sending traffic, it doesn’t Do anything and kind of

Deirdre: on the wire or do anything in like in memory?

or

Jason: doesn’t do anything on it.

Doesn’t do anything on the wire.

Deirdre: okay.

Jason: So.

Deirdre: keep alives or anything like that.

Jason: Yeah, so the keep lives, go awa if there’s not actually traffic to send. and if you send traffic to WireGuard that it doesn’t recognize, it just won’t respond. Um, and so kind of a task to this then is a very stubborn state machine where everything moves around with, uh, with timers. So that attackers can’t really influence much from the outside.

if even if you send legitimate packets, the most you’ll do is crank a timer, but you won’t be able to elicit some immediate response or, or move the whole state ahead by one notch. You’ll just schedule a timer to happen when it’s going to happen. Anyway. So it’s, it’s very stubborn. You, you know, you, you annoy it to do something and it’ll get around to doing it. Maybe if it feels like it but it won’t ever really respond to you.

So I, so these kind of go together as, as being, um, this is kind of like stealthy, uh, small property where it hides on the network. It’s, it’s resilient.

The crypto, uh, as another thing, um, in WireGuard is also, uh, not ancient, has, you know, one set of ciphers with a provably secure construction.

Uh, and that’s kind of, it, it doesn’t have a bunch of options for what to do with those. You can’t configure here, you know, RSA bitesize though. Um,

I suppose somewhat post quantum RSA, you know, gigabyte keys and stuff, but no unfortunately not with WireGuard.

Deirdre: Well, I have questions about post quantum stuff. We’ll save that for later.

Jason: sure. and so I it’s, it’s not configurable the, the, the choices in it are good reasonable choices for. You know, just about every reasonable use case. and if they ever break, uh, you know, it’s the same as if the software has got a bug and then we just change to something different,

Thomas: I think it surprises people. Like if I look at, like, if I look at reactions to WireGuard’s design, you know, from people that are somewhat familiar with VPN protocols, I think that’s a surprising detail of WireGuard, for people. It looks at first, I think to some people like it’s a bug, although it’s a huge feature.

And I think it’s counterintuitive why it’s a feature that WireGuard doesn’t have cipher suites, doesn’t have configuration, doesn’t do negotiation, right? Like, it’s, it’s a single set of primitives. And then people’s reaction to that is generally, well, what happens if one of those primitives break?

And I mean, I guess we all have thoughts on that, right. But there’s like a general kind of train of thought right now, among cryptography engineers, that the path you’re taking of selecting just a couple of primitives and sticking with them, um, and then versioning, the whole protocol is the right path to take.

I wonder how clear that is to have like, to people that aren’t like paying attention to cryptography engineering, um, why that’s a win?

Jason: Yeah, I think in the beginning, the project, uh, this caught a lot of people off guard and struck a lot of people as a red flag, even like, ‘oh my God, no, no cipher, agility. What are we going to do?’

David: I remember, um, at NSS, uh, the security conference, academic security conference in 2017, you were there because you had published WireGuard at that conference. And I remember sitting out like in the lobby or something and hearing a table of people from Cisco, talk about, ‘that WireGuard thing looks pretty cool, but like clearly, no one’s going to use it. There’s no key distribution and you can’t pick your ciphers. It’s just not possible to use.’ Um,

Jason: Yeah, but you know the answer to this question, it’s true that the answer to this question, what are we going to do when the ciphers break is the same as, you know, what are you going to do when there’s a heap overflow or something? it just, it can be dealt with the same way in this day and age. you know, maybe the, the conditions around that were different in the nineties or something ciphers were breaking right and left. No one trusted anything. I don’t know. I think certainly now, you know, Cha-Poly, curve25519, that stuff is fine.

Deirdre: Yeah.

David: I think that, like a VPN situation, you have pretty good control of both end points.

Um, like there’s near not usually just letting random people connect to your VPN.

Deirdre: It’s not TLS

David: Um, it doesn’t have to support every device on the internet and kind of provide a rolling upgrade path in the same way that TLS does. Like, you can just run two versions at once for a little bit, if you need to, or just do a hard cutoff.

Jason: yeah. I mean, this connects with something else you just mentioned, which is all, there’s also No, key distribution in it. which is another one of these weird things where I see this as a big strength of WireGuard, but a lot of more wary people see that as ‘huh. But the other things have key distribution, that’s clearly missing, it’s a problem.’ Uh, but, Indeed, as you said, for the most part, you have control over both ends of, of VPN and VPN context. and by sticking with just basic static keys, uh, the whole configuration gets super simple. The attack surface gets really small and then people are able to put their own thing on top of it.

and so we’ve seen a bunch of different solutions and products and projects and all sorts of things come up where people have their own take on how should WireGuard keys be distributed. but importantly it’s not, you know, you always must use X.509 and you know, let’s put another ASN.1 Parser in the kernel and it’s, it’s just not

Deirdre: No, let’s not,

Jason: Yeah.

Thomas: And there’s like, there’s a kind of, there’s like a kind of humility to that design, right? Like I think, uh, you know, a stumbling block for a lot of other systems is like, you look at the set of features that people are potentially going to want and you feel obligated to implement them all yourself, like to build them into your system.

But like, I think it’s probably safe to say not a lot of people have built interesting new networking systems off of OpenVPN. Right? Like people have done a lot with OpenVPN, but like there aren’t systems built with OpenVPN as like a building block. Um, like this is our new protocol and like the kernel of the protocols OpenVPN.

OpenVPN has opinions about absolutely everything and your system is simple and really orthogonal, is a cool thing about it, right? Like it’s really easy to build things on top of it because you don’t have a key distribution thing built in, right. You just have, you know, a mechanism for keying, both sides of a connection.

And then it’s kind of it’s up to the integrator or to the next level up to kind of come up with those things.

Jason: right. It’s just a building block. Um, and even in the tooling that the WireGuard project provides. You know, for people who are running this on their laptop and just want to have kind of personal situation, there’s a little tool called WG QUIC that, you know, is what kind of most people use, but actually that’s just like a crappy bash script I wrote.

cause it just uses the, the basic things under the hood. And then for people who want more robust things, you know, there’s a API to use it and it can be integrated in that way. but it doesn’t prescribe any of that. And, uh, the, the hope is that people will maybe figure out more interesting designs than traditional PKI for distributing keys.

And you know, we’ve already seen this in the mesh space, seen it a lot in, uh, con containerization. also a lot of systems people have kind of already have an existing channel for distributing keys. Um, some people run WireGuard, and you know, Kubernetes, which already has this massive distribution system for config.

And so adding WireGuard key, to an already existing trusted channel is just a no-brainer. Whereas if you’re trying to do that with IPSec or OpenVPN or something, then you’re adding this additional weird PKI thing on top of that. and what you wind up doing is trying to recreate basically this notion of pre shared keys, but into some PKI that doesn’t really fit well.

David: Could you talk a little bit about how, what you call crypto key routing works in the WireGuard, just because I think. Is really cool. And also like the thing that kind of makes all of this building possible.

Jason: Sure. So, the concepts based on configuration key, that’s called allowed ip’s. Uh, which was maybe not, not named so well, perhaps it should be tunneled IPS, but it’s allowed IPS. And the way this works is on the way out it’s a routing table, and on the way in it’s an ACL. and I mean that like this, um, when you send an outbound packet, WireGuard will look at the destination address of that packet and see, okay, which of the peers, is configured for that destination address. Uh, And if it finds one that matches, uh, using the usual, uh, prefix matching that routing tables use, then it will encrypt that to the peer’s public key, uh, you know, after a handshake and such.

On the way in, when it gets a packet from a peer, uh, it will look at the source address of that packet. and it’ll say, okay, we’re sending a packet to this source address, which peer would I send it to? And if that peer is the same as the peer that actually sent you the packet, then it’s considered to be authentic. So it’s a kind of an ACL / reverse path filter. A nice property, this gives is a, uh, mapping between public keys and wIP addresses. so from the perspective of a network service running on a system, if it comes from the WireGuard interface and from a given IP, and you can know with certainty that it’s an authentic packet and it’s really from that peer. So you don’t need to have any additional complicated stuff in your firewall about keys or any WireGuard specifics, you can just use IP addresses.

In some way um, it’s like the model of, uh rsh. but, you know, that rhost model, but, uh, it actually works, it’s actually cryptographically identified. Now I’m not advocating we go back to using rhost. It’s a terrible idea for other reasons, but for just the basic bonding between pub key and IP address, the crypto key routing concept, winds up being really kind of powerful thing for administrators.

David: And so WG, like QUIC, just kind of sets up a one to one, roughly connection. If I remember correctly, you know, sets the allowed eye

IPs

peas

Jason: Yeah, I mean, WG QUIC, will look at a WireGuard config, um, which contains private key, listen port, a list of peers. Each peer has a public key. A list of allowed IPs an optionally, an endpoint, uh, maybe persistent keep alive, WG QUIC adds on a couple of things to the basic WireGuard thing where you can also throw like an IP address in the config file is that it’ll set the IP address for the interface, which isn’t a WireGuard thing. That’s just normal Linux networking, but it’s convenient. So it’s just throwing the Spanish script.

It will also, uh, add all of the allowed IPs from each of the peers and set those as routes to the interface. Which again, isn’t a WireGuard thing. It’s just a Linux networking thing, but it just automates it. So WG QUIC is just the kind of easy wrapper around Linux admin stuff.

David: Yeah, but I think the, the core insight there is that, like, you can manipulate the L the routing table, as you know, just like on Linux. Like, you don’t have to like, push out a config. It has everything right up and fancy. You could build a system that’s like dynamically editing these things at the same way that like you’re dynamically constructing routes, just like you would on Linux.

Jason: sure. I mean the WG QUIC config files are generally just static, but you could very easily make a whole dynamic system to do this too.

Thomas: So we’re talking a lot about Linux networking. I think like the most important implementation, or at least up till now the most important implementation of WireGuard has been the Linux kernel implementation of it. It runs everywhere, right? Like there isn’t a, is there a mainstream system right now where there isn’t a decent WireGuard implementation?

I mean, I think all the phones, um, you have a really good one on windows now. Um, yeah, there’s one on macOS you’ve got pretty much coverage right now, right?

Jason: yeah.

I mean, I’d say the, um, the one in last place right now is the Mac one, because we still don’t have a kernel implementation

there, but everywhere else we’ve got in the kernel, uh, is a windows kernel implantation came out recently super fast, crazy code writing for NTkernel can talk about that in a bit, if you like, uh, there there’s one for freeBSD for openBSD and then Linux covers Android and it actually, it’s now in the Android 12 kernel, which is really nice.

Thomas: Wait, what? It’s like the it’s stock Android now?

Deirdre: I

Jason: Yeah, so

it’s, it’s, they haven’t built out the userspace component of it. Um, so you still have to be rooted if you want to actually use it. so hopefully that’ll be in the next version, but it’s now in the builds for the kernel. so.

all the phones that are coming out this year will eventually have, you know, user space support that uses the kernel component.

and if you’ve got the WireGuard app and you root your phone, then it’ll opportunistically use the kernel implementation.

Thomas: So I think, like, I think, I think that’s hard to get your head around is that like like the, the, the most, the original WireGuard implementation was Linux kernel and it’s in the mainline kernel now. It’s part of the Linux kernel. Like I think a lot of people are wondering how you pulled that off.

Jason: Um, yeah, I don’t, I don’t know how I pulled that off. Um, I guess, um,

David: Maybe he’s one of the only people besides Linus that understands how to email a git patch around. that’s.

Jason: I, a part of that story that I think is super significant that people don’t really talk about or really care about because it’s slightly mundane, but super important in the success was that, I backed ported WireGuard to every Linux kernel back to 3.10.

Um, so I always developed against mainline, but then I maintained this super crappy compat.h File, which is like, did the worst if-Def hacks to like transform the code, using the preprocessor to run an old kernel. it’s still there and still maintained and as awful as ever. but that, that worked and it allowed people to start using WireGuard long before it was in mainline or even a thought in main line.

and so once that was there, then I could go around to each of the distros and say, Hey, by the way, I’ve got a package for your distro that will allow people to add this with just one line. Uh, so worked on all the distros. And then it was available and people started using it.

Deirdre: incredible.

The like that’s a nontrivial work piece of work.

Jason: Yeah, and kind of, you know, boring, bad work too, just like the compat stuff. I mean, it sucked, but I think it necessary. And, and even for my own usage, you know, I wanted to run it on, uh, you know, a crappy old edge router. Um, which runs 3.10, so, you know, ha ha had to do it.

And then once people were using it and especially once Linux kernel developers themselves were using it, uh, there was, Hey, why are we compiling this out tree? Can we get this in-tree? You know, then it just became naturally like that. At the same time. you know, I gave a few talks at Linux conferences and, you know, talking to folks on the mailing list and, uh, it’s, it’s a community I’ve been part of for a long time and written other parts of the kernel and so forth.

So,

Thomas: What was your other kernel work before?

Jason: Uh, I’m actually the, uh, the author of the siphash implementation in Linux, which is fun.

Thomas: Huh.

Deirdre: There you go.

Jason: I dunno if there’s some like arm, arithmetic routines, I wrote just a bunch of, kind of random things around the tree. I’ve been on, uh, security@kernel.org for a really long time doing security stuff there And I, you know, I’ve kind of been doing both sides of the Linux kernel security game for, for ages. so I, I don’t know, it’s a, it’s a community I’m familiar with and know people in.

Thomas: And like the general path was, you’re kind of open source, out of tree, back to three dot 10 or whatever, you know, kernel package. And then after that, distros, and then after that, kind of talking to, you know, about having it in main line.

What was like the first distro? Did you get P— w were there any distros that were difficult to get this done with? Is there anything interesting there?

Jason: Uh, no, nothing too interesting. First distro was Gentoo cause I’m a Gentoo developer. So I just did it myself. Um, Ubuntu is always, uh, a horrible distribution to work with, just

Deirdre: Why? I used to— before I switched to macOS, I was on Ubuntu for a long time.

Jason: Well, they sort of inherit from Debian, but they’re like not super tuned in to what’s going on and like not really on top of things. And so it was just always, it’s still a pain to like make sure Ubuntu is working well. but I, I don’t know, it’s not too much interesting to say about the distro story, just open source politics as usual.

David: What about on windows? Is that a kernel module or is it actually in the windows kernel? Proper?

Jason: Okay. So that’s a, it’s a kernel driver. So everything in windows, is a kernel driver, even their networking stack is multiple kernel drivers. There’s nds for the devices and there’s TCP IP for the upper layers and there’s net IO that kind of glues it all together. And, uh, NDI proxy to talk to userspace and so forth.

The a— windows was a really crazy limitation. It started out as a port of, uh, the Linux code and then kind of took on a life of its own. and, uh, it has super fast crypto in it and really deep integration with windows. the funny thing about developing for windows is, um, it’s really like an archeology of computing.

There’s just trash upon trash, upon trash. Everyone in different generations has added their own way of doing things to windows and nothing has ever gotten removed for compatibility reasons. And so it’s just like, it’s just like sifting through the dumpster and trying to understand these historic relics, which is on one hand really awful, but on the other hand, really kind of addictive and an interesting, and so I I’ve spent ridiculous amount of hours in IDAPro now, has taken apart their networking stack and, you know, finding weird bugs, but also just figuring out how to make this thing work well and be fast.

And, that WireGuard for windows implementation does a lot of strange undocumented stuff to make it work well. But, um, I’m quite happy with it.

Thomas: What

are the strange

undocumented

Deirdre: Yeah.

Thomas: say more?

Jason: Let’s see, uh, it works around bugs in an old layer called TDI, uh, by just disabling it, moving around it. I don’t know, integrates with the service manager in a weird way where you have services be getting services. it’s using a DNS setting API that’s undocumented.

Thomas: That you literally found in IDApro?

Jason: Yeah, I, I mean, I, I can’t program for windows without IDApro. I like the, you know, uh, every major function of that thing I’m taking apart in IDApro.

I mean, I really, I can’t program without it, this to somewhere these days, even for Linux where I have the source where most changes to WireGuard, I compile and we’ll then look at what’s happened or like after a set of changes. Uh, and that’s just kind of part of my like, compile, run, then disassemble is like the last step. Um, but with windows, that kind of, uh, like obsessive way of coding really gets out of hand because I don’t even have source to look at, to start with. So if I’m calling some function, I want to understand what it’s doing.

Um, you know, uh, what the side-effects are what’s happening in memory. And I can’t just look at the code, like I can with Linux. And so as extremely time consuming, I mean, everything has got to go through Ida and yeah.

Deirdre: I feel like we need more…. I hesitate to call you a cryptographer, but you are a protocol designer. and I mean, you implemented SipHash so you’re, you’re practically a cryptographer. we need more people designing and implementing protocols that are literally decompiling things to make sure that the state machine that they have designed is doing what they intended to do when they implement it.

Because I don’t, I don’t hear other people talking about how they made sure that the thing that they designed is doing what they think it’s supposed to do like you do right now.

Jason: Yeah, I mean, it’s, it’s not just state machines too, but you know, uh, crypto as well. you know, if I, if I write some, uh, some curve code or if I write, you know, ChaCha implementation or something, even the reference implementation in C is gonna make some funky code and compilers are weird. I want to understand what it’s doing and how it works.

So, I mean, even that stuff has gotta be taken apart.

David: Yeah, I think this is more an indictment of like the fact that even C, you don’t know what the hell the compiler’s going to do. Like we just, we don’t have particularly good tooling for writing lowish level stuff that isn’t just, like writing assembly directly and we don’t have good tooling for doing that either.

Deirdre: Oh, and I was going to, you know, say something like, oh, Rust, lets you do things, blah, blah, blah. But even for Rust, people are like extremely excited to have a, um, a key word to inline assembly, to get that to stabilization because they need it. And so yeah, even, even then like the highly typed, like compile time guarantees and memory safety guarantees of like your LLVM backed Rust, people still want to inline their assembly to guarantee that it’ll do what they think it’s supposed to do.

David: Also, I think in a lot of cases where you’d want to look at that you’d end up being in an unsafe block anyway, but maybe I’m just a negative person.

Deirdre: negative

Thomas: like the Linux implementation of WireGuard is written in kernel C. It’s kernel-resident memory, unsafe C code. Tell me why I should trust it. Why shouldn’t that, like, revolt me?

Deirdre: Hm.

Jason: I dunno, it’s kind of scary. I mean, I,

Thomas: Oh, come on.

Deirdre: Oh, I don’t know. I just wrote it.

Jason: yeah, I I mean, it’s worrisome, but, uh, I suppose there are mitigating factors. it’s very carefully written C and there’s not a lot of it. And so it’s something that you can look at and assess and look for bugs, uh, in a sitting or two. it’s not like it’s the task of reading the entire kernel rooting a massive implementation. It’s a small implementation. and so, you know, the, the many eyeballs theory is mostly BS because, you know, if the code is big enough, many eyeballs don’t want to do anything, you know, that it’s just too much work, but uh WireGuard hopefully is interesting enough and small enough that it can be done as a, as a casual project.

Um, but also just the, the attention that’s gone into the code, um, uh, is, is considerable and maybe different than a lot of other C projects where things are added and features are added at an alarming pace. Um,

it’s, it’s also been designed to be implementable in a way that’s, um, secure or, uh, or leads itself to be secure.

there’s, uh, kind of a fixed amount of state so that you don’t have to have a dynamic memory allocation. Um, all the messages are fixed size, so, you don’t have any parsers, you know, no parsers, you’ve got no parser bugs. And so it kind of a bunch of different coding techniques like this lead to a C implementation that isn’t doing anything to scary.

Deirdre: there, there are parsers, but they are, they’re not dynamic. They’re not reading like a, like, "the following message is, you know, N bytes", and then you try to trust it that it’s actually N bytes and you’re not, uh, you know, I’m going to read a bunch of things and try to parse it as a type that, uh, it lied to you about.

It’s like, everything is a fixed size and it either, either fits or it doesn’t fit. And if it doesn’t fit, you throw it away.

Jason: Yeah. that’s right.

So, uh, so a message. So th th the, the parsing action that happens is looking if a message is exactly the size or if it isn’t. Um, and then after that, it’s just dumped into a struct and that’s it.

Deirdre: This leads me to asking about, so what if all of these asymmetric primitives that we built into this thing are broken by say a large, fault-tolerant quantum computer, sometime in the next 10 to 20 years? How can we make the things bigger so that we can fit some of our favorite post quantum primitives into these messages?

Thomas: Rodents of unusual size. I don’t believe they exist.

Jason: Yeah. So PQ WireGuard is topic that comes up a bunch. I mean, first I should mention WireGuard, as it exists has a kind of a post quantum safety hatch in it, where you can mix in, an additional static, pre-shared key.

Deirdre: nice.

Jason: you, in theory, could negotiate normal WireGuard tunnel. And then through that tunnel, do something reliable, like TCP to run, you know, McEliece, where, you’ve got a lot of stuff to transfer, but it doesn’t really matter because you’ve got TCP and it’s authenticated already pre pre quantum, but authenticated already for now. And then once you get the result out of McElisse, you pop it in the pre-shared key slot, and now you have a post quantum forward secrecy.

So that exists now, that’s kind of the current solution. The reason it’s done that way is because I think at this point, no one really knows aside from maybe McEliece and other code-based things, which post quantum primitives are going to be the ones that make it, you know, NIST competition, isn’t really over.

Eh, you know, if, if, if you, if you looked into this, you know, maybe a year or two ago, it’s think, well, this lattice stuff has been around for awhile, but, uh, you know, now, you know, people are starting to look at lattices and, "Hey, are these really the best proposals for them? How are we coming up with the parameters you don’t like?"

And maybe it’ll all be fine. Maybe it won’t, I don’t know, but it’s clearly very early with post quantum primitives for putting that kind of thing in the kernel. So it doesn’t

Deirdre: yeah, yeah. In the kernel, uh, yeah,

Thomas: well,

Jason: but, but at some point you’re

Thomas: wrapping up.

Deirdre: it’s got another like year to go at, like we’re on round three and there’s like three there, three round, three finalists for, uh, key, um, establishment or KEM. Uh, and there’s three finalists for signatures. Signatures has gotten less attention because we, you know, we care more about the long-term key establishment.

There’s also like, runners up, and my favorites are in the runners up. So the SIKE, uh, isogenies stuff is in the runners up, but yeah, they’re almost done.

Thomas: So the three finalists right now, are they all lattice?

No one of will be McEliece right.

Deirdre: No, I don’t think McEliece is a, is a finalist. Let me check. Oh, sorry. Uh, there’s four. Yeah, classic McEliece, CRYSTALS, Kyber, which is lattices, NTRU, which is lattices, and Saber, which I think is also lattices. And then, um, for signatures, CRYSTALS, which is also, which is lattices, Falcon and lattices, and Rainbow is not lattices it’s like codes or polynomials or something.

Thomas: Jason you like, you do cryptography work. Do you have opinions on like, you know, lattice cryptography or, you know, elliptic curve isogenies and stuff like that? Like, what’s your, what’s your take on that? Are you enthusiastic about this?

Jason: I am enthusiastic, but, uh, uh, my feeling now is like, if you gotta design a system, figure out how to use McEliece in it, despite it being expensive. I mean, if you’ve got a design, a PQ system, it seems like McEliece is the conservative choice and the others are really up in the air. but getting back to your original question.

So post quantum WireGuard, what’s the deal? Um, so yeah, if in, you know, 10, 20, 30, 50 years, depending on, you know, who you’re talking to, who needs the budget or whatever, there is quantum computers, um, everything breaks. and now we also need post quantum authentication. that’s online, et cetera. Now we’ve got to redesign things.

And it seems to me that if things continue as they are with the types of designs that have come out, um, the WireGuard design in general is going to need some big adjustments. now it is I think technically possible to kind of shoehorn in a bunch of PQ stuff now into WireGuard’s design. like it does static style Diffie-Hellman, but there’s CSIDH, um, which, you know, can kind of do that.

Deirdre: Uh,

you don’t want to do static-static with CSIDH, but you can use SIKE, which is just a tiny bit larger.

Jason: Okay. Sure. Um, and you know, maybe that’s fine, but then you also probably want to add some elliptic curve stuff on top of it, too. Uh, so you have pre quantum security, um,

and you know, messages start to blow up, but importantly, computational complexity starts to blow up. Uh, and now you’re sending a little UDP packets or a big UDP packets that have no other, no other authenticating information into the kernel that does a lot of computation on them.

Um, and seems like that leads to DoS and all sorts of other ugly things. Um, or maybe you, you get rid of the static-static, uh, but now you’ve got another round trip. So now the state machine blows up.

Thomas: If you were like, if you were talking to somebody who, uh, does not know what the hell you’re talking about, when you say CSIDH and static-static, uh, do you want to demystify.

Deirdre: okay. Um, so SIDH is supersingular isogeny Diffie-Hellman, um, instead of using elliptic curves to do a diffie-Hellman, key, agreement, you do a walk in a graph of, isogeny maps between elliptic curve, uh, classes. So just say elliptic curves. Um, and you’ll start at one curve and you do a, um, a walk in the graph to another curve.

The secret walk is the isogeny. That’s your secret key, and the public curve that you walk to, is your public key. And you’re able to do something with this walking on this curve graph that’s Diffie Hellman-ish. Uh, it’s not really Diffie-Hellman because there are no, uh, groups. This is not abelian, there’s a commutative aspect because of the way the isogeny maps "commute". I’m using air quotes. They "commute".

When this was originally proposed, you could theoretically do a static-s SIDH key establishment. There is, a static adaptive attack against a long-term static SIDH key, so that you could make multiple queries against the static key, and you would get enough bits from that to break it in, you know, if you have a 700 bit field, you would do like 700, uh, key establishments against it, and then you would have broken their static key. SIKE, which is super singular isogeny key establishment is the submission that was proposed to, NIST. And it basically takes psych and it wraps it up in like The, the transform that lets you do… it’s sort of like turning it into an encryption key establishment and it, it turns it from CPA secure to CCA secure and protects against this, uh, active adaptive attack. So you can use it for a static key, and ephemeral, but you can use it for a longterm static key, which you need in current Wireguard, um, and anything else such as Signal protocol.

Uh, it’s just a little bit bigger. I think it went from 300 bytes to 300, some more bytes, uh, for a

Thomas: And this is, and this is all kind of important for Wireguard because like a big difference between Wireguard and other kind of public key, um, you know, secure transports is that, Wireguard is based on, it’s based on Noise, which is in turn, like based on essentially triple Diffie-Hellman, right? So, um, you know, the common architecture of internet, you know, cryptography protocols prior to Noise, was you’d have, you’d do Diffie-Hellman if you wanted forward secrecy, if you wanted every connection to essentially have its own keys, but you’d be doing ephemeral key Diffie-Hellman.

You’d be making up keys— in theory, you’re making up keys on both sides of that connection for every new connection, the keys just, you know, they get thrown away when they’re done. They don’t have any meaning. In triple Diffie-Hellman, what you’re doing is— and then for those protocols, for those old, you know, the old school, you know, secure transport protocols, to kind of break the man in the middle tie there, you would sign, right.

You would do a signed Diffie-Hellman, right?

Deirdre: Yeah.

Thomas: Diffie-Hellman actually just uses nothing but Diffie-Hellman and there’s this, you have like, you have ephemeral keys and then you have, long-term kind of static identity keys. And so you need to be able to do a, you know, a static Diffie-Hellman on both sides to do, to kind of mix in the identity key in that connection.

That’s

Jason: so why are Wireguard actually does four Diffie-Hellman’s in this case to static-static, static-ephemeral, ephemeral-static, ephemeral-ephemeral, but, uh, Yeah. the original 3DH gets a bunch of properties without the static-static in there.

Deirdre: And then the idea being once you’ve done all, you do all of these Diffie-Hellman’s, either the three for signal or the four for, uh, for Wireguard. And you literally like feed them all into your, your key derivation function. And then you can ratchet. If you’re in Signal, you just keep ratcheting your keys forward, every time you send messages back and forth to each other, or not, I don’t think Wireguard does that right.

Jason: Uh, Wireguard will redo the entire handshake every two minutes, more or less. So it just, it just throws it out and starts over.

Deirdre: Ahhh.

Jason: And then there’s, uh, another kind of limited state state machine where it will, um, it’ll kind of juggle between three different, uh, states: uh, current session, next session, previous session, and will rotate those according to some rules. so you don’t have to allocate and such. Uh, but anyway, I was going somewhere with the post quantum thing, which is, um, you know, one design is you

Thomas: It’s our job to keep you from getting there.

Jason: you can just kind of go, uh, PQ, primitive shopping, and, you know, find the ones that fit in a 1500 byte or 1280 byte UDP packet and see what you can pack in there, and, you know, come up with something for the, for the first message: either you give up on the static-static thing and introduce, uh, you know, uh, a half round trip, a trip, I guess, or, or you, you throw it in there and, Um, you know, hope it’s secure.

but, uh, and you know, there have been papers to this effect. Um, it’s a, legitimate academic exercise to go through and find out what primitives and parameters and whatnot will make this work. And he looked through the wildcard paper and you see the security properties it’s got, and then you try and match them all up with the thing you’re proposing, and, you know, it’s a successful paper, fine, but, uh, I think it, it it’s ultimately too expensive and too prone to DoS. And the whole thing with Wireguard is it gets away now being so light because there there’s just not that much crypto. C urve25519 is small and cheap and well understood. And so we can be kind of very loose with this one round trip handshake.

So I think new designs that incorporate post quantum crypto, are in some ways it’s going to have to give up on one round trip, um, which is unfortunate, but also, uh, Th there are some security drawbacks to one round trip: uh, with one round trip, you get identity hiding, but you don’t get forward secrecy for identity hiding, for example. and so the Noise patterns that do more than one round trip, wind up needing to store state on both sides, um, which, which doesn’t really fit well with Wireguard. Yeah. But, um, what I think it would be possible for future protocols, maybe, you know, future revisions of Wireguard, et cetera, is, uh, to go back to the old cookie idea where the sides aren’t storing state, they pass the state back and forth either, uh, with like a hash seed or encrypted with some, uh, you know, locally cached key to keep around for certain amount of time.

And so you don’t need a state machine on both side with a bunch of memory, um, You can, uh, you can just kind of read, derive things. And then it’s the question of how do you organize the protocol, so that re deriving things, um, from, you know, a little bit of information by the time you’re at, you know, message 4, or 3 or something it’s, it’s cheap.

and you know, it’s a little complicated, but I think it’s also been done before and isn’t impossible.

Uh, and I think that kind of

Deirdre: TLS, right? Like 1.— Is it 1.3 where you can encrypt this— this is zero RTT? You’re encrypting a bunch of this stuff. I forget. Maybe David knows

it’s not a cookie, but it’s state.

Jason: Yeah. So

so, the zero RTT, um, uh, you know, has similar issues with, forward secrecy on the authenticator. but yeah, you, you have a little stored piece of information that you, you send and, uh, the other side can hang on to something to decrypt that and then resume a session.

Deirdre: Um,

What would you say to, the, isogeny stuff has very small keys, so we would fit in the zero in the one round trip, the copy, the computational complexity of doing the key establishment with that is larger. And putting that in the kernel might be a little bit more than people want to do.

Jason: Yeah, so I mean, you could do it right. And people have made these proposals and it’s probably not too hard to implement. If, you know, you can come up with a decent implementation of the actual primitive, which is hard in itself with these things. Um, but still you’ve got this DoS issue. And I I mean, Wireguard already has this DoS issue with 25519, but it works around it with, um, these two cookies as the messages, these two max ads on,

um, where, uh, Yeah, basically, you have to prove that you know, who you’re sending a packet to.

and, uh, if the other side is under load, uh, it’ll then ask for another round trip, basically in a stateless way. Um, so that you prove that you control an IP address and then you can token bucket rate, limit that IP address.

Deirdre: we can keep that

Jason: and yeah.

Deirdre: quantum,

Jason: yeah. And so, you know, that that could also work for, for doing new stuff.

That’s a little more expensive, but also in practice it’s hard. um,

because even if you’re right limiting, you’re still processing a lot of those messages and that still uses some amount of CPU and with Curve25519, it’s, you know, a lot, but it’s not too much, hopefully, depending on the hardware, but

Deirdre: a lot more than that.

Jason: yeah, so it gets hard.

Deirdre: Yeah.

Jason: uh, and, and it seems like if you were to go back to the drawing board anyway, maybe we want some additional properties that you don’t get with one round trip.

Deirdre: Um,

Jason: next challenge is how can we add more roundtrips while keeping the state machine just as small? Um, and you know, there’s the other aspect of the timers around that state machine and re transmits and so forth.

You don’t want to wind up with something crazy, like DTLS, but it seems possible, but there’s work to be done there. and anyway, I think that’s probably what the future will, will have in store for the post quantum stuff.

Thomas: What do you think the future has in store for, uh, for an RFC or a standard for Wireguard? And what’s your take, what do you want the future to be there?

Jason: Yeah. I’ve started writing an RFC a couple of times. I’ve got some drafts of it around. I think, I think I could probably send it up and get the informational one published and some people would say, wow, now, you know, Wireguard is RFC, you know, 1, 2, 3, 4, 5, 6, and now it’s super legitimate or something, even though it’s just informational, as, you know, it gets that number and then people think it’s important. BUt also I, I’m not sure how, uh, how productive it would actually be in the end, what that would actually give.

Another aspect to a Wireguard as a, as a project that uh, it gets overlooked is it’s not just about the protocol. It’s also about how the implementations work. and that’s not to say that like, oh, you’re specifying implementation behavior.

That’s like the wrong thing to do. I, I actually mean it in an even more detailed way, that it’s not just implementation behavior, but implementation technique I think is important. Um, where it’s not enough just to have, you know, a certain domain range of an algorithm. I actually want the way it’s implemented to be a really solid, you know, down to how the memory allocation works and so forth. And so as a, as a project, I’ve tried really hard to, to have high quality implementations that live up to that.

To that extent, I also worry that publishing an RFC might send the wrong message where, oh, it sends the right bits on the wire. It’s done. It’s good enough for Wireguard, but really it’s, that’s not good enough. Um, uh, which, you know, a lot of IETF folks will disagree with, a lot of, you know, very legitimate internet people will disagree with. But, I think when it comes to making a secure protocol to implementation stuff is really just as important as how the protocol itself works.

Deirdre: Mm. And like the design of the protocol being small enough lends itself, easier to a better and tighter implementation, but you’re right. That it’s sort of like you hand over the specification and you, you don’t know what people will do with it. Like it might be compatible, but it might not be anywhere near what, you and your collaborators have produced in your own code in the like official Wireguard repositories.

but it’s, it’s very good because like I remember before, when I, when it came out, I was on the like macOS, so I used the Golang wrapper or whatever, and now there’s the Golang one. There’s Rust. There’s the Android kernel stuff. There’s the freeBSD stuff. There’s like it, the windows stuff. Now, like you basically have something officially, Wireguard, compat / approved for almost every platform.

And they’re all very good. That’s amazing because not every project has like the resources and the capability and the, the energy to actually be like, "yup. And I’ve looked at all of these and they are up to snuff", rather than be like, "here’s the spec. Someone go, please implement it. Like, I just need an implementation that is compatible. Like I’m s— I’m desperate."

Jason: yeah, I mean, I I’d say that’s, that’s a good summary. I mean, th there are a lot of protocol documents out there, so, I mean, you can read it and learn about the protocol. It’s not like, uh, you know, you use this phrase, like hand over the protocol, but like, you know, it’s out there, there’s no secrets or obfuscation or anything like that, it’s there.

But I I’m, I’m just, I don’t want to kind of encourage, like, the way that part of the internet thinks about things, you know, by, by going to the RFC route. I, I still might do it. but I, I’m just, I’m not, I’m not super, uh, I don’t know. I’m not super enthusiastic about it right now anyway.

Deirdre: Ooh. Um, support or integration of hardware or enclave backed keys? That would be neat. Like you would have your long-term Wireguard, key pair backed by like secure enclave on your, you know, your Android or your iPhone or your, you know, secure element on your Macbook or something.

Jason: Yeah. that’d be cool. Um, you know, on iOS and, on Mac OS, the storage for the private keys are in the key chain, which then uses some hardware backed stuff, but of course the computations are happening on the CPU. So, uh, you can look at that way. Um, so putting it down in some hardware would be nice.

It’s always a little tricky to do with, uh, Diffie-Hellman stuff. It’s not like a signature where, you know, you don’t have to worry about, uh, how many things it signs and what it signs for leaking keys. with, with Diffie-Hellman stuff that’s, you know, possibly a little more complicated where, uh, if you’re just doing Diffie-Hellman on another device and you, you know, give it stuff to multiply, can you trick it, extract the key, all that.

Uh, so these are a little more complicated there. So I think, uh, to that extent, people have looked at doing, uh, the whole Wireguard handshake on dedicated chips. Uh, I don’t know, a few different projects, um, all currently private and commercial that are trying to make ASICs and custom hardware to do that kind of thing. And I hope those succeed, it’d be cool to see.

Deirdre: yeah.

David: Do people use Wireguard or do you have an opinion on using Wireguard as just a transport and not a full, like a layer— I guess this would be layer five transport rather than like a full layer, three VPN?

Thomas: Would you find a way to use Wireguard instead of TLS? Why do you think that? Do you think there’s enough of a win to, uh, you know, there, there are things people don’t like about TLS, although maybe less so with 1.3, like if you had to pick between 1.3 and Wireguard?

Jason: Well the comparison there, it doesn’t really fit because TLS running over TCP, which gives you a reliable stream and Wireguard doesn’t. So then it depends on use case, but maybe between like DTLS and Wireguard, would be the better comparison. but, um,

Thomas: we could run, like you could run a QUIC over it or something.

Jason: Yeah, I, I guess, um, so, what I had hoped would happen was that the Nosie pipe stuff would take off to replace a lot of TLS use cases where you could, you know, pick some Noise handshake, not necessarily I K the one that, uh, Wireguard uses, but X K you have additional, packet and you got some other security guarantees out of that.

and that would be a neat TLS replacement. It’s just a kind of straight forward thing you can run over TCP. But Wireguard itself indeed does work fine, for doing, I guess, in this case, uh, layer four stuff or layer five stuff. I was talking, uh, online with, uh, someone building a Wireguard pipe the other day.

Um, we’re looking at ways where to kind of work around the, the crypto key routing stuff. So you really only have to set a couple bytes and then you don’t need a full IP header. Um, so it is possible that I think works well. Um, but for most use cases where you want reliable stuff, if something like Noise pipe probably works better.

You mentioned QUIC, which is interesting. uh, what I would expect to happen in the next couple of years with QUIC in general in this space is start to see QUIC-based VPNs. uh, you know, there are tons of TLS based VPNs. QUIC gives you way more possibilities with those, um, because it’s UDP. So you don’t have, uh, the had a lot of blocking stuff and, uh, you don’t have to use DTLs, you know, QUIC kind of has it all. But also a running QUIC inside a Wireguard seems superfluous and QUIC already has a bunch of crypto bolted onto it. so as far as mixing the worlds that I don’t know about that,

Deirdre: All right. What’s next for Wireguard?

Jason: oh boy,

I don’t know. Uh,

Deirdre: up.

Jason: let’s see. Hopefully it will be getting the freeBSD implementation actually merged through their kernel. It’s still out of tree. Um,

so yeah, and there’s a little bit of work on their crypto API going on there. I hope in the next year to finally put some attention onto the Wireguard Rust implementation.

Um, we’ve kind of had one sit in the repos for a while, but it needs to be reviewed, cleaned up a bit. And then I think, you know, we’ll be able to send the announcement, email, Hey, this is ready, build things out of it.

Deirdre: Mmm

Jason: in the last months I’ve been putting tons of energy into the Windows stuff and that I expect to continue for a few months still to kind of get that fully ironed out and done. You know, that software is trying to be like a real system component of Windows. So it seems like it came with the OS, is what a striving to do, um, and that winds up being way more time consuming than any of the other platforms for the reasons we discussed, so that’ll be going on for a bit.

Deirdre: As an Android user, I look forward to the kernel level Wireguard to be exposed from— I’ve been using the Wireguard on the Android user space app for a long time. So, uh, I love that, but if it’s, if it’s kernel level exposed, that’ll be even nicer.

Jason: Yeah. So, so that’s another thing, uh, hopefully it’ll be coming up is, uh, working with the Google folks to write their user space for that, but also, um, uh, for Chromebooks. Um, think we’re going to be adding Wireguard there And so there’s some interesting, uh, tooling and, uh, plumbing that’s going to hook that up and expose that in the UI.

So hopefully there’ll be some things about that coming out in the next, uh, next few months.

Deirdre: Are you aware of Fuchsia OS?

Jason: yeah, I mean, I know about fuchsia,

but, uh, you’re

David: It’s not a podcast episode, unless Deirdre mentions Fuchsia.

Deirdre: Hey, Hey, I’ve already mentioned the isogenies. We’ve got Wireguard in Rust, we should just throw it at the Fuchsia folks and just make it part of their— well, they have a, they have a microkernel that’s not in Rust, but everything else is in Rust.

Jason: that would be a cool idea. I remember talking to them a long time ago about using something Wireguard alike for what were they talking to me about? Like their Bluetooth stack or I dunno, some kind of crazy IPC, something crazy, and it didn’t seem to fit, but it was on their radar. So,

yeah, I, I think, uh, I think that could be something neat.

Deirdre: I know, I know a little birdie or two, and I can just be like, "Hey. Hey. You should just put this in your tree. Go. Yeah, it’s ready to go."

David: once the Rust implementations in a good spot, we’ll print it off and then physically mail it to Fuchsia people.

Jason: you know, you know, that’s what I did with the Wireguard paper originally?

Is I physically mailed it. so I, I wrote that paper and I didn’t really have any thing to do with academia at all, And like, you know, where do I send it? Who’s going to look at It? Who will break it? So I, I printed out a copy and I physically mailed it to DJB

Deirdre: nice.

Jason: he, he didn’t respond to it, but I figured like, if there’s any chance, like of, you know, find

Deirdre: protocol using almost all of your crypto primitive. Like, tell me, tell me where it is broken. If anything.

Jason: Yeah.

Deirdre: he ever hear back?

Jason: No. And then, you know, years later, finally, I met him at a conference. He was like, "oh yeah, you sent me there in the mail and it’s on my desk somewhere."

Oops.

Deirdre: amongst all the

Thomas: Like, I think like, and not recently, but like maybe a couple of years ago, some of the flack that Wireguard got was from people that were really big into formal verification.

Um, and like there, there was a, there’s a notion that like, you know, any new, like major protocol, like major secure transport, we do should be designed with formal methods.

Um, and you know, should be directly provable in some, you know, model that we already have. how compelling do you find that argument? I know you’ve done some stuff with formal analysis for Wireguard.

Jason: I mean, I think it’s a compelling argument. It was used in context to say like, NDSS never should have accepted the Wireguard paper because it didn’t come with a formal security proof. And,

you know, that seems unreasonable because, um, because for, you know, the most concrete reason, at NDSS, I met a guy, Kevin Milner, who is working with Cas Kramers at Oxford. And he was like, "Hey, that looks cool. If you ever heard of formal verification, have you ever used Tamarin?" Um, I said, I have never used Tamarin. And then we sat down at the conference and he showed me to use Tamarin. And then a few months later I was hanging out with him up at Oxford and, you know, banging out the first proofs of Wireguard.

Deirdre: There you go.

Jason: had it, not gone to NDSS and the first place that never would have happened.

Um, and, uh, since then formal verification now it’s just become part of my general flow of doing things with the protocols, but it’s, I think it’s an important tool without a doubt. and I, and I guess, that variety of stuff, automated solvers also has been useful for me for just hacking things, I wound up using SAT solvers, for, you know, doing little implementation proofs for crypto things like if I’m, uh, writing some funky C code to like change the base of some limbs. oftentimes I’ll want to prove that, you know, break out the SAT solver, but it’s, you know, equally as useful for hacking stuff. I want to, see how some weird code works or find unusual paths through it. I can load the assembly up in something like ANgler and on a run bool vector from the SMT output of that.

Uh, and so I think in general, these, uh, techniques, you know, symbolically symbolic model for crypto, um, connotation model for crypto sat solving, et cetera, have just become part of a tool set, that’s super useful across the board.

Deirdre: Love it. I want to learn more about that, but I work on a cryptocurrency. So I have enough things to work on

Jason: well, Hey, if anything needs proofs, you know,

Deirdre: yeah, the, yeah. We have a network protocol and we’ve got a bunch of protocols all smushed together. You have to like figure out which one you would like to formally verify. Like where’s the low hanging fruit.

David: I think Bitcoin fixes this.

Deirdre: What?

Jason: when I was doing the state machine for Wireguard, I indeed didn’t know about Tamarin. You know, that didn’t happen ‘til I met Kevin, uh, but I sat down on my floor and taped a bunch of pieces of printer paper together, and then just started drawing, it.

Deirdre: drawing drawing Wireguard, the protocol

Jason: drawing, like drawing the drawing, the state machine.

Yeah. Working it out. And the goal was to convince myself that the state machine was sound and I, that, you

Thomas: you

Jason: not that it wasn’t rigorous— but nah, unfortunately not, that’d be fun to have, but

Thomas: You could have auctioned it off.

Jason: oh God. man.

Deirdre: I mean, that’s not far off from, like, if you were trying to encode the state machine as literal state transitions in types. So for a bunch of stuff in Rust, it’s literally like you cannot represent one of these states, unless you consume the memory of N of one of them, of one state and transform it into another.

That was the only way in this implementation that you’re able to do this. So literally writing it down on paper is like the first step to doing that. And then the next step is to write it as transitions between types and then compiling it and making sure that, that the, the flow actually works as you think it to does.

Jason: And I mean, underlying that process of course, is a bunch of type calculus for why that theory is sound, you know, why that works out using types.

Deirdre: Yeah.

David: All right aside from, uh, paying for and winning an auction of your state machine pieces of paper. Um, how else could people support the development of Wireguard?

Jason: So the project lives on donations, I’m living off of donations. If you go to Wireguard.com/donations, there’s a form you can send money, GitHub sponsors has a little show link, there’s a Patreon. If you, run a company, you want to give a lot of money, we can throw the logo on Wireguard.com/donation.

But that’s, that’s how the project ticks. I mean, it’s tried really hard to kind of make it an independent project, that’s not, financed by some product that would bias it. Um, uh, and you know, isn’t in the pocket of some huge company, I just kind of this independent thing with a mailing list and so forth, but that also means that the funding, is, you know, random just comes from anyone pitching in and from a lot of great companies that, you know, aren’t trying to, you know, be the project, but appreciate the project and want to see it live on doing its thing.

And, uh, so that’s been real helpful.

Deirdre: I just went to check if I was already sponsoring uh Wireguard on GitHub and I am, so full disclosure, I’m sponsoring, one of Wireguard’s many GitHub

Jason: Oh, thanks. That’s nice of

Deirdre: Awesome, Jason, thank you very much for joining us. This has been wonderful, I’m learning so much from you and I’m, "we’re not worthy. We’re not worthy".

Jason: Thanks for having me on the show.

Thomas: I would have talked more and annoyed Jason more, but there’s a rock saw going on my backyard right behind us.

Deirdre: This is cool. I need to go learn Tamarin and

David: Me too.

Thomas: Just take a second real QUIC, sell us Tamarin. Like you, you make it sound very cool and very easy to pick up and I’ve never even considered it. So

sell me a tamarind.

Deirdre: it sounds like a, a mountain to climb

Jason: tamarins cool. so, tamarin is like Proverif, uh, Better. Way better. uh, so if you use Proverif, it’s like the same thing. If you haven’t, the deal is this, um, they’ve got a domain specific language where you write, uh, each message, and who its’ transmitted to and how it’s computed. and if you use a hash function, you have just a generic thing called a hash function.

You’re not specifying that it’s, you know, Blake or SHA or something. so you, so you can kind of write down the flow of the protocol, generically, which means it’s a symbolic proof and not a computational one because you’re not looking at, uh, you know, what are the exact limits on the number of messages and that kind of thing.

Um, once you’ve written down a description, uh, then you can, You can write down what you want it to prove that, if you, you know, send these messages and these messages, this next message, uh, won’t be readable except by, you know, this other principal. and, uh, it has a little bit of, of temporal logic built in as well.

So you can order things based on a time, one and a time, two. Um, and so it’s, it’s kind of very expressive language. You can write down the whole, flow the protocol and then all these different things that you want to prove. and then you tell it to prove it. And, um, it will use tons of Ram and CPU and it probably won’t succeed.

it might, it, which is cool when it happens, but it probably won’t. Um, and at that point, in say, Proverif, you can, you know you can choose different things. You can, give it some more CPU and memory and have it run longer and hope that it will work then, or you can write some helper lemmas where you say, uh, well, you know, actually, if you look at this hash chain this way, it reduces to this. So just assume that it’s clear and then maybe that’ll help out the prover.

Or with Tamarin and the really cool thing that makes it great is it has a web interface where you can then click through the different, like paths that a proof can take.

Deirdre: yes.

Jason: And it’ll show with like GraphViz output of like, okay, here are the assumptions we can make and then move on to the next step.

And so you can kind of click through these and see visually where it’s going in the proof and so,

Deirdre: so you can catch, like, it should not be able to go in this direction, but the way that I have written it down says that it can go in this direction. You’re like, "that’s bad."

Jason: Yeah.

So you can say, go in this one instead and like visit that area. So you can say, all right, go here and now try and try and prove it again automatically. And so usually you, you run, it gets to where it is. You click a few times and then it’ll finish it off. Um, and then you can, encode what you’ve just clicked into helper lemmas and such, uh, or uh, Kevin wound up fixing a lot of the internal logic of, of Tamarin, it’s a big Haskell program, so that it would better choose things for Wireguard’s proof, was nice. this interactive aspect is very cool.

it, the interactive aspect. Makes the whole thing fast enough that I can use it as a real tool in development, because it’s not like I write up the protocol and then I got to wait like three days for it to finish or something.

I can write it off, like click through it a little bit and see if thing I just wrote up is stupid or if it works. Um, and you think, you know, when you’re doing crypto yeah. Like you just shouldn’t be stupid period. But actually when you’ve got a prover, you can just write down, whatever occurs to you and see if it’s solid.

Um, kind of a guess and check, which is a very nice way to develop things.

Deirdre: So once you write this down in this DSL, and the thing that you wrote down in your DSL is like, good to go. You have to go implement that in the real thing that you want to deploy. And how do you like check for divergence? Just by eye or what?

Jason: Yeah. So with, with something like Tamarin or, uh, or Proverif Yeah, it’s really two different implementations because you’re writing in this domain specific language. And so if you’re mapping one to another, Yeah.

It’s just, eye, that it’s, it’s the same, but you just hope that it’s the same implementation,

um, which, you know, it’s better than nothing, but you would like to be the same.

There, there are other projects, um, like, uh, HACL* out for example, where they’re able to write implementations of protocols in a language called F* and then prove things about the implementation, but then also lower it down to C.

Deirdre: Yeah. And they’re doing this for TLS or something or pieces of TLS.

Jason: yeah. For, for pieces. And they, and they’ve even done this, uh, other parts of the general project with, uh, primitives. Uh, so not just with protocols, but like with. Is this actually ChaCha, uh, or is this actually Curve25519 and what’s cool with that is like I was saying with protocols where I can mess with it a, little bit and, you know, do silly things to see if it proves, they could make optimizations to their curve code, uh, that are speculative, not super well thought out, but we’ll probably make it faster and then see if it’s actually correct after.

Deirdre: Like As a, in the protocol and Tamarins view of correctness.

Jason: what I’m talking about for, for HACL*. So like if they’re working on a curve implementation like of curve25519, let’s say, and they see, oh actually if we just omit these steps or rearrange these steps or do this a little differently, the code is going to generate as faster. then they can just check immediately, is it also correct? Which is really powerful because most of the time when you’re writing super optimized code for primitives, You spend a lot of time, like carefully scrutinizing your math to see is this op optimization legit. And then, you know, I think the math checks out, hopefully it’s okay.

Deirdre: Yeah. Or like I’m windowing just this much for this field to try and get a speed up and it should be correct. And all my test vectors are passing, but like, you know, maybe it did something weird at an edge case or something.

Yeah.

Jason: Yeah. And you know, when it’s just you in front of your computer, how much are you hand-waving for yourself and how much are you actually being rigorous? And that’s a hard thing to do. So I think these tools are really important where you just, you can develop fast and then it checks you.

So I guess to bring back that back to Wireguard, it would be cool to have something like a HACL* Wireguard implementation, we’d looked at various times at doing that, and I think the code, it generates still isn’t super suitable for the kernel. Uh, but you know, maybe, maybe it’ll get there in time. but the other aspect is that Wireguard’s trying to be simple enough that, you can just, you know, look at both things and see that they line up,

that hopefully the, the manual version is sufficient.

Deirdre: yeah.

Jason: Hopefully.

Deirdre: As opposed to TLS, which, or IPSec, where it’s just like, it’s so complicated that you kind of can’t eyeball it anymore. And so you’re just like, yes. If we have a computer checked proof of the thing that we’re spitting out we are, we’re more confident than that. Whereas if the thing is small enough to be Wireguard, you can just like, look at it and just be like, yeah, we it’s small enough that a human or two can just hold it in their head and grok it as opposed to like the complexity of IPSec or TLS even, even 1.3.

Thomas: Jason, thank you for doing

David: yeah. Thank you.

Deirdre: Um, and we may keep bugging you about post-quantum Wireguard , although like literally you enumerated all the paths forward. So there’s nothing to say for several years

Jason: Well, I dunno if you think of something cool that, or like, if you want to actually pursue a certain path. I mean, I’m, happy to,

I mean, get

Deirdre: The rust Wireguard and just be like, here, this is how you slot in a nice rust implementation of SIKE, and this is what it does. And you can just

say, you know, this is too much or too little or too complex or too DoS-y or,

David: or go back to your cupboard under the stairs. Deirdre

Jason: mean

David: what a nice implementation you get a cookie. Okay. Now

Deirdre: yeah. That’s like, it’s very nice. You can go use it. You, you, you yourself and only you

Jason: well, it’s just the opinions I have on like, should we do PQ now or later. And how should it be done? I mean, they’re opinions, but they’re not like super strong and you might find that in the practice of implementing it, you come up with something pretty cool and good, and worth doing anyway.

Deirdre: Oh yeah. It’s definitely research because it’s basically, there are no obvious options. There’s trade-offs in every axis. So it’s all, it’s all sort of like, okay, let’s, let’s try some stuff and find out where we get burnt, because we’re going to get burnt somewhere. We either have to change the protocol we’re trying to retrofit. We either have to compromise on some of the security levels of some of these primitives, we have to, you know, we either have to accept that these things are going to be slow. It, you know, like there’s, there’s, trade-offs everywhere. So we got to figure it out???

Because we have to figure something out before we ask people to try to adopt it.

Jason: if you’re just trying to slide stuff in, you could probably do SIKE and Kyber, you know,

just do it a hybrid of them.

Deirdre: Yeah.

Yeah. That’s, that’s basically the direction I would go and we’ll figure out signatures later. We, we could do, we can do MACs. We don’t have to worry about signatures, signatures, or like TLS and other stuff. Anyway, I’ll stop talking.

David: we can Chris Peikert on later this month under the guise of it being a discussion about post quantum crypto, but actually he and I will spend the entire time talking about the upcoming Michigan versus Ohio state football

Deirdre: I was going to say that it should be under the guise of Michigan football, and then I will grill him,

David: swap it around. There we go.

Deirdre: about post quantum primitives.

Awesome.

Thomas: Jason, Thank you for doing

David: yeah. Thank you.

Deirdre: All right. Uh, cool.