Research Teams Seminar
Prosecco Seminar: Verifying a mixture of C and assembly code with Low* and Vale
For performance and security reasons, it is sometimes necessary to program at the lowest levels of abstraction, using a mixture of C and assembly. In this talk, we present techniques that allow verifying such code for correctness and side-channel resistance.
- Date : 9/10/2019
- Place : Wednesday, October 9th, 11am ✫ Room Jacques-Louis Lions 2
- Guest(s) : Nik Swamy (MSR) and Aymeric Fromherz (CMU)
Our approach involves embedding two languages for verified C and assembly programming within F*, a proof assistant. The first, Low*, is a shallow embedding of a subset of C that enables verified code to be safely extracted to C without the use of a garbage collector or runtime bounds checks. The second, Vale, is a deep embedding of an assembly language with structured control flow---verified Vale programs can be easily printed as assembly programs.
This talk presents the design of Low* and Vale, focusing on their safe interoperation by reconciling differences in their memory models, calling conventions and side-channel defenses in a provable manner. Low* and Vale have been used together in EverCrypt, a high-performance verified cryptographic provider. Proofs of hand-optimized assembly code in Vale are carefully related to verified C code programmed in Low* to provide an end-to-end guarantee of correctness and security.
This talk is based on joint work with many people in the Project Everest team and is described in 3 recent papers:
- Date : Wednesday, October 9th 2019
- Hour : 11am
- Place: Inria de Paris, Room Salle Jacques Louis Lions 2