The Jasmin documentation
About Jasmin
Jasmin is a workbench for high-assurance and high-speed cryptography. Jasmin implementations aim at being efficient, safe, correct, and secure.
The Jasmin programming language smoothly combines high-level and low-level constructs, so as to support “assembly in the head” programming. Programmers can control many low-level details that are performance-critical: instruction selection and scheduling, what registers to spill and when, etc. They can also rely on high-level abstractions (variables, functions, arrays, loops, etc.) to structure their code and make it more amenable to formal verification.
The semantics is formally defined to allow rigorous reasoning about program behaviors.
The Coq definitions can be found in the proofs/lang/sem.v file.
This semantics is executable, thus Jasmin programs can be directly interpreted.
Jasmin programs can be automatically checked for safety and termination (using a trusted static analyzer).
The Jasmin compiler produces predictable assembly and ensures that the use of high-level abstractions incurs no run-time penalty.
It is formally verified for correctness (the precise Coq statement and the corresponding machine-checked proofs can be found in the proofs/compiler/compiler_proof.v file).
This justifies that many properties can be proved on a source program and still apply to the corresponding assembly program: safety, termination, functional correctness…
The Jasmin workbench leverages the EasyCrypt toolset for formal verification. Jasmin programs can be extracted to corresponding EasyCrypt programs to prove functional correctness, cryptographic security, or security against side-channel attacks (constant-time).
Language reference
Compiler
Tools
- How to compile a Jasmin program to assembly
- Easycrypt extraction
- Safety checker
- Constant-time programming
- Selective Speculative Load Hardening
- Selective Speculative Load Hardening (DRAFT)
- Background
- Spectre v1 (Bounds check Bypass) attack [brief]
- Speculative Load Hardening (SLH) [simplified]
- Constant-Time Programming
- Selective Speculative Load Hardening (in Jasmin)
- SLH v/s Selective SLH
- Misspeculation flag (MSF) states
- Jasmin primitives to perform SLH
- Annotations supported to perform selective SLH
- Things to consider
- Examples
- Additional examples and test cases
- Selective Speculative Load Hardening (DRAFT)
- How to execute the formal semantics
- How to pretty-print a Jasmin program
Bibliography
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub, “The Last Mile: High-Assurance and High-Speed Cryptographic Implementations,” 2020 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA, 2020, pp. 965-982, doi: 10.1109/SP40000.2020.00028.
José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, and Pierre-Yves Strub. 2019. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS ‘19). Association for Computing Machinery, New York, NY, USA, 1607–1622. DOI:10.1145/3319535.3363211
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS ‘17). Association for Computing Machinery, New York, NY, USA, 1807–1823. DOI:10.1145/3133956.3134078