Rosenpass – formally verified post-quantum WireGuard | Hacker News Reader

Rosenpass – formally verified post-quantum WireGuard

github.com

285 pointslima80 comments

How does this compare to the work done by the Netherlands group (Hulsing/Zimmermann, etc al) [1] and the Kudeldki group from Switzerland (Raynal/Genet/Romailler) [2]? It's nice to see someone making this more available. I had thought about trying to push the pq-wg implementation from Kudelski group to wg or trying it out, but I never had the time. Rust implementation seems to be an improvement of implementation, but I don't know about the underlying proofs.

[1] https://eprint.iacr.org/2020/379.pdf [2] https://csrc.nist.gov/CSRC/media/Presentations/pq-wireguard-... [3] https://github.com/kudelskisecurity/pq-wireguard

We are based on the work of Hülsing, Ning, Zimmermann, Weber and Schwabe and in contact with the group. I havn't heard about kuedlki; the slides seem to refer to a reimplementation of the 2020 paper and the go implementation has been stale for two years. They also seem to use a tweaked krystals implementation which I would not trust. The link to the blog post they refer to dis dead.

The Rosenpass protocol builds on the 2020 paper but also adds security against state disruption attacks (CVE-2021-46873). The implementation is actively maintained, written un Rust not in go. We use Classic McEliece and Kyber from the OQS library.

> We are working on a cryptographic proof of security, but we already provide a symbolic analysis using proverif as part of the software package

How can you prove this? There is still no mathematical proof that i.e discrete log is NP complete

edit - I see it's a WIP but even the definition of secure seems difficult

Rosenpass author here;

There is a confusion about terminology here I think. Mathematical proofs including cryptography proofs use models simplifying reality; i.e. the real practical system might still be susceptible to attacks despite a proof of security.

For crypto primitives (classic mc eliece, curve25519, ed25519, RSA, etc etc) the standard for proofs is currently showing that they are as hard as some well studied mathematical problem. This is done by showing that an attack on the primitive leads to an attack on the underlying mathematical primitive. The proof for Diffie-Hellman shows that attacking DH leads to an efficient solution for the discrete log problem. I.e. the proof is a reduction to the underlying primitive.

No primitive is perfectly secure (at least a brute force – i.e. guessing each possibility is possible); there is some probability that the adversary can guess the right key. We call this probability the adversary's advantage. One task in cryptoanalysis is to find better attacks against primitives with a higher advantage; if an attack with a polynomial time average runtime is found, the primitive is broken. Finding a higher non-polynomial attack is still an interesting result.

The standard for protocols is proving that the protocol is secure assuming the primitives are secure; since multiple primitives are used you basically get a formula deriving an advantage for breaking the entire protocol. The proof is a reduction to a set of primitives.

We did not build a proof in that gold standard, although we are working on it. We built a proof in the symbolic model – known as a symbolic analysis. This uses the perfect cryptography assumption; i.e. we assumed that the advantages for each primitive are zero. Google "Dolev-Yao-Model".

This makes the proof much easier; a proof assistant such as ProVerif can basically find a proof automatically using logic programming methods (horn clauses).

The definitions of security are fairly well understood; unfortunately there is a lot to go into so I can't expand on that here. Looking up "IND-CPA" and "IND-CCA" might be a good start; these are the security games/models of security for asymmetric encryption; you could move on to the models for key exchange algorithms there. Reading the [noise protocol spec](https://noiseprotocol.org/) is also a good start.

A professor in university had an interesting illustration of the attackers advantage.

First off, an attack is straight up impossible. If you need to invest ~ 10k operations for each atom in the observable universe to break a system with more than 50% probability, well. That won't get broken, until breakthroughs in related mathematics happen. Even if you were lucky to guess a key once, you will never be twice.

Then, you enter the area of throwing money at it. You can conquer quite a few exponents of two of search space if you throw a distributed system worth billions of dollars at it. And a couple more millions in change in post-docs shaving off fractions off of that exponent. Here you are usually safe, since it'll be hard even with all that hardware, manpower and math research.

But once it's exponential growth with lower exponents or even polynomial, it's just an implementation and optimization issue on the way to real-time decodeability.

However, even if the math is hard, the implementation might not be. And that's why a formally proven implementation of a very hard algorithm is exciting. If the implementation is provably as hard as discrete logarithms, and you get broken, a silly amount of modern crypto gets broken all at once.

Or we might learn something about formal verification and your method and tooling. Which is also good progress.

