Partager cette page :

Séminaire #1 mercredi 16/09/2020 par David Pichardie : Formal Verification of a Constant-Time Preserving C Compiler

le 16 septembre 2020

17h30-18h30

ENS Rennes En distanciel sur ce serveur BigBlueButton

Intervention de David Pichardie, professeur des universités à l'ENS Rennes, chercheur dans l'équipe CELTIQUE de l'IRISA et Inria Rennes, dans le cadre des séminaires du département Informatique et télécommunications.

Séminaire Informatique et télécommunications - Seminaire-DIT.jpg

/medias/photo/seminaire-dit_1599740647464-jpg

Timing side-channels are arguably one of the main sources of vulnerabilities in cryptographic implementations. One effective mitigation against timing side-channels is to write programs that do not perform secret-dependent branches and memory accesses. This mitigation, known as "cryptographic constant-time", is adopted by several popular cryptographic libraries.

This work focuses on compilation of cryptographic constant-time programs, and more specifically on the following question: is the code generated by a realistic compiler for a constant-time source program itself provably constant-time? Surprisingly, we answer the question positively for a mildly modified version of the CompCert compiler, a formally verified and moderately optimizing compiler for C. Concretely, we modify the CompCert compiler to eliminate sources of potential leakage. Then, we instrument the operational semantics of CompCert intermediate languages so as to be able to capture cryptographic constant-time. Finally, we prove that the modified CompCert compiler preserves constant-time. Our mechanization maximizes reuse of the CompCert correctness proof, through the use of new proof techniques for proving preservation of constant-time. These techniques achieve complementary trade-offs between generality and tractability of proof effort, and are of independent interest.

De 17h30 à 18h30 en visio-conférence via ce serveur BigBlueButton. Séminaire ouvert à toutes et à tous, élèves et personnel de l'ENS Rennes et extérieurs, tous départements confondus. Obligatoire pour les élèves de 1re et 2e année du département informatique.

Thématique(s)
Formation, Recherche - Valorisation
Contact

Mise à jour le 3 septembre 2021