Advising

2025 Mar 31st Martín Rodríguez (Licenciatura en Ciencias de la Computación, like a Master's degree)
Co-advised with Miguel Pagano at FaMAF.
"Detectar y explotar vulnerabilidades web con grandes modelos de lenguajes" (local copy).

Reviewing

2026 Jan 11th Reviewed for Principles of Secure Compilation (PriSC)

Other Activities

2026 Jun 8th Talk at GDR Sécurité Informatique
Presented "Formal Verification of Assembly-Level Side-Channel Security in Crypto Code."
Mar 9th Talk at Real World Crypto (RWC) (with Ignacio Cuevas)
Presented "End-to-End Formally Verified High-Assurance High-Speed Crypto Software."
2025 Oct 12th Jasmin tutorial at High-Assurance Systems Engineering (HASE)
Apr 3rd Conference talk at Architectural Support for Programming Languages and Operating Systems (ASPLOS)
Presented "Protecting Cryptographic Code Against Spectre-RSB."
Mar 13th Course at the RIO summer school (with Gilles)
One-week course "Programming Languages for Cybersecurity."
Mar 7th Lectures at FaMAF (with Gilles)
Two-week course "Foundations of Cybersecurity" for Bachelor's and Master's students.
Feb 19th Talk and Jasmin tutorial at Fing, Udelar (with Gilles)
See /pages/2025-02-19-fing.
Jan 20th Conference talk at Principles of Programming Languages (POPL)
Presented "Preservation of Speculative Constant-Time by Compilation" (recording).
Jan 20th Talk at Principles of Secure Compilation (PriSC)
Presented "Preservation of Speculative Constant-Time by Compilation."
2024 Sep 7th Conference talk at Cryptographic Hardware and Embedded Systems (CHES)
Presented "High-assurance zeroization" (recording).
Sep 4th Jasmin tutorial at Cryptographic Hardware and Embedded Systems (CHES)
Tutorial page.
Mar 22nd Jasmin tutorial at High-Assurance Crypto Software (HACS)
2023 Mar 31st Jasmin tutorial at High-Assurance Crypto Software (HACS)
2022 Jan 12th Jasmin tutorial at High-Assurance Crypto Software (HACS)

Publications (last updated 2026-08-17)

Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte, and Paolo Torrini. 2026. “KEM-IND-CCA-Preserving Compilation of Jasmin’s ML-KEM.” Proc. ACM Conference on Computer and Communications Security. To appear.
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Youcef Bouzid, Sören van der Wall, and Zhiyuan Zhang. 2026. “Decompiling for Constant-Time Analysis.” Proc. ACM Program. Lang., 10, OOPSLA1. DOI: 10.1145/3798201.
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Xingyu Xie, and Zhiyuan Zhang. 2026. “(Dis)Proving Spectre Security with Speculation-Passing Style.” Proc. ACM Program. Lang., 10, OOPSLA1. DOI: 10.1145/3798222.
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, 1293–1325. DOI: 10.1145/3704880.
Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, and Zhiyuan Zhang. 2025. “Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants).” Proc. ACM Conference on Architectural Support for Programming Languages and Operating Systems, 2, ASPLOS, 933–948. DOI: 10.1145/3676641.3716015.
Santiago Arranz-Olmos, Gilles Barthe, Benjamin Grégoire, Jan Jancar, Vincent Laporte, Tiago Oliveira, and Peter Schwabe. 2025. “Let’s DOIT: Using Intel’s Extended HW/SW Contract for Secure Compilation of Crypto Code.” IACR Trans. Cryptogr. Hardw. Embed. Syst., 2025, 3, 644–667. DOI: 10.46586/TCHES.V2025.I3.644-667.
Santiago Arranz-Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, and Peter Schwabe. 2024. “High-assurance zeroization.” IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024, 1, 375–397. DOI: 10.46586/TCHES.V2024.I1.375-397.
Santiago Arranz-Olmos, Martín Fernández, Matías Steinberg, Alejandro Gadea, Emmanuel Gunther, and Miguel Pagano. 2020. “A formalisation of LEGv8 in Agda.” Proc. Brazilian Symposium on Programming Languages, SBLP, 33–39. DOI: 10.1145/3427081.3427086.

Subpages