Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/50513
Título: | Jasmin: high-assurance and high-speed cryptography |
Autor(es): | Almeida, José Bacelar Barbosa, Manuel |
Palavras-chave: | High-speed cryptography Certified compilation Cryptographic implementations Verified compiler Safety Constant-time security |
Data: | 30-Out-2017 |
Editora: | Association for Computing Machinery (ACM) |
Revista: | Proceedings of the ACM Conference on Computer and Communications Security |
Resumo(s): | Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and effciency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant. Using the supercop framework, we evaluate the Jasmin compiler on representative cryptographic routines and conclude that the code generated by the compiler is as efficient as fast, hand-crafted, implementations. Moreover, the framework includes highly automated tools for proving memory safety and constant-time security (for protecting against cache-based timing attacks). We also demonstrate the effectiveness of the verification tools on a large set of cryptographic routines. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/50513 |
ISBN: | 978-1-4503-4946-8 |
DOI: | 10.1145/3133956.3134078 |
ISSN: | 1543-7221 |
Versão da editora: | The original publication is available at https://dl.acm.org/citation.cfm?id=3134078 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
17CCSb.pdf | 778,14 kB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons