TY - GEN
T1 - Jasmin
T2 - 24th ACM SIGSAC Conference on Computer and Communications Security, CCS 2017
AU - Almeida, José Bacelar
AU - Barbosa, Manuel
AU - Barthe, Gilles
AU - Blot, Arthur
AU - Grégoire, Benjamin
AU - Laporte, Vincent
AU - Oliveira, Tiago
AU - Pacheco, Hugo
AU - Schmidt, Benedikt
AU - Strub, Pierre Yves
N1 - Publisher Copyright:
© 2017 author(s).
PY - 2017/10/30
Y1 - 2017/10/30
N2 - 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 efficiency 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.
AB - 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 efficiency 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.
KW - Constanttime security
KW - Cryptographic Implementations
KW - Safety
KW - Verified Compiler
UR - https://www.scopus.com/pages/publications/85041430933
U2 - 10.1145/3133956.3134078
DO - 10.1145/3133956.3134078
M3 - Conference contribution
AN - SCOPUS:85041430933
T3 - Proceedings of the ACM Conference on Computer and Communications Security
SP - 1807
EP - 1823
BT - CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security
PB - Association for Computing Machinery
Y2 - 30 October 2017 through 3 November 2017
ER -