Hacker News new | ask | show | jobs
by ekiwi 1209 days 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.
2 comments
jraph 1209 days 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)

link
sevenoftwelve 1209 days ago
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.

link
touisteur 1209 days 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/.

link