constantine icon indicating copy to clipboard operation
constantine copied to clipboard

Published 20 hours ago • verified publisher icon mratsim

Formal verification

Open mratsim opened this issue 5 years ago • 6 comments

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 avatar Feb 08 '20 11:02 mratsim

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

mratsim avatar Feb 09 '20 15:02 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 avatar Feb 23 '20 22:02 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 avatar Jun 19 '20 15:06 mratsim

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

mratsim avatar Jan 12 '21 20:01 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 avatar Aug 06 '22 12:08 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.

mratsim avatar Apr 26 '23 08:04 mratsim