Research

My research is at the intersection of security, programming languages and formal verification. Specifically, I am interested in investigating the gap between software and hardware. That is, how can one protect software from inherent hardware flawsSuch as side-channels., and how one can preserve software abstractions down to assembly.

Service

Program committee: PriSC24, JFLA22, NordSec19

Extended review committee: ECOOP23

Artifact evaluation committee: POPL21, ECOOP20

(Sub-)Reviewer: CC18, CPP18, VSTTE17, JAR, JCS, ACM TOPLAS, ACM TOPS

Publications

My publications on DBLP or Google Scholar.

In proceedings

• 2023
  • Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.
    Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal.
    Journal of the ACM (JACM).
    Preprint (.pdf) DOI Code
    
    
  • A Generic Framework to Develop and Verify Security Mechanisms at the Microarchitectural Level: Application to Control-Flow Integrity.
    Matthieu Baty, Pierre Wilke, Guillaume Hiet, Arnaud Fontaine, Alix Trieu.
    Computer Security Foundations Symposium (CSF23).
    Preprint (.pdf) DOI Code
• 2022
  • Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities.
    Aïna Linn Georges, Alix Trieu, Lars Birkedal.
    Object-oriented Programming, Systems, Languages, and Applications (OOPSLA22).
    🏆 Distinguished paper award.
    Preprint (.pdf) DOI Appendix (.pdf) Code
    
    
  • Proving Full-System Security Properties under Multiple Attacker Models on Capability Machines.
    Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese.
    Computer Security Foundations Symposium (CSF22).
    Preprint (.pdf) DOI
• 2021
  • Efficient and Provable Local Capability Revocation using Uninitialized Capabilities.
    Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal.
    Principles of Programming Languages (POPL21).
    Preprint (.pdf) DOI Code
• 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.
    Principles of Programming Languages (POPL20).
    Preprint (.pdf) DOI Artifact
• 2019
  • Verifying Constant-Time Implementations by Abstract Interpretation.
    Sandrine Blazy, David Pichardie, Alix Trieu.
    Journal of Computer Security (JCS).
    DOI
• 2017
  • Verifying Constant-Time Implementations by Abstract Interpretation.
    Sandrine Blazy, David Pichardie, Alix Trieu.
    European Symposium on Research in Computer Security (ESORICS17).
    Preprint (.pdf) DOI Code
    
    
  • Verified Translation Validation of Static Analyses.
    Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu.
    Computer Security Foundations Symposium (CSF17).
    Preprint (.pdf) DOI Code
• 2016
  • Formal verification of control-flow graph flattening.
    Sandrine Blazy, Alix Trieu.
    Certified Programs and Proofs (CPP16).
    Preprint (.pdf) DOI Code

Workshops

• 2021
  • Toward Complete Stack Safety for Capability Machines.
    Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Lars Birkedal.
    Workshop on Principles of Secure Compilation (PriSC21).
    Preprint (.pdf)
    
    
  • Cap’ ou pas cap’ ? Preuve de programmes pour une machine à capacités en présence de code inconnu.
    Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal.
    Journées Francophones des Langages Applicatifs (JFLA21).
    Preprint (.pdf) Code
• 2020
  • Mechanized Reasoning about a Capability Machine.
    Aïna Linn Georges, Alix Trieu, Lars Birkedal.
    Workshop on Principles of Secure Compilation (PriSC20).
    Preprint (.pdf)
• 2018
  • A Study on the Preservation of Cryptographic Constant-Time Security in the CompCert Compiler.
    Alix Trieu.
    Workshop on Foundations of Computer Security (FCS18).
    Preprint (.pdf)
• 2015
  • Static conflict detection for a policy language.
    Alix Trieu, Robert Dockins, Andrew Tolmach.
    Journées Francophones des Langages Applicatifs (JFLA15).

Theses

• 2018
  • Verifying Constant-Time Implementations in a Verified Compilation Toolchain.
    Alix Trieu.
    PhD Thesis, University of Rennes 1, France.
    Thesis (.pdf)