Follow
Alix Trieu
Title
Cited by
Cited by
Year
Formal verification of a constant-time preserving C compiler
G Barthe, S Blazy, B Grégoire, R Hutin, V Laporte, D Pichardie, A Trieu
Proceedings of the ACM on Programming Languages 4 (POPL), 1-30, 2019
1072019
Verifying constant-time implementations by abstract interpretation
S Blazy, D Pichardie, A Trieu
Journal of Computer Security 27 (1), 137-163, 2019
632019
Efficient and provable local capability revocation using uninitialized capabilities
AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, ...
Proceedings of the ACM on Programming Languages 5 (POPL), 1-30, 2021
322021
Formal verification of control-flow graph flattening
S Blazy, A Trieu
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016
232016
Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities
AL Georges, A Trieu, L Birkedal
Proceedings of the ACM on Programming Languages 6 (OOPSLA1), 1-30, 2022
132022
Verified translation validation of static analyses
G Barthe, S Blazy, V Laporte, D Pichardie, A Trieu
2017 IEEE 30th Computer Security Foundations Symposium (CSF), 405-419, 2017
112017
Proving full-system security properties under multiple attacker models on capability machines
T Van Strydonck, AL Georges, A Guéneau, A Trieu, A Timany, F Piessens, ...
2022 IEEE 35th Computer Security Foundations Symposium (CSF), 80-95, 2022
82022
Cerise: Program verification on a capability machine in the presence of untrusted code
AL Georges*, A Guéneau*, T Van Strydonck, A Timany, A Trieu*, ...
Journal of the ACM 71 (1), 1-59, 2024
72024
Cap’ou pas cap’?: Preuve de programmes pour une machine à capacités en présence de code inconnu
AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, D Devriese, ...
Journées Francophones des Langages Applicatifs 2021, 2021
62021
A generic framework to develop and verify security mechanisms at the microarchitectural level: application to control-flow integrity
M Baty, P Wilke, G Hiet, A Fontaine, A Trieu
2023 IEEE 36th Computer Security Foundations Symposium (CSF), 372-387, 2023
32023
Aide à la conception et vérification de spécifications formelles de protocoles cryptographiques
A Trieu, ARA Chatalic, B Tessiau, LSS Kachanovich
Univ. Rennes, Rennes, France, Tech. Rep 1, 2014
22014
33èmes journées francophones des langages applicatifs
C Keller, T Bourke, S Blazy, F Bour, G Bury, S Dumbrava, D Gallois-Wong, ...
2022
Mechanized Program Verification on a Capability Machine in Presence of Untrusted Code
AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, ...
2020
Verifying constant-time implementations in a verified compilation toolchain
A Trieu
Université de Rennes, 2018
2018
A Study on the Preservation of Cryptographic Constant-Time Security in the CompCert Compiler
A Trieu
2018
Semantic preservation of constant-time policies during compilation
V Laporte, D Pichardie, A Trieu, S Blazy
Program verification on a capability machine in presence of untrusted code
AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, ...
Toward Complete Stack Safety for Capability Machines
AL Georges, A Guéneau, A Trieu, L Birkedal
Cap’ou pas cap’?
AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, D Devriese, ...
32 ème Journées Francophones des Langages Applicatifs, 157, 0
Mechanized Reasoning about a Capability Machine
AL Georges, A Trieu, L Birkedal
The system can't perform the operation now. Try again later.
Articles 1–20