Santiago Arranz-Olmos

14 papers Journal 11Unranked 3
YearRankTypeTitle / Venue / Authors
2025 J jnl
(Dis)Proving Spectre Security with Speculation-Passing Style.
CoRR
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Xingyu Xie, Zhiyuan Zhang
2025 J jnl
Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code.
IACR Cryptol. ePrint Arch.
Santiago Arranz-Olmos, Gilles Barthe, Benjamin Grégoire, Jan Jancar, Vincent Laporte, Tiago Oliveira, Peter Schwabe
2025 J jnl
Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
Santiago Arranz-Olmos, Gilles Barthe, Benjamin Grégoire, Jan Jancar, Vincent Laporte, Tiago Oliveira, Peter Schwabe
2025 J jnl
Preservation of Speculative Constant-Time by Compilation.
Proc. ACM Program. Lang.
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
2025 — conf
Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants).
ASPLOS (2)
Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang
2025 J jnl
The Jasmin Compiler Preserves Cryptographic Security.
CoRR
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte, Paolo Torrini
2025 J jnl
Transparent Decompilation for Timing Side-Channel Analyses.
CoRR
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Sören van der Wall, Zhiyuan Zhang
2024 — conf
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt.
CRYPTO (2)
José Bacelar Almeida, Santiago Arranz-Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
2024 J jnl
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Santiago Arranz-Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
2024 J jnl
High-assurance zeroization.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
Santiago Arranz-Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
2024 J jnl
Preservation of Speculative Constant-time by Compilation.
IACR Cryptol. ePrint Arch.
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
2024 J jnl
Protecting cryptographic code against Spectre-RSB.
IACR Cryptol. ePrint Arch.
Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang
2023 J jnl
High-assurance zeroization.
IACR Cryptol. ePrint Arch.
Santiago Arranz-Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
2020 — conf
A formalisation of LEGv8 in Agda.
SBLP
Santiago Arranz-Olmos, Martín Fernández, Matías Steinberg, Alejandro Gadea, Emmanuel Gunther, Miguel Pagano