Skip to Main content Skip to Navigation
Preprints, Working 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 metadatas

Cited literature [41 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/hal-02983256
Contributor : Vincent Laporte <>
Submitted on : Thursday, October 29, 2020 - 6:11:16 PM
Last modification on : Sunday, November 1, 2020 - 3:33:26 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02983256, version 1

Collections

Citation

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

Share

Metrics

Record views

47

Files downloads

53