Jasmin
| Autor: | José B. Almeida, Gilles Barthe, Benedikt Schmidt, Pierre-Yves Strub, Benjamin Grégoire, Vincent Laporte, Hugo Pacheco, Tiago Oliveira, Arthur Blot, Manuel Barbosa |
|---|---|
| Přispěvatelé: | Institute for Systems and Computer Engineering, Technology and Science [Porto] (INESC TEC), Universidade do Minho = University of Minho [Braga], Universidade do Porto = University of Porto, Institute IMDEA Software [Madrid], École normale supérieure de Lyon (ENS de Lyon), Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), University of Minho [Braga], Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Universidade do Minho, Universidade do Porto, École normale supérieure - Lyon (ENS Lyon), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Gregoire, Benjamin |
| Rok vydání: | 2017 |
| Předmět: |
safety
Computer science 02 engineering and technology [INFO] Computer Science [cs] computer.software_genre cryptographic implementations verified compiler Software portability Software Compiler construction 0202 electrical engineering electronic engineering information engineering [INFO]Computer Science [cs] Implementation Memory safety Compiler correctness Cryptographic primitive business.industry Programming language Proof assistant 020207 software engineering Functional compiler Logic and verification 020201 artificial intelligence & image processing Compiler business computer Software security engineering constant- time security |
| Zdroj: | CCS CCS 2017-Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security CCS 2017-Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.1-17 |
| Popis: | International audience; 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 super-cop 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|