Skip to Main content Skip to Navigation
New interface
Conference papers

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification

Abstract : We present a new tool for the generation and verification of high-assurance high-speed machine-level cryptography implementations: a certified C compiler supporting instruction extensions to the x86. We demonstrate the practical applicability of our tool by incorporating it into supercop: a toolkit for measuring the performance of cryptographic software, which includes over 2000 different implementations. We show i. that the coverage of x86 implementations in supercop increases significantly due to the added support of instruction extensions via intrinsics and ii. that the obtained verifiably correct implementations are much closer in performance to unverified ones. We extend our compiler with a specialized type system that acts at pre-assembly level; this is the first constant-time verifier that can deal with extended instruction sets. We confirm that, by using instruction extensions, the performance penalty for verifiably constant-time code can be greatly reduced.
Complete list of metadata

Cited literature [41 references]  Display  Hide  Download
Contributor : Vincent Laporte Connect in order to contact the contributor
Submitted on : Thursday, October 29, 2020 - 6:11:16 PM
Last modification on : Sunday, June 26, 2022 - 2:55:33 AM
Long-term archiving on: : Saturday, January 30, 2021 - 6:26:35 PM


Files produced by the author(s)


  • HAL Id : hal-02983256, version 1



José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira. Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. Indocrypt 2020, Dec 2020, Bangalore, India. ⟨hal-02983256⟩



Record views


Files downloads