Survey of Verified Cryptography

Abstract

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
• Memory Safety
• Functional Correctness
• Resistance to Side-Channel Attacks
3. Tools
• F* and Low* - Programming language to implement specifications and efficient implementations.
• HACL* - Verified cryptographic algorithms.
4. Conclusion

Definitions

• F* - Programming language based on F# which compiles to either OCaml or F#, and has built-in machinery to generate lemmas that can be tested by Z3 to verify program behavior. There is also a special dialect called Low* which can be extracted to C for additional verification and embedding.
• HACL* - A library of cryptography algorithms and primitives written in Low*. These can be compiled to C and integrated into existing codebases.

---

Overview

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.

Documents

• Project Update (slides)
• Project Final (slides)
• Project Final (paper)

References

1. HACL*: A Verified Modern Cryptographic Library. https://eprint.iacr.org/2017/536.pdf
2. Verified Low-Level Programming Embedded in F*. https://arxiv.org/pdf/1703.00053.pdf
3. Implementing and Proving the TLS 1.3 Record Layer. https://eprint.iacr.org/2016/1178.pdf
4. Dependent Types and Multi-monadic Effects in F*. https://eprint.iacr.org/2016/1178.pdf

---

Up