Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification - Université de Lorraine Access content directly
Conference Papers Year : 2020

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.
Fichier principal
Vignette du fichier
main.pdf (452.34 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02983256 , version 1 (29-10-2020)

Licence

Attribution

Identifiers

  • HAL Id : hal-02983256 , version 1

Cite

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⟩
247 View
442 Download

Share

Gmail Facebook X LinkedIn More