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

61–70 of 86 posts

Re: Rosenpass – formally verified post-quantum WireGuard

#61

Post by wolf550e »

sevenoftwelve wrote: post #56
wstuartcl wrote: post #41

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?

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.

Re: Rosenpass – formally verified post-quantum WireGuard

#62

Post by yjftsjthsd-h »

foobiekr wrote: post #53
madspindel wrote: post #3

Why not just use PresharedKey in 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?

Re: Rosenpass – formally verified post-quantum WireGuard

#63

Post by Jweb_Guru »

rurban wrote: post #47
emperorcezar wrote: post #32

Earlier quoted context omitted.

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

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.

Re: Rosenpass – formally verified post-quantum WireGuard

#64

Post by tetha »

sevenoftwelve wrote: post #55
yellow_lead wrote: post #40

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

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.

Re: Rosenpass – formally verified post-quantum WireGuard

#65

Post by [deleted] »

Jweb_Guru wrote: post #63
rurban wrote: post #47

Earlier quoted context omitted.

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.

[deleted]

Re: Rosenpass – formally verified post-quantum WireGuard

#69

Post by chlorion »

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…

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.

Post reply on HN