Formal verification about constantine HOT 6 OPEN

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

from constantine.

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

from constantine.

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

from constantine.

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

from constantine.

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.

from constantine.

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.

from constantine.