Thank you for the informative comment!

Wouldn't the proof be: assuming discrete log is NP hard, then these specific properties hold?

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

(my answer is general and not specific to this submission)

The question is too broad to be answered, there are many different formal verification techniques (including static formal verification techniques, and also dynamic formal verification techniques which happen at runtime), and you could be formally verifying only specific properties of the system.

Now, if your formal verification technique forces you to check that each index you use is within bounds (for instance, by forcing you to write loop invariants for each loop, but that's not sufficient because you can index buffers outside a loop or with something unrelated to the loop invariant), then yes, you have proved that you will not overflow buffers.

But those pesky implementations are always imperfect and never totally proved correct, what's more they run on pesky hardware which could have flaws and which is usually not itself perfectly verified, so…

And then you have model checking, which is also a formal verification technique. You can prove that you won't overflow buffers… in the model (which is a spec). That proves that your spec is sound and that you can implement it without flaws, but it does not actually check that your implementation is correct, of course. Unless your model checking tool can also build the implementation and this feature is proved correct.

edit: it seems my model checking paragraph is more relevant than I expected, this submission is actually about model checking if it checks the protocol (and not the implementation).

Author here: No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does

We are investigating ways how to do more formal verification for the implementation itself.

> Writing the implementation in Rust does

sigh, not true.

https://tgrez.github.io/posts/2022-06-19-buffer-overflow-in-... https://shnatsel.medium.com/how-rusts-standard-library-was-v... "This is a buffer overflow bug in the standard library’s implementation of a double-ended queue." "Rust will panic if you attempt to write out of bounds."

Writing the implementation will increase memory safety but only if the implementation adheres strictly to safe Rust - which means even avoiding ANY packages that use unsafe features. The fact Rust can pull in any package that has an unsafe {} block means you're not promised to be safe.

The equivalent could be said about writing the implementation in JavaScript, Python, etc... (that they protect against buffer overflows)

Granted, writing things in Rust doesn't exclude the possibility of a buffer overflow entirely. It does help make it much less likely.

Yes, I mentioned it :)

So any claim such as your previous one is rather of no value.

>It does help make it much less likely.

Yeah... To the same extent as the infamous proof of formal correctness of an example program published in a book, until the program was tested negatively by a student some months later.

Panicking when writing out of bounds is not a bad thing though, this is the behavior you want, assuming you can't statically guarantee that indexes are always in bounds.

It is true though that the underlying unsafe rust in std, or crates or whatnot can have errors though and sometimes we just kind of pretend it's not there since we don't see it.

>The equivalent could be said about writing the implementation in JavaScript, Python, etc... (that they protect against buffer overflows)

This is why we should be encouraging people to write in memory safe languages in general and not just rust or whatever. The overwhelming majority of software does not need to be some super optimized native-code SIMD+AVX1024 beast and would run on something like .net or the JVM, and even Python with no issues. It makes me cringe every time I see some random utils written in C that would work fine in Python.

> No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does

I don't believe writing the implementation in Rust does that: https://blog.rust-lang.org/2018/09/21/Security-advisory-for-...

One would think that this would be fixed in the last five years?

Certainly. What I don't believe is certain is that only one such vulnerability has ever existed and none exist in Rust today.

It's not pedantic to differentiate between mitigating a thing and preventing a thing.

You can add `#![forbid(unsafe_code)]` to your codebase to avoid any unsafe Rust, which should prevent buffer overflows. Obviously it may make writing a codebase somewhat harder.

Will that restriction also be applied transitively to all dependencies?

No. That kind of restriction cannot realistically be applied to any project above toy scale. The stdlib uses unsafe code to implement a large number of memory management primitives, because the language is (by design!) not complex enough to express every necessary feature in just safe code. Rust's intention is merely to limit the amount of unsafe code as much as possible.

For that, I believe you need to use cargo-geiger[0] and audit the results.

[0] - https://github.com/rust-secure-code/cargo-geiger

No, and in fact that would be impractical, because you can't do anything useful (e.g., any I/O whatsoever) without ultimately either calling into a non-Rust library or issuing system calls directly, both of which are unsafe.

The amount of reported and unfixed memory bugs in Rust went 10x more, not less in the last 5 years.

If you believe you can find a memory unsafety vulnerability in this project's Rust code based on the existence of those bugs, feel free to do so.

They verified the protocol, not the actual implementation: https://github.com/rosenpass/rosenpass#security-analysis

This is still a pretty neat result! End-to-end proofs from high level protocol to low level implementation are mostly still a research topic.

