Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs

José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Lionel Blatter; Gustavo Delerue; João Diogo Duarte; Benjamin Gregoire; Tiago Oliveira; Miguel Quaresma; Pierre Yves Strub; Ming Hsien Tsai; Bow Yaw Wang; Bo Yin Yang

doi:10.1145/3719027.3744814

Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs

José Bacelar Almeida
, Manuel Barbosa
, Gilles Barthe
, Lionel Blatter
, Gustavo Delerue
, João Diogo Duarte
, Benjamin Gregoire
, Tiago Oliveira
, Miguel Quaresma
, Pierre Yves Strub
, Ming Hsien Tsai
, Bow Yaw Wang
, Bo Yin Yang

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

Abstract

Jasmin is a programming language for high-speed and high-assurance cryptography. Correctness proofs of Jasmin programs are typically carried out deductively in EasyCrypt. This allows generality, modularity and composable reasoning, but does not scale well for low-level architecture-specific routines. CryptoLine offers a semi-automatic approach to formally verify algebraically-rich low-level cryptographic routines. CryptoLine proofs are self-contained: they are not integrated into higher-level formal verification developments. This paper shows how to soundly use CryptoLine to discharge subgoals in functional correctness proofs for complex Jasmin programs. We extend Jasmin with annotations and provide an automatic translation into a CryptoLine model, where most complex transformations are certified. We also formalize and implement the automatic extraction of the semantics of a CryptoLine proof to EasyCrypt. Our motivating use-case is the X-Wing hybrid KEM, for which we present the first formally verified implementation.

Original language	English
Title of host publication	CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security
Publisher	Association for Computing Machinery, Inc
Pages	1409-1423
Number of pages	15
ISBN (Electronic)	9798400715259
DOIs	https://doi.org/10.1145/3719027.3744814
Publication status	Published - 22 Nov 2025
Externally published	Yes
Event	32nd ACM SIGSAC Conference on Computer and Communications Security, CCS 2025 - Taipei, Taiwan, Province of China Duration: 13 Oct 2025 → 17 Oct 2025

Publication series

Name	CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security

Conference

Conference	32nd ACM SIGSAC Conference on Computer and Communications Security, CCS 2025
Country/Territory	Taiwan, Province of China
City	Taipei
Period	13/10/25 → 17/10/25

Keywords

CryptoLine
EasyCrypt
Formal Verification
Jasmin

Access to Document

10.1145/3719027.3744814

Cite this

Almeida, J. B., Barbosa, M., Barthe, G., Blatter, L., Delerue, G., Duarte, J. D., Gregoire, B., Oliveira, T., Quaresma, M., Strub, P. Y., Tsai, M. H., Wang, B. Y., & Yang, B. Y. (2025). Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. In CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security (pp. 1409-1423). (CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security). Association for Computing Machinery, Inc. https://doi.org/10.1145/3719027.3744814

Almeida, José Bacelar ; Barbosa, Manuel ; Barthe, Gilles et al. / Jazzline : Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, Inc, 2025. pp. 1409-1423 (CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security).

@inproceedings{ca66101138b244eba1611965155a7406,

title = "Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs",

abstract = "Jasmin is a programming language for high-speed and high-assurance cryptography. Correctness proofs of Jasmin programs are typically carried out deductively in EasyCrypt. This allows generality, modularity and composable reasoning, but does not scale well for low-level architecture-specific routines. CryptoLine offers a semi-automatic approach to formally verify algebraically-rich low-level cryptographic routines. CryptoLine proofs are self-contained: they are not integrated into higher-level formal verification developments. This paper shows how to soundly use CryptoLine to discharge subgoals in functional correctness proofs for complex Jasmin programs. We extend Jasmin with annotations and provide an automatic translation into a CryptoLine model, where most complex transformations are certified. We also formalize and implement the automatic extraction of the semantics of a CryptoLine proof to EasyCrypt. Our motivating use-case is the X-Wing hybrid KEM, for which we present the first formally verified implementation.",

keywords = "CryptoLine, EasyCrypt, Formal Verification, Jasmin",

author = "Almeida, \{Jos{\'e} Bacelar\} and Manuel Barbosa and Gilles Barthe and Lionel Blatter and Gustavo Delerue and Duarte, \{Jo{\~a}o Diogo\} and Benjamin Gregoire and Tiago Oliveira and Miguel Quaresma and Strub, \{Pierre Yves\} and Tsai, \{Ming Hsien\} and Wang, \{Bow Yaw\} and Yang, \{Bo Yin\}",

note = "Publisher Copyright: {\textcopyright} 2025 Copyright held by the owner/author(s).; 32nd ACM SIGSAC Conference on Computer and Communications Security, CCS 2025 ; Conference date: 13-10-2025 Through 17-10-2025",

year = "2025",

month = nov,

day = "22",

doi = "10.1145/3719027.3744814",

language = "English",

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

publisher = "Association for Computing Machinery, Inc",

pages = "1409--1423",

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

}

