Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs
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.
Authors
- Lionel Blatter (ORCID: https://orcid.org/0000-0001-9058-2005)
- Bo‐Yin Yang (ORCID: https://orcid.org/0000-0002-9362-5282)
- José Bacelar Almeida (ORCID: https://orcid.org/0000-0003-0011-7455)
- Bow-Yaw Wang (ORCID: https://orcid.org/0000-0002-5757-545X)
- Pierre-Yves Strub (ORCID: https://orcid.org/0000-0002-8196-7875)
- Manuel Barbosa (ORCID: https://orcid.org/0000-0002-6848-5564)
- Gilles Barthe (ORCID: https://orcid.org/0000-0002-3853-1777)
- Tiago Oliveira (ORCID: https://orcid.org/0000-0001-7395-3070)
- Miguel Quaresma (ORCID: https://orcid.org/0009-0008-8350-6870)
- J. L. M. Duarte (ORCID: https://orcid.org/0000-0001-5236-260X)
- Benjamin Grégoire (ORCID: https://orcid.org/0000-0001-6650-9924)
- Ming-Hsien Tsai (ORCID: https://orcid.org/0009-0001-7621-7981)
- Gustavo Delerue (ORCID: https://orcid.org/0009-0005-6458-1419)
Institutions
- Institut national de recherche en sciences et technologies du numérique (FR)
- National Taiwan University of Science and Technology (TW)
- Universidade do Porto (PT)
- Max Planck Institute for Security and Privacy (DE)
- Centre Inria d'Université Côte d'Azur (FR)
- Fondation Sophia Antipolis (FR)
- INESC TEC (PT)
- Academia Sinica (TW)
- University of Minho (PT)
Publication Details
- Published
- 2025-11-19
- DOI
- https://doi.org/10.1145/3719027.3744814
- Primary Topic
- Cryptographic Implementations and Security
- Type
- article
- Field-Weighted Citation Impact
- 0.00