High-Assurance Crypto Software

HACS – Projects & Links

Please find below links to projects, tools, libraries, and general reading material that is relevant to HACS. Most of these projects are with involvement of HACS participants; some grew out of a collaboration that started through the HACS workshop.

Formally verified crypto

  • CertiKOS: kernel with clean-slate design with end-to-end guarantees on extensibility, security, and resilience
  • hacl*: an F* verified cryptographic library
  • hacrypto: snapshots, architectures, audits, validation, and verification of crypto libraries
  • miTLS: a verified reference implementation of TLS
  • WIP: applying SAW to OpenSSL
  • seL4: an L4 kernel verified with Isabelle/HOL
  • Verificatum: verified crypto for voting protocols

Tools for verification

  • AutoG&P: tool for performing highly automated game-hopping proofs for pairing-based cryptographic primitives
  • CBMC: a bounded model checker for C and Java
  • CompCert A verified C compiler, written in Coq
  • The Coq Proof Assistant
    While you can install Coq with apt-get install coqide or executing the binary/dmg if you use Windows. The best way to install coq is to use opam:
    sudo apt-get install gcc 
    sudo apt-get install opam
    opam init
    opam switch coq --alias-of 4.04.0
    opam install coq 
    opam install coqide
    opam repo add coq-released https://coq.inria.fr/opam/released
    opam install coq-mathcomp-ssreflect
    opam install menhir
  • Crucible: a language-agnostic library for performing forward symbolic execution of imperative progams
  • Cryptol: a domain-specific language for specifying cryptographic algorithms
  • EasyCrypt: a toolset for reasoning about relational properties of probabilistic computations with adversarial code
  • Entroposcope: a tool for finding entropy loss bugs in PRNGs
  • F*: an ML-like language with a type system for program verification
  • Fiat Crypto: automatic derivation of fast crypto-primitive code (for now just ECC) from specifications in Coq, generating proofs along the way
  • Frama-C: an extensible and collaborative platform dedicated to source-code analysis of C software
  • gfverif: fast and easy verification of finite-field arithmetic
  • hacspec: a language for specifying crypto
  • Ivory: an eDSL for safe systems programming. You can think of Ivory as a safer C, embedded in Haskell
  • Kami: tool for verified hardware design (ISA->RTL)
  • KeY: a deductive verifier of functional correctness of Java programs (wrt properties annotated in JML)
  • Kremlin: translate a subset of F* to C
  • Software Analysis Workbench (SAW)
  • Vale: Verified Assembly Language for Everest
  • VeriFast: a verifier for single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic
  • Verified Software Toolchain (VST): software toolchain which includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program
  • ZooCrypt: fully automated analysis of padding-based encryption

Fuzzing tools


Reading material