High-Assurance Crypto Software

HACS – Projects & Links

Please find below a non-comprehensive list of links to projects, tools, and libraries that are relevant to HACS. Many of these projects are with involvement of HACS participants; some grew out of collaborations that started through the HACS workshop.

Formally verified crypto

  • by-inversion: Formalization of a prime field inversion algorithm by Bernstein and Yang
  • Fiat-Crypto: automatic derivation of fast field arithmatic code from specifications in Coq
  • HACL*: a verified cryptographic library in F* including verified assembly code from Vale
  • hacrypto: verified crypto primitives using SAW/Cryptol
  • Jasmin: verified assembly implementations of crypto primitives
  • A Formal Proof of safegcd Bounds
  • ValeCrypto: formally verified high-performance cryptographic code in assembly language

Other verification projects

  • CertiKOS: kernel with clean-slate design with end-to-end guarantees on extensibility, security, and resilience
  • CompCert A verified C compiler, written in Coq
  • seL4: an L4 kernel verified with Isabelle/HOL
  • miTLS: a verified reference implementation of TLS
  • DeepSpec: specification and verification of full functional correctness of software and hardware
  • Project Everest: verified end-to-end secure transport
  • RustBelt: Logical Foundations for the Future of Safe Systems Programming

Tools for verification

  • AutoG&P: tool for performing highly automated game-hopping proofs for pairing-based cryptographic primitives
  • Binsec/Haunted: A binary-level analyzer to detect Spectre attacks.
  • CASM-verify: Automatic Equivalence Checking for AssemblyImplementations of Cryptography Libraries
  • CBMC: a bounded model checker for C and Java
  • CompCert A verified C compiler, written in Coq
  • The Coq Proof Assistant
  • Crucible: a language-agnostic library for performing forward symbolic execution of imperative progams
  • CryptHOL: A framework for formalising cryptographic arguments in Isabelle/HOL; see also ePrint 2018/941
  • Cryptol: a domain-specific language for specifying cryptographic algorithms
  • Cryptoline: verification of low-level implementations of mathematical constructs
  • CryptoVerif: cryptographic protocol verifier in the computational model
  • EasyCrypt: a toolset for reasoning about relational properties of probabilistic computations with adversarial code
  • EasyUC: Experiments with Universal Composability in EasyCrypt
  • 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
  • Jasmin: high-speed and high-assurance cryptographic software in assembly
  • 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
  • FaCT: A DSL for timing-sensitive computation
  • HoRSt: Horn clause based sound static analysis
  • ProVerif: automatic cryptographic protocol verifier in the formal (Dolev-Yao) model
  • qrhl-tool: Proof assistant for qRHL
  • RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
  • Rust verification tools
  • Software Analysis Workbench (SAW)
  • Tamarin: security protocol verification tool that supports both falsification and unbounded verification in the symbolic model.
  • UC-DSL: UC Domain Specific Language
  • 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
  • Verifpal: a protocol analyzer and verifier with a focus on real-world protocols and ease of use
  • Verified Software Toolchain (VST): software toolchain that uses static analyzers and proof assistants to verify software
  • ZooCrypt: fully automated analysis of padding-based encryption

Fuzzing and testing tools

  • AFL: american fuzzy lop
  • Cryptofuzz: Differential cryptography fuzzing
  • libFuzzer: a fuzzer
  • OSS-Fuzz: fuzzing service for open-source software
  • Wycheproof: testing crypto libraries against known attacks

Other HACS-related projects

  • OpenTitan: Open source project building a transparent, high-quality reference design and integration guidelines for silicon root of trust (RoT) chips
  • SCARV: Side-channel security for RISC-V
  • Simplicity: A blockchain programming language designed as an alternative to Bitcoin script