Related: Coq - https://coq.inria.fr/

And CompCert, a formally verified C compiler written in Coq: https://compcert.org/

(even then, there are parts which are not formally verified, mostly at the interfaces with the outside world)

Author of Rosenpass here;

Coq is fairly generic; it has a long history and made it possible to write some really cool proofs such as a proof of the four colors theorem, but writing crypto proofs is really hard using Coq.

For symbolic verification Tamarin and ProVerif are the tools of choice; I used ProVerif.

For proofs of security for protocols EasyCrypt and CryptoVerif can be used. CryptoVerif, ProVerif and Coq where developed at the same Institute by the way; at Inria Paris.

Although it would be a great exercise in hybrid SPARK+Coq proof. If (that's a big if) you can specify your algorithm in SPARK then (I think) you can use either the SPARK automated/guided prover, or when it can't discharge the proof, use some predefined lemmas, and barring that go down to the interactive Coq environment (or Isabelle, I've seen it done once) and discharge the verification conditions.

Not sure anyone has published such a multi-layer spec and proof effort /with crypto code in the mix/.

From the read me:

As with any application a small risk of critical security issues (such as buffer overflows, remote code execution) exists; the Rosenpass application is written in the Rust programming language which is much less prone to such issues.

I think their formal analysis is only security/crypto related, at least for the time being.

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 reasonable to hope that once formally verified PQ primitives are in place, a fully verified protocol implementation could be generated?

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.

My verifier (cbmc) does, the ones they used not. Frama-C/Eye would also catch buffer overflows.

I suppose if its implemented in a language that is formally proven to not allow buffer overflows.

The code signing project I worked on was formally verified. The whole time they were verifying it I found horrible bugs that needed fixing. One even made it past soft launch. So great job boys but this doesn’t help me.

What is a bug in the spec? Or in a part that was not formally verified?

There are a couple of presentations out there about how challenging it is to use XML-Sig correctly. The XML part introduces a whole raft of ambiguities. Chief amongst them is document.getElementByID() and element.getElementByID() can return different answers. Compression file formats have similar ambiguities you need to work out to avoid doppelgängers, and then also avoid overwriting system files via canonical path bugs.

Essentially the answer depends on who you ask. For my part I would say both.

I have not been following this closely but I thought most all of the quantum safe algorithms that had been proposed so far had been found lacking for traditional attacks very soon after they where held up as a standard contender. Has this changed?

I believe three of the four contenders for round 4 of the NIST competition are still showing secure:

https://en.wikipedia.org/wiki/NIST_Post-Quantum_Cryptography...

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.

One of the KEMS they've elected to (McEliece) has been around since the 70's, and has arguably been studied more than the others. If you're not quite sure about lattices, I've heard it called the "conservative choice" for a PQ KEM.

Why not just use PresharedKey in Wireguard?

Using a PSK alone doesn't make WireGuard quantum-safe. The security of the key exchange mechanism in WireGuard, which relies on the Diffie-Hellman protocol, is still vulnerable to quantum attacks.

If an attacker were to obtain the PSK and use a quantum computer to break the Diffie-Hellman key exchange, they would be able to decrypt the VPN traffic.

This is currently the thought-process and main reason behind why PQWG (Post Quantum Wireguard) are actively being researched [1].

[1] https://ieeexplore.ieee.org/document/9519445/

> Using a PSK alone doesn't make WireGuard quantum-safe.

Not sure what you're trying to say here. If you share the PSK out-of-band, securely, then wireguard is quantum resistant (I wouldn't say quantum-safe, because I'm not that optimistic).

> If an attacker were to obtain the PSK

Indeed if the attacker obtains the PSK then obviously the PSK isn't going to help you.

Wireguard explicitly mentions that mixing in a PSK provides post-quantum security [1].

1: https://www.wireguard.com/protocol/

Please be careful in your quoting. The page you linked says "post-quantum resistance", not "post-quantum security" (which would be a much stronger claim).

> If an attacker were to obtain the PSK

I believe it is traditional, in most threat models, to assume that the attacker doesn't have your private keys.

That's what they're doing, generating a key using post-quantum crypto and using it as the PSK - from TFA: "The tool establishes a symmetric key and provides it to WireGuard. Since it supplies WireGuard with key through the PSK feature using Rosenpass+WireGuard is cryptographically no less secure than using WireGuard on its own ("hybrid security"). Rosenpass refreshes the symmetric key every two minutes."

Author here;

We are :) Rosenpass is a fancy way of generating a PSK for WireGuard.

You still can. The problem arises when you don't actually wanna pre-share the key, and you still want post-quantum forward secrecy. Then you need a PQ KEM like McEliece or Kyber to run a PQ-secure key establishment.

That doesn't solve the key management problem, it just defines it as out-of-scope, since you still need to exchange that preshared key outside Wireguard.

Why not just use preshared keys in all VPNs like IPSEC?

Because key exchange and key rotation is a huge problem.

Is it any harder than exchanging and rotating asymmetric keys?

You can do that on top of a public/private keypair, too.

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

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.

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

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).

Do you have a reason to not use Kyber? The way it is combined should be sound.

Not in particular. Yes, the way they are combining them should be sound.

Rosenpass author here;

Mate, you could just read the code…or give it a try ;)

> the WG author seems like he doesn't care about PQC

This is plainly not true; WG supports post-quantum security with the use of the PSK mechanism as we do. PQ-crypto is high quality but it is also new and fairly inefficient; not a good thing to integrate into the kernel directly. Using the PSK mechanism is the best way to do this I know of at this point in time.

> 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.

WireGuard establishes a session with the existing PSK; we replace the PSK every two minutes but WireGuard keeps its established session around until it renegotiates a session.

Both WG and RP rekey their session every two minutes; there is no interruption.

So is the rosenpass tunnel separate from the non PQC tunnel (the non PQC tunnel being used just for rosenpass)?

Because afaik the moment the PSK is changed all packets immediately start being encrypted by it.

If the change doesn't coincide on both the sender and receiver (within an instant), there will be dropped packets until both PSK's are the same again. Being separate from WG, I don't see how you can insert yourself into their state machine for better coordination.

Starred! And thanks to the author for taking the time to answer so many questions here!

This available in tailscale?

Interesting people downvote me without bothering to answer. I'll take that as a no, but it's valid question, depsite the downvotes.

I'm too stupid to understand the crypto technicalities. Is this really a good solution? Or embrace, extend, extinguish targeted on Wireguard?

The paper abstract mentions a "cookie"-like concept, and from websec I know that cookies are not always the optimal solution and historically cookie implementations had a lot of attack surface.

EDIT: Seems to come from German Max-Planck Institute which is funded by German government.

The article refers to a "cookie" as a "biscuit"

"Lacking a reliable way to detect retransmission, we remove the replay protection mechanism and store the responder state in an encrypted cookie called “the biscuit” instead. Since the responder does not store any session-dependent state until the initiator is interactively authenticated, there is no state to disrupt in an attack."

Both WG and PQWG are vulnerable to state disruption attacks; they rely on a timestamp to protect against replay of the first protocol message. An attacker who can tamper with the local time of the protocol initiator can inhibit future handshakes, rendering the initiator’s static keypair practically useless.

The use of the insecure NTP protocol is the reason for the "cookie" / "Biscuit" mechanism.

AFAIK a NTP client doesn't accept a value which highly differentiates from the current time. At least, not without user interaction. Does that render this attack less likely?

Rosenpass author here.

It does yes. But it is a mitigation, not a real fix.

An attacker could still just speed up time. Although not being able to produce a KillPacket for the year three thousand is a good thing :)

Rosenpass author here; I myself am independent, thus funding by NLNet. We have some project participants who are Freelancers; two of my co-authors are employed at research institutes. One of my co authors is employed at MPI-SP.

The cookie thing is a defense against WireGuard CVE-2021-46873; the attack is in my view not bad enough to get rid of the WireGuard protocol. WG is still the standard for pre-quantum VPN implementations. Rosenpass also needs to use post-quantum crypto-primitives that need a lot of cpu and memory resources.

Rosenpass and WireGuard work together; Rosenpass runs in userspace and gives keys to WireGuard so we do not plan to replace it any time.

It would be possible to apply the biscuit mechanism to classical WireGuard; unfortunately that would cause a protocol incompatibility. I am not sure if they are going to take that path.

> EDIT: Seems to come from German Max-Planck Institute which is funded by German government.

On the Github repo it says:

"Supported by

Funded through NLNet with financial support for the European Commission's NGI Assure program."

On the website it says:

"Funded through NLnet with financial support from the European Commission's NGI Assure program."

On the paper it says MPI

European program funding a University team, no?

One of the people involved works for the MPI as a crypto researcher, however the project itself was funded by NLnet

Reply on news.ycombinator.com