Verified Low-Level Programming Embedded in F*
This work addresses the need for secure and efficient low-level software, particularly in cryptography, by providing a verified programming approach that is incremental in combining existing verification techniques with a new embedded language.
The authors tackled the problem of writing and verifying low-level, high-assurance cryptographic code by developing Low*, a language embedded in F*, which ensures memory safety and functional correctness through typing and verification. They demonstrated its effectiveness by implementing and verifying about 28,000 lines of cryptographic code that achieves performance competitive with unverified C libraries.
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently-typed variant of ML aimed at program verification. Departing from ML, Low* does not involve any garbage collection or implicit heap allocation; instead, it has a structured memory model à la CompCert, and it provides the control required for writing efficient low-level security-critical code. By virtue of typing, any Low* program is memory safe. In addition, the programmer can make full use of the verification power of F* to write high-level specifications and verify the functional correctness of Low* code using a combination of SMT automation and sophisticated manual proofs. At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance. We provide a new compiler back-end from Low* to C and, to evaluate our approach, we implement and verify various cryptographic algorithms, constructions, and tools for a total of about 28,000 lines of code, specification and proof. We show that our Low* code delivers performance competitive with existing (unverified) C cryptographic libraries, suggesting our approach may be applicable to larger-scale low-level software.