search

mratsim / constantine

Constantine: modular, high-performance, zero-dependency cryptography stack for verifiable computation, proof systems and blockchain protocols.
Other
389 stars 43 forks source link

Formal verification #6

Open mratsim opened 4 years ago

mratsim commented 4 years ago

Given that Constantine aims to be used for elliptic curve cryptographic, it is required to be proved bug-free.

Traditional model checker like TLA+ or Spin are more suited to formally distributed consensus protocols or concurrent data structures.

However the Galois companies offer SAW, a formal verifier that supports C and is used to AES, SHA and ECDSA formal verification: https://saw.galois.com/, it is based on Z3 https://github.com/GaloisInc/saw-script

mratsim commented 4 years ago

Nice PDF presented at Black Hat conference 2015 on finding BigNum vulnerabilities: https://comsecuris.com/slides/slides-bignum-bhus2015.pdf

mratsim commented 4 years ago

Formally verified crypto code generated from Coq.

Thesis: http://adam.chlipala.net/theses/andreser_meng.pdf Crafting Certified Elliptic CurveCryptography Implementations in Coq

Paper: http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf

Repo: https://github.com/mit-plv/fiat-crypto

mratsim commented 4 years ago

Using Z3 for formally verifying bignum implementation and example on an OpenSSL CVE: https://kryptoslogic.blogspot.com/2015/01/openssls-squaring-bug-and-opportunistic.html

Also: http://crypto.di.uminho.pt/CACE/ from the paper: Practical realisation and elimination of an ECC-related software bug attack. https://eprint.iacr.org/2011/633.pdf

mratsim commented 3 years ago

Formally verified crypto assembly primitives using Dafny (and Z3): https://project-everest.github.io/assets/vale2017.pdf

mratsim commented 2 years ago

Using Why3

https://eprint.iacr.org/2021/415.pdf - Efficient Verification of Optimized Code Correct High-speed X25519

Frama-C which inspired Dr.Nim uses Why3 in the backend.

mratsim commented 1 year ago

Cryptoline can verify assembler for cryptography:

It works directly on the compiler internal representation (Gimple for GCC, LLVM IR for LLVM)

Jasmin can generate formally-verified assembly:

Like Vale, it also uses Dafny+Z3 for formal verification and the Jasmin compiler itself is written in Coq.