Verified Low-Level Programming Embedded in F*

Jonathan Protzenko (RiSE: Research in Software Engineering, Microsoft Research, Redmond, WA, USA)
Jean-Karim Zinzindohoué (Prosecco, INRIA, Paris, France)
Aseem Rastogi (Microsoft Research, Bengaluru, Karnataka, India)
Tahina Ramananandro (RiSE)
Peng Wang (RiSE; CSAIL, MIT, Cambridge, MA, USA)
Santiago Zanella-Béguelin (Programming Principles and Tools, Microsoft Research, Cambridge, United Kingdom)
Antoine Delignat-Lavaud(Programming Principles and Tools)
Catalin Hritcu (Prosecco)
Karthikeyan Bhargavan (Prosecco)
Cédric Fournet (Programming Principles and Tools)
Nikhil Swamy (RiSE)

ICFP 2017

• Conference paper (final version at ACM Digital Library)
• Paper preprint
• Submission (pre-review) version on arXiV
• Artifact submitted to the ICFP 2017 Artifact Evaluation:
  • Docker image
  • sources (also available at Zenodo)
  • GitHub branch

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