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

ver descrição completa

Detalhes bibliográficos
Autor principal: Almeida, José Bacelar (author)
Outros Autores: Barbosa, Manuel (author), Barthe, Gilles (author), Laporte, Vincent (author), Oliveira, Tiago (author)
Formato: conferencePaper
Idioma:eng
Publicado em: 2020
Assuntos:
Texto completo:http://hdl.handle.net/1822/71547
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/71547