Live data from Hacker News

Rosenpass – formally verified post-quantum WireGuard

github.com

71–80 of 86 posts

Re: Rosenpass – formally verified post-quantum WireGuard

#71

What is super interesting is that rosenpass logo is a rabbit, a duck, and a sinister looking boy sporting a cap all fighting over the same key .. https://raw.githubusercontent.com/rosenpass/rosenpass/papers...

At least the name doesn't seem to be a reference to one of the aliases used in the movie _Fletch_. Phew

Re: Rosenpass – formally verified post-quantum WireGuard

#72

Mullvad VPN has a PQC key exchange feature, they are even using two algorithms in parallel: McEliece and Kyber. https://github.com/mullvad/mullvadvpn-app/tree/main/talpid-t...

It's important to point out that these programs have two different objectives.

The Mullvad client is designed to connect to a closed-source service, which is run by someone else. It supports a bunch of different plugins, including openvpn and WireGuard. So probably it could adopt rosenpass, at least with its WG plugin.

WireGuard is designed for minimal protocol variability, high assurance implementations, and ultra small code size. It's used by VPN services, but also by end-users creating their own tunnels.

Re: Rosenpass – formally verified post-quantum WireGuard

#73
post #57
post #6

Does formal verification protect against buffer overflows? (it's a serious question)

Maybe not in general, but there is really interesting work happening in the area of verified protocols generating safe C code (memory safe, overflow safe, timing safe, etc). In particular Project Everest has a set of verified primitives underlying higher level protocols like TLS and more recently all Noise variants ( https://eprint.iacr.org/2022/607 ). As WireGuard is based on a Noise construction, it seems reasonabl…

AFAIK Wireguard is just Noise_IK as an IP tunneling protocol.

I’ve seen some draft ideas for Noise patterns using Kyber on a slack I am on, but they’d be different since Kyber is a KEM rather than a Diffie-Hellman type construction. Noise is all built around DH.

You can use Kyber alongside Noise in a hybrid construction. Just mix it in with the PSK or something.

Re: Rosenpass – formally verified post-quantum WireGuard

#74

Mullvad VPN has a PQC key exchange feature, they are even using two algorithms in parallel: McEliece and Kyber. https://github.com/mullvad/mullvadvpn-app/tree/main/talpid-t...

It's important to point out that these programs have two different objectives. The Mullvad client is designed to connect to a closed-source service, which is run by someone else. It supports a bunch of different plugins, including openvpn and WireGuard. So probably it could adopt rosenpass, at least with its WG plugin. WireGuard is designed for minimal protocol variability, high assurance implementations, and ultra s…

True. But they should have just forked either wireguard-go or boringtun to implement this functionality, and give up on the wg driver, the WG author seems like he doesn't care about PQC. Juggling multiple tooling is always a hassle.

It's also not clear how the WG PSK change is coordinated, and whether that entails a brief loss of connectivity - packet loss, latency spike.

Re: Rosenpass – formally verified post-quantum WireGuard

#75

Earlier quoted context omitted.

Rosenpass author here; nope, that is not correct. NIST has elected Kyber as one of the algorithms to standardize and we are using that. As other commenters mentioned (very good info there, thank you all!) the other algorithm we use – Classic McEliece – is one of the oldest algorithms and has been well studied. There is no known efficient attack against it.

Have you seen https://isd.mceliece.org/1347.html ? DJB agrees with you.

DJB says the parameters designed for long term use mceliece6960119 and mceliece6688128 are fine against an attack billions or trillions of times stronger.

Re: Rosenpass – formally verified post-quantum WireGuard

#76

Earlier quoted context omitted.

It's important to point out that these programs have two different objectives. The Mullvad client is designed to connect to a closed-source service, which is run by someone else. It supports a bunch of different plugins, including openvpn and WireGuard. So probably it could adopt rosenpass, at least with its WG plugin. WireGuard is designed for minimal protocol variability, high assurance implementations, and ultra s…

True. But they should have just forked either wireguard-go or boringtun to implement this functionality, and give up on the wg driver, the WG author seems like he doesn't care about PQC. Juggling multiple tooling is always a hassle. It's also not clear how the WG PSK change is coordinated, and whether that entails a brief loss of connectivity - packet loss, latency spike.

They maintain separate peers for Pre-quantum and Post-quantum so that connectivity isn't interrupted. Each Pre-quantum peer is implicitly paired with a corresponding Post-quantum peer. Negotiating the PSK happens over a grpc api they expose at `10.64.0.1:1337`. The spec is public, if you're curious: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t...

If you're a fuddy-dud like me who uses the Vanilla WireGuard config files, I wrote a tool to upgrade your pre-quantum peer to a post-quantum one. https://github.com/d-z-m/pq-adapter-mullvad

Re: Rosenpass – formally verified post-quantum WireGuard

#77
post #76

Earlier quoted context omitted.

True. But they should have just forked either wireguard-go or boringtun to implement this functionality, and give up on the wg driver, the WG author seems like he doesn't care about PQC. Juggling multiple tooling is always a hassle. It's also not clear how the WG PSK change is coordinated, and whether that entails a brief loss of connectivity - packet loss, latency spike.

They maintain separate peers for Pre-quantum and Post-quantum so that connectivity isn't interrupted. Each Pre-quantum peer is implicitly paired with a corresponding Post-quantum peer. Negotiating the PSK happens over a grpc api they expose at `10.64.0.1:1337`. The spec is public, if you're curious: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t... If you're a fuddy-dud like me who uses the Vanilla Wire…

[deleted]

Re: Rosenpass – formally verified post-quantum WireGuard

#78
post #76

Earlier quoted context omitted.

True. But they should have just forked either wireguard-go or boringtun to implement this functionality, and give up on the wg driver, the WG author seems like he doesn't care about PQC. Juggling multiple tooling is always a hassle. It's also not clear how the WG PSK change is coordinated, and whether that entails a brief loss of connectivity - packet loss, latency spike.

They maintain separate peers for Pre-quantum and Post-quantum so that connectivity isn't interrupted. Each Pre-quantum peer is implicitly paired with a corresponding Post-quantum peer. Negotiating the PSK happens over a grpc api they expose at `10.64.0.1:1337`. The spec is public, if you're curious: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t... If you're a fuddy-dud like me who uses the Vanilla Wire…

Nice. But I think you missed an update, Mullvad now also uses Kyber, your tool doesn't appear to.

You also don't need Go: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t...

Re: Rosenpass – formally verified post-quantum WireGuard

#80
post #76

Earlier quoted context omitted.

They maintain separate peers for Pre-quantum and Post-quantum so that connectivity isn't interrupted. Each Pre-quantum peer is implicitly paired with a corresponding Post-quantum peer. Negotiating the PSK happens over a grpc api they expose at `10.64.0.1:1337`. The spec is public, if you're curious: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t... If you're a fuddy-dud like me who uses the Vanilla Wire…

Nice. But I think you missed an update, Mullvad now also uses Kyber, your tool doesn't appear to. You also don't need Go: https://github.com/mullvad/mullvadvpn-app/blob/main/talpid-t...

I'm intentionally not using Kyber, the key xor only happens if you elect to use both.

It works just fine with McEliece only.

> You also don't need Go

You don't need any language in particular. That's the beauty of the .proto spec. Can generate some client(and server) code in whatever language you want(that protoc supports).

Post reply on HN