Certified compilation for cryptography: Extended x86 instructions and constant-time verification

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...

Full description

Bibliographic Details
Main Author: Almeida, José Bacelar (author)
Other Authors: Barbosa, Manuel (author), Barthe, Gilles (author), Laporte, Vincent (author), Oliveira, Tiago (author)
Format: conferencePaper
Language:eng
Published: 2020
Subjects:
Online Access:http://hdl.handle.net/1822/71547
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/71547