Almeida, JB, Barbosa, M, Barthe, G, Blatter, L, Delerue, G, Duarte, JD, Gregoire, B, Oliveira, T, Quaresma, M, Strub, PY, Tsai, MH, Wang, BY & Yang, BY 2025, Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. in CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, Inc, pp. 1409-1423, 32nd ACM SIGSAC Conference on Computer and Communications Security, CCS 2025, Taipei, Taiwan, Province of China, 13/10/25. https://doi.org/10.1145/3719027.3744814

Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. / Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles et al.
CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, Inc, 2025. p. 1409-1423 (CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security).

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

TY - GEN

T1 - Jazzline

T2 - 32nd ACM SIGSAC Conference on Computer and Communications Security, CCS 2025

AU - Almeida, José Bacelar

AU - Barbosa, Manuel

AU - Barthe, Gilles

AU - Blatter, Lionel

AU - Delerue, Gustavo

AU - Duarte, João Diogo

AU - Gregoire, Benjamin

AU - Oliveira, Tiago

AU - Quaresma, Miguel

AU - Strub, Pierre Yves

AU - Tsai, Ming Hsien

AU - Wang, Bow Yaw

AU - Yang, Bo Yin

PY - 2025/11/22

Y1 - 2025/11/22

N2 - Jasmin is a programming language for high-speed and high-assurance cryptography. Correctness proofs of Jasmin programs are typically carried out deductively in EasyCrypt. This allows generality, modularity and composable reasoning, but does not scale well for low-level architecture-specific routines. CryptoLine offers a semi-automatic approach to formally verify algebraically-rich low-level cryptographic routines. CryptoLine proofs are self-contained: they are not integrated into higher-level formal verification developments. This paper shows how to soundly use CryptoLine to discharge subgoals in functional correctness proofs for complex Jasmin programs. We extend Jasmin with annotations and provide an automatic translation into a CryptoLine model, where most complex transformations are certified. We also formalize and implement the automatic extraction of the semantics of a CryptoLine proof to EasyCrypt. Our motivating use-case is the X-Wing hybrid KEM, for which we present the first formally verified implementation.

AB - Jasmin is a programming language for high-speed and high-assurance cryptography. Correctness proofs of Jasmin programs are typically carried out deductively in EasyCrypt. This allows generality, modularity and composable reasoning, but does not scale well for low-level architecture-specific routines. CryptoLine offers a semi-automatic approach to formally verify algebraically-rich low-level cryptographic routines. CryptoLine proofs are self-contained: they are not integrated into higher-level formal verification developments. This paper shows how to soundly use CryptoLine to discharge subgoals in functional correctness proofs for complex Jasmin programs. We extend Jasmin with annotations and provide an automatic translation into a CryptoLine model, where most complex transformations are certified. We also formalize and implement the automatic extraction of the semantics of a CryptoLine proof to EasyCrypt. Our motivating use-case is the X-Wing hybrid KEM, for which we present the first formally verified implementation.

KW - CryptoLine

KW - EasyCrypt

KW - Formal Verification

KW - Jasmin

UR - https://www.scopus.com/pages/publications/105023842262

U2 - 10.1145/3719027.3744814

DO - 10.1145/3719027.3744814

M3 - Conference contribution

AN - SCOPUS:105023842262

T3 - CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security

SP - 1409

EP - 1423

BT - CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security

PB - Association for Computing Machinery, Inc

Y2 - 13 October 2025 through 17 October 2025

ER -

Almeida JB, Barbosa M, Barthe G, Blatter L, Delerue G, Duarte JD et al. Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. In CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, Inc. 2025. p. 1409-1423. (CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security). doi: 10.1145/3719027.3744814

Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this