Alix Trieu

13 papers A 3B 1Journal 7Unranked 1
YearRankTypeTitle / Venue / Authors
2026 J jnl
Formally Verified Number-Theoretic Transform.
IACR Commun. Cryptol.
Alix Trieu
2024 J jnl
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.
J. ACM
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal
2023 A conf
A Generic Framework to Develop and Verify Security Mechanisms at the Microarchitectural Level: Application to Control-Flow Integrity.
CSF
Matthieu Baty, Pierre Wilke, Guillaume Hiet, Arnaud Fontaine, Alix Trieu
2022 J jnl
Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities.
Proc. ACM Program. Lang.
Aïna Linn Georges, Alix Trieu, Lars Birkedal
2022 A conf
Proving full-system security properties under multiple attacker models on capability machines.
CSF
Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese
2021 J jnl
Efficient and provable local capability revocation using uninitialized capabilities.
Proc. ACM Program. Lang.
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal
2020 J jnl
Formal verification of a constant-time preserving C compiler.
Proc. ACM Program. Lang.
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
2019 J jnl
Formal Verification of a Constant-Time Preserving C Compiler.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
2019 J jnl
Verifying constant-time implementations by abstract interpretation.
J. Comput. Secur.
Sandrine Blazy, David Pichardie, Alix Trieu
2018 — —
Verifying Constant-Time Implementations in a Verified Compilation Toolchain. (Vérification d'implémentations constant-time dans une chaîne de compilation vérifiée).
Alix Trieu
2017 A conf
Verified Translation Validation of Static Analyses.
CSF
Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu
2017 — conf
Verifying Constant-Time Implementations by Abstract Interpretation.
ESORICS (1)
Sandrine Blazy, David Pichardie, Alix Trieu
2016 B conf
Formal verification of control-flow graph flattening.
CPP
Sandrine Blazy, Alix Trieu