Rosenpass – formally verified post-quantum WireGuard

by lima • 3 years ago

285 80 3 years ago

bflesch2• 3 years ago

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.

gzer02• 3 years ago

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.

Fnoord3• 3 years ago

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?

Fnoord3• 3 years ago

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

bflesch2• 3 years ago

On the paper it says MPI

wucke13• 3 years ago

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

sevenoftwelve10• 3 years ago

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.

madspindel• 3 years ago

Why not just use PresharedKey in Wireguard?

gzer02• 3 years ago

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/

ThePhysicist• 3 years ago

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

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

d-z-m6• 3 years ago

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.

yjftsjthsd-h2• 3 years ago

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.

Fnoord3• 3 years ago

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

miloignis• 3 years ago

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

CodesInChaos• 3 years ago

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.

sevenoftwelve10• 3 years ago

Author here;

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

d-z-m6• 3 years ago

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.

foobiekr• 3 years ago

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

Because key exchange and key rotation is a huge problem.

yjftsjthsd-h2• 3 years ago

Is it any harder than exchanging and rotating asymmetric keys?

Tepix• 3 years ago

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

l-lousy• 3 years ago

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.

jraph3• 3 years ago

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

ekiwi• 3 years ago

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.

jraph3• 3 years ago

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)

touisteur2• 3 years ago

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

hinkley2• 3 years ago

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.

jraph3• 3 years ago

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

ape4• 3 years ago

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

sevenoftwelve10• 3 years ago

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.

acaloiar2• 3 years ago

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

fallat2• 3 years ago

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)

rurban2• 3 years ago

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

thadt• 3 years ago

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?

api• 3 years ago

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.

_joel2• 3 years ago

This available in tailscale?

_joel2• 3 years ago

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

yellow_lead2• 3 years ago

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

dcow• 3 years ago

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

sevenoftwelve10• 3 years ago

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.

tetha• 3 years ago

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.

yellow_lead2• 3 years ago

Thank you for the informative comment!

wstuartcl• 3 years ago

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?

jrexilius• 3 years ago

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

d-z-m6• 3 years ago

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.

sevenoftwelve10• 3 years ago

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.

wolf550e• 3 years ago

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

chaxor• 3 years ago

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

sevenoftwelve10• 3 years ago

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.

inChargeOfIT• 3 years ago

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

rogers184455• 3 years ago

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

KateLawson• 3 years ago

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.

rogers184455• 3 years ago

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.

eternalban• 3 years ago

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

themodelplumber• 3 years ago

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

Rosenpass – formally verified post-quantum WireGuard

Related Stories