Tom Arnold

Survey of Verified Cryptography


Secure cryptosystems are frequently defeated by flawed implementations. This paper looks at formal methods to verify implementation correctness of cryptosystems in software. Specifically we review the FStar (F*) programming language and its use to build HACL*, a library of verified cryptography primitives.

Table of Contents

  1. Overview
  2. Aspects of Verified Cryptography
  3. Tools
  4. Conclusion



In class we focus heavily on correctness of algorithms and the mathematical theorems that show that a particular cryptosystem is secure, but in the real world these systems are plagued with implementation issues that weaken or break them. Some examples of these failures are HeartBleed (memory safety) where an attacker specified buffer size could be used to read encryption keys out of process memory, and Apple's Goto bug (logic errors) where an extra goto and lack of braces caused certificate validation code to be skipped unconditionally. In this paper we look at tools being developed and used by Microsoft Research and INRIA to verify implementations of cryptographic algorithms.



  1. HACL*: A Verified Modern Cryptographic Library.
  2. Verified Low-Level Programming Embedded in F*.
  3. Implementing and Proving the TLS 1.3 Record Layer.
  4. Dependent Types and Multi-monadic Effects in F*.