Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Rosenpass – formally verified post-quantum WireGuard

github.com

Post reply on HN
Print view View original

31–40 of 86 posts

Re: Rosenpass – formally verified post-quantum WireGuard

#31

Post by ThePhysicist »

gzer0 wrote: post #5
madspindel wrote: post #3

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…

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

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

Re: Rosenpass – formally verified post-quantum WireGuard

#32

Post by emperorcezar »

acaloiar wrote: post #30
sevenoftwelve wrote: post #21

Earlier quoted context omitted.

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.

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

Re: Rosenpass – formally verified post-quantum WireGuard

#33

Post by fallat »

sevenoftwelve wrote: post #21
Tepix wrote: post #6

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

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)

Re: Rosenpass – formally verified post-quantum WireGuard

#34

Post by sevenoftwelve »

fallat wrote: post #33
sevenoftwelve wrote: post #21

Earlier quoted context omitted.

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 impleme…

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

Re: Rosenpass – formally verified post-quantum WireGuard

#35

Post by acaloiar »

emperorcezar wrote: post #32
acaloiar wrote: post #30

Earlier quoted context omitted.

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

Re: Rosenpass – formally verified post-quantum WireGuard

#36

Post by fallat »

sevenoftwelve wrote: post #34
fallat wrote: post #33

Earlier quoted context omitted.

> 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 impleme…

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

Re: Rosenpass – formally verified post-quantum WireGuard

#37

Post by touisteur »

ekiwi wrote: post #13
Tepix wrote: post #6

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

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.

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

Re: Rosenpass – formally verified post-quantum WireGuard

#38

Post by touisteur »

bflesch wrote: post #19
Fnoord wrote: post #12

Earlier quoted context omitted.

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

Re: Rosenpass – formally verified post-quantum WireGuard

#39

Post by hhda »

acaloiar wrote: post #35
emperorcezar wrote: post #32

Earlier quoted context omitted.

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.

Re: Rosenpass – formally verified post-quantum WireGuard

#40

Post by yellow_lead »

> 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

Post reply on HN