Verified Low-Level Programming Embedded in F

Co-written by Jonathan Protzen (Microsoft Research, United States), Jean-Karim Zinzindohoué (Inria, France), Aseem Rastogi (Microsoft Research, India), Tahina Ramananandro (Microsoft Research, United States), Peng Wang (Massachusetts Institute of Technology, USA), Santiago Zanella-Beguelin (Microsoft Research), Antoine Delignat-Lavaud (Microsoft Research), Catalin Hritcu (India and Paris), Karthikeyan Bhargavan (Inria, France), Cedric Fount (Microsoft Research), Nikhil Swamy (Microsoft Research, United States).

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 a 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.