Formal verification

[mratsim]

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]

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

[mratsim]

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]

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]

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

[mratsim]

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]

Cryptoline can verify assembler for cryptography:

• https://github.com/fmlab-iis/cryptoline
• https://dl.acm.org/doi/pdf/10.1145/3319535.3354199

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

• https://github.com/fmlab-iis/gcc2cryptoline
• https://github.com/fmlab-iis/llvm2cryptoline

Jasmin can generate formally-verified assembly:

• https://formosa-crypto.org/
• https://dl.acm.org/doi/pdf/10.1145/3133956.3134078
• https://blog.cloudflare.com/post-quantum-easycrypt-jasmin/

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