Paper 2024/1203
Preservation of Speculative Constant-time by Compilation
Abstract
Compilers often weaken or even discard software-based countermeasures commonly used to protect programs against side-channel attacks; worse, they may also introduce vulnerabilities that attackers can exploit. The solution to this problem is to develop compilers that preserve these countermeasures. Prior work establishes that (a mildly modified version of) the CompCert and Jasmin formally verified compilers preserve constant-time, an information flow policy that ensures that programs are protected against cache side-channel attacks. However, nothing is known about preservation of speculative constant-time, a strengthening of the constant-time policy that ensures that programs are protected against Spectre v1 attacks. We first show that preservation of speculative constant-time fails in practice by providing examples of secure programs whose compilation is not speculative constant-time using GCC (GCC -O0 and GCC -O1) and Jasmin. Then, we define a proof-of-concept compiler that distills some of the critical passes of the Jasmin compiler and use the Coq proof assistant to prove that it preserves speculative constant-time. Finally, we patch the Jasmin speculative constant-time type checker and demonstrate that all cryptographic implementations written in Jasmin can be fixed with minimal impact.
Metadata
- Available format(s)
-
PDF
- Category
- Applications
- Publication info
- Preprint.
- Keywords
- formal methodsSpectrespeculative constant-timepreservationcompilers
- Contact author(s)
-
santiago arranz-olmos @ mpi-sp org
gilles barthe @ mpi-sp org
lionel blatter @ mpi-sp org
benjamin gregoire @ inria fr
vincent laporte @ loria fr - History
- 2024-07-29: approved
- 2024-07-25: received
- See all versions
- Short URL
- https://ia.cr/2024/1203
- License
-
CC0
BibTeX
@misc{cryptoeprint:2024/1203, author = {Santiago Arranz Olmos and Gilles Barthe and Lionel Blatter and Benjamin Grégoire and Vincent Laporte}, title = {Preservation of Speculative Constant-time by Compilation}, howpublished = {Cryptology {ePrint} Archive, Paper 2024/1203}, year = {2024}, url = {https://eprint.iacr.org/2024/1203} }