Formal verification of a constant-time preserving C compiler
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Dec 20, 2019
- Source ID
- 10.1145/3371075
Entities
People
- Alix Trieu
- Benjamin Grégoire
- David Pichardie
- Gilles Barthe
- Rémi Hutin
- Sandrine Blazy
- Vincent Laporte
Organizations
- Aarhus University
- Institut National de Recherche en Informatique et en Automatique
- Instituto Madrileño de Estudios Avanzados
- Natural Sciences, Danish Council for Independent Research
- Office of Naval Research
- University of Rennes