Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/71547
Título: | Certified compilation for cryptography: Extended x86 instructions and constant-time verification |
Autor(es): | Almeida, José Bacelar Barbosa, Manuel Barthe, Gilles Laporte, Vincent Oliveira, Tiago |
Palavras-chave: | Certified compiler Constant-time simd supercop |
Data: | 2020 |
Editora: | Springer, Cham |
Revista: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Citação: | Almeida J.B., Barbosa M., Barthe G., Laporte V., Oliveira T. (2020) Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. In: Bhargavan K., Oswald E., Prabhakaran M. (eds) Progress in Cryptology – INDOCRYPT 2020. INDOCRYPT 2020. Lecture Notes in Computer Science, vol 12578. Springer, Cham. https://doi.org/10.1007/978-3-030-65277-7_6 |
Resumo(s): | 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. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/71547 |
ISBN: | 978-3-030-65276-0 |
e-ISBN: | 978-3-030-65277-7 |
DOI: | 10.1007/978-3-030-65277-7_6 |
ISSN: | 0302-9743 |
Versão da editora: | https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_6 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Certified Compilation for Cryptography.pdf | 451,65 kB | Adobe PDF | Ver/Abrir |