Resources cited in this volume

[Algehed and Bernardy 2019] Simple noninterference from parametricity. Maximilian Algehed, Jean-Philippe Bernardy. Proc. ACM Program. Lang. 3(ICFP): 89:1-89:22. 2019. https://doi.org/10.1145/3341693 [Algehed et al 2021] Dynamic IFC Theorems for Free! Maximilian Algehed, Jean-Philippe Bernardy, Catalin Hritcu. CSF 2021. 1-14. https://arxiv.org/abs/2005.04722 [Almeida et al 2020] The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub. IEEE Symposium on Security and Privacy. 2020. https://doi.org/10.1109/SP40000.2020.00028 [Arranz-Olmos et al 2025] Preservation of Speculative Constant-Time by Compilation. Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte. Proc. ACM Program. Lang. 9(POPL): 1293-1325. 2025. https://doi.org/10.1145/3704880 [Barthe et al 2019] System-Level Non-interference of Constant-Time Cryptography. Part I: Model. Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna. J. Autom. Reason. 63(1): 1-51. 2019. https://doi.org/10.1007/s10817-017-9441-5 [Barthe et al 2020] Formal verification of a constant-time preserving C compiler. Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu. Proc. ACM Program. Lang. 4(POPL): 7:1-7:30. 2020. https://doi.org/10.1145/3371075 [Barthe et al 2021] Structured Leakage and Applications to Cryptographic Constant-Time and Cost. Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya. ACM SIGSAC Conference on Computer and Communications Security (CCS). 2021. https://doi.org/10.1145/3460120.3484761 [Baumann et al 2025] FSLH: Flexible Mechanized Speculative Load Hardening. Jonathan Baumann, Roberto Blanco, Léon Ducruet, Sebastian Harwig, and Cătălin Hrițcu. IEEE Computer Security Foundations Symposium (CSF). 2025. http://arxiv.org/abs/2502.03203 [Devriese and Piessens 2010] Noninterference through Secure Multi-execution. Dominique Devriese, Frank Piessens. IEEE Symposium on Security and Privacy. 2010. https://doi.org/10.1109/SP.2010.15 [Lau et al 2024] Specification and Verification of Strong Timing Isolation of Hardware Enclaves. Stella Lau, Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala. ACM SIGSAC Conference on Computer and Communications Security (CCS). 2024. https://doi.org/10.1145/3658644.3690203 [Molnar et al 2005] The Program Counter Security Model: Automatic Detection and Removal of Control-Flow Side Channel Attacks. David Molnar, Matt Piotrowski, David Schultz, and David Wagner. ICISC 2005. https://eprint.iacr.org/2005/368 [Ngo et al 2018] Impossibility of Precise and Sound Termination-Sensitive Security Enforcements. Minh Ngo, Frank Piessens, Tamara Rezk. IEEE Symposium on Security and Privacy. 2018. https://doi.org/10.1109/SP.2018.00048 [Sabelfeld and Myers 2003] Language-based information-flow security. Andrei Sabelfeld and Andrew C. Myers. IEEE Journal on Selected Areas in Communications 21 (1), 5-19. 2003. https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf [Shivakumar et al 2023] Spectre Declassified: Reading from the Right Place at the Wrong Time. B. A. Shivakumar, J. Barnes, G. Barthe, S. Cauligi, C. Chuengsatiansup, D. Genkin, S. O’Connell, P. Schwabe, R. Q. Sim, and Y. Yarom. IEEE Symposium on Security and Privacy. 2023. http://dx.doi.org/10.1109/SP46215.2023.10179355 [Volpano et al 1996] A Sound Type System for Secure Flow Analysis. Dennis M. Volpano, Cynthia E. Irvine, Geoffrey Smith. J. Comput. Secur. 4(2/3): 167-188. 1996. https://people.mpi-sws.org/~dg/teaching/lis2014/modules/ifc-1-volpano96.pdf [Volpano and Smith 1997] Eliminating Covert Flows with Minimum Typings. Dennis M. Volpano, Geoffrey Smith. Computer Security Foundations Workshop (CSFW). 1997. https://ifc-challenge.appspot.com/static/pdfs/csfw97.pdf [Zhang et al 2023] Ultimate SLH: Taking Speculative Load Hardening to the Next Level. Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom. USENIX Security Symposium. 2023. https://www.usenix.org/conference/usenixsecurity23/presentation/zhang-zhiyuan-slh