Jasmin: High-assurance and high-speed cryptography

José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Arthur Blot; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira; Hugo Pacheco; Benedikt Schmidt; Pierre Yves Strub

doi:10.1145/3133956.3134078

Jasmin: High-assurance and high-speed cryptography

José Bacelar Almeida
, Manuel Barbosa
, Gilles Barthe
, Arthur Blot
, Benjamin Grégoire
, Vincent Laporte
, Tiago Oliveira
, Hugo Pacheco
, Benedikt Schmidt
, Pierre Yves Strub

École Polytechnique

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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.

Original language	English
Title of host publication	CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security
Publisher	Association for Computing Machinery
Pages	1807-1823
Number of pages	17
ISBN (Electronic)	9781450349468
DOIs	https://doi.org/10.1145/3133956.3134078
Publication status	Published - 30 Oct 2017
Event	24th ACM SIGSAC Conference on Computer and Communications Security, CCS 2017 - Dallas, United States Duration: 30 Oct 2017 → 3 Nov 2017

Publication series

Name	Proceedings of the ACM Conference on Computer and Communications Security
ISSN (Print)	1543-7221

Conference

Conference	24th ACM SIGSAC Conference on Computer and Communications Security, CCS 2017
Country/Territory	United States
City	Dallas
Period	30/10/17 → 3/11/17

Keywords

Constanttime security
Cryptographic Implementations
Safety
Verified Compiler

Access to Document

10.1145/3133956.3134078

Cite this

Almeida, J. B., Barbosa, M., Barthe, G., Blot, A., Grégoire, B., Laporte, V., Oliveira, T., Pacheco, H., Schmidt, B., & Strub, P. Y. (2017). Jasmin: High-assurance and high-speed cryptography. In CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (pp. 1807-1823). (Proceedings of the ACM Conference on Computer and Communications Security). Association for Computing Machinery. https://doi.org/10.1145/3133956.3134078

@inproceedings{9e7b42d3128042ad846e6c0146f4a7b8,

title = "Jasmin: High-assurance and high-speed cryptography",

abstract = "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.",

keywords = "Constanttime security, Cryptographic Implementations, Safety, Verified Compiler",

author = "Almeida, \{Jos{\'e} Bacelar\} and Manuel Barbosa and Gilles Barthe and Arthur Blot and Benjamin Gr{\'e}goire and Vincent Laporte and Tiago Oliveira and Hugo Pacheco and Benedikt Schmidt and Strub, \{Pierre Yves\}",

note = "Publisher Copyright: {\textcopyright} 2017 author(s).; 24th ACM SIGSAC Conference on Computer and Communications Security, CCS 2017 ; Conference date: 30-10-2017 Through 03-11-2017",

year = "2017",

month = oct,

day = "30",

doi = "10.1145/3133956.3134078",

language = "English",

series = "Proceedings of the ACM Conference on Computer and Communications Security",

publisher = "Association for Computing Machinery",

pages = "1807--1823",

booktitle = "CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security",

}

Almeida, JB, Barbosa, M, Barthe, G, Blot, A, Grégoire, B, Laporte, V, Oliveira, T, Pacheco, H, Schmidt, B & Strub, PY 2017, Jasmin: High-assurance and high-speed cryptography. in CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. Proceedings of the ACM Conference on Computer and Communications Security, Association for Computing Machinery, pp. 1807-1823, 24th ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, United States, 30/10/17. https://doi.org/10.1145/3133956.3134078

Jasmin: High-assurance and high-speed cryptography. / Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles et al.
CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, 2017. p. 1807-1823 (Proceedings of the ACM Conference on Computer and Communications Security).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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

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 -

Almeida JB, Barbosa M, Barthe G, Blot A, Grégoire B, Laporte V et al. Jasmin: High-assurance and high-speed cryptography. In CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery. 2017. p. 1807-1823. (Proceedings of the ACM Conference on Computer and Communications Security). doi: 10.1145/3133956.3134078

Jasmin: High-assurance and high-speed cryptography

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this