3 ms·
They verified the protocol, not the actual implementation: https://github.com/rosenpass/rosenpass#security-analysis https://github.com/rosenpass/rosenpass#secur
by ekiwi 4y ago
They verified the protocol, not the actual implementation: https://github.com/rosenpass/rosenpass#security-analysis 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.
- jraph 4y agoRelated: Coq - https://coq.inria.fr/ https://coq.inria.fr/ And CompCert, a formally verified C compiler written in Coq: https://compcert.org/ https://compcert.org/ (even then, there are parts which are not formally verified, mostly at the interfaces with the outside world)
- sevenoftwelve 4y agoAuthor 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.
- touisteur 4y agoAlthough 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/.