Programming Languages for Cybersecurity at RIO 2025

The course is taught by Gilles Barthe and Santiago Arranz Olmos.

In this course we will show how to approach some security problems in a rigorous and principled way, using programming language theory. Some of the problems we will tackle are: reasoning about interaction with polynomial adversaries, relating highly optimized implementations with their corresponding specifications, and analyzing secret and public data flow of a program.

Our case study will be Jasmin, a language designed to implement high assurance high speed cryptography. Jasmin provides a detailed control of the assembly generated by the compiler, allowing for maximal optimization of cryptographic routines. The compiler is verified in Coq, guaranteeing that a Jasmin program and its compilation have equivalent behaviors.

From a Jasmin program, one may extract a model for the EasyCrypt proof assistant, which may be used to prove program properties such as cryptographic security. Additionally, Jasmin provides a safety checker to detect common mistakes such as out-of-bounds accesses and arithmetic errors.

Finally, we will show a type system that allows to compute the public and private information flow of a program, and how such information can be used to guarantee that a program does not reveal secret information, even in the presence of side channels and speculative execution.

The tutorial is available here. Please follow the README.md to install everything and have it ready for the course. Contact me at santiago [dot] arranz-olmos [at] mpi-sp [dot] org if you are having trouble with it.

UPDATE 2025-03-15: I added many comments and small fixes in the tutorial.

Formosa, EasyCrypt, and Jasmin; review of Hoare logic

Referenced material:

• Shai Halevi. A plausible approach to computer-aided cryptographic proofs. https://eprint.iacr.org/2005/181.
• Johannes Wikner, Daniël Trujillo, and Kaveh Razavi. 2023. Phantom: Exploiting Decoder-detectable Mispredictions. In 56th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO ’23), October 28-November 1, 2023, Toronto, ON, Canada. ACM, New York, NY, USA, § 13 pages. https://doi.org/10.1145/3613424.3614275.
• Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, and Yuval Yarom. 2024. Testing Side-channel Security of Cryptographic Implementations against Future Microarchitectures. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security (CCS '24). Association for Computing Machinery, New York, NY, USA, 1076–1090. https://doi.org/10.1145/3658644.3670319.

Relational Hoare Logic; relational properties; example HL proof in EC; Jasmin tutorial

Referenced material:

• G. Barthe, P. R. D'Argenio, and T. Rezk, "Secure information flow by self-composition," Mathematical Structures in Computer Science, vol. 21, no. 6, pp. 1207–1252, 2011. doi:10.1017/S0960129511000193.
• N Benton. Semantics of Program Analyses and Transformations. Lecture notes for the PAT Summer School. June 2005. https://nickbenton.name/patrevised.pdf.
• An introduction to relational program verification: https://software.imdea.org/~gbarthe/__introrelver.pdf.

Operational semantics; semantics with observations; constant-time

Referenced material:

• The Formal Semantics of Programming Languages by Glynn Winskel. https://doi.org/10.7551/mitpress/3054.001.0001.
• Software Foundations by Benjamin Pierce. https://softwarefoundations.cis.upenn.edu/lf-current/index.html.

Safety properties; functional correctness; forward and backward simulations; CT simulations; simulations with transformers

Referenced material:

• CompCert: compcert.org
• CakeML: cakeml.org
• Leroy, X. A Formally Verified Compiler Back-end. J Autom Reasoning 43, 363–446 (2009). https://doi.org/10.1007/s10817-009-9155-4.
• G. Barthe, B. Grégoire and V. Laporte, "Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”," 2018 IEEE 31st Computer Security Foundations Symposium (CSF), Oxford, UK, 2018, pp. 328-343, doi:10.1109/CSF.2018.00031.
• Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, and Vincent Laporte. 2025. Preservation of Speculative Constant-Time by Compilation. Proc. ACM Program. Lang. 9, POPL, Article 44 (January 2025), 33 pages. https://doi.org/10.1145/3704880.

You should have finished the reference implementation of Gimli during the course. Should you need help, or want the solutions, contact me for hints (or search more thoroughly).

Side-channel attacks:

• Yuval Yarom and Katrina Falkner. 2014. FLUSH+RELOAD: a high resolution, low noise, L3 cache side-channel attack. In Proceedings of the 23rd USENIX conference on Security Symposium (SEC'14). USENIX Association, USA, 719–732. eprint.iacr.org/2013/448.
• Dag Arne Osvik, Adi Shamir, and Eran Tromer. 2006. Cache attacks and countermeasures: the case of AES. In Proceedings of the 2006 The Cryptographers' Track at the RSA conference on Topics in Cryptology (CT-RSA'06). Springer-Verlag, Berlin, Heidelberg, 1–20. doi.org/10.1007/11605805_1.
• https://github.com/0xADE1A1DE/Mastik

You can submit your exam here: nce.mpi-sp.org/index.php/apps/forms/s/AEJFP3bHAs83wsxnLD39DjCn.