Séminaire des équipes de recherche
Séminaire Prosecco : 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
- Lieu : Mercredi 9 octobre, 11h00 ✫ Salle Jacques-Louis Lions 2
- Intervenant(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 : Mercredi 9 Octobre 2019
- Heure : 11h00
- Lieu : Salle Jacques Louis Lions 2