Over 4000 free audio and video lectures, seminars and teaching resources from Oxford University.
Skip to Content Skip to Navigation

Thank you for visiting! Please consider filling out our questionnaire. This will help us improve our service providing free educational media recorded from the University of Oxford. Many thanks!

Click here to access the survey (3 minutes to complete).

Verified Low-Level Programming Embedded in F

Loading Video...
Duration: 0:18:12 | Added: 18 Dec 2017
Jonathan Protzen, Microsoft Research, United States, gives the second talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference.

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.

Copy and paste this HTML snippet to embed the audio or video on your site: