Sites Inria

English version

Séminaire des équipes de recherche

Séminaire Prosecco : Verifying a mixture of C and assembly code with Low* and Vale

© INRIA Sophie Auvin - P comme Protocole

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:

Mots-clés : Science Inria Prosecco Recherche Séminaire Vale Low* Assembly Code

Haut de page

Suivez Inria

Siège et centres de recherche Inria

Accès direct


Ressources