Alix Trieu

I am currently a Postdoc since January 2019 working with Aslan Askarov and Lars Birkedal in the Logic and Semantics group at the Department of Computer Science of Aarhus University.

Before that, I was a Ph.D student between January 2016 to December 2018 in the Celtique group at Inria/IRISA/Université de Rennes 1 in France under the supervision of Sandrine Blazy and David Pichardie.

My Ph.D thesis is on the verification of constant-time implementations in a verified compiler toolchain such as CompCert and Verasco.

Before that, in 2015, I did an intership supervised by Sandrine Blazy on program obfuscations, more specifically on the formal verification of control-flow graph flattening.

In 2014, I did an internship supervised by Robert Dockins and Andrew Tolmach at Portland State University on static conflict detection in a policy language using Why3.

Curriculum Vitæ (pdf)

Contact

E-mail: alix.trieu@cs.au.dk

Work Address:
Building 5341, Office 228
Department of Computer Science
Aarhus University
Åbogade 34
DK-8200 Aarhus N
Denmark

Publications

My publications on DBLP and Google Scholar.

• 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.
    48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2021.
    Preprint (.pdf)
  • Toward Complete Stack Safety for Capability Machines.
    Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Lars Birkedal.
    5th Workshop on Principles of Secure Compilation (PriSC), 2021.
    Preprint (.pdf)
  • Cap’ ou pas cap’ ? Preuve de programmes pour une machine à capacités en presence de code inconnu.
    Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal.
    Trente-deuxièmes Journées Francophones des Langages Applicatifs (JFLA), 2021.
    Preprint (.pdf)
• 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.
    47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2020.
    Preprint (.pdf)
  • Mechanized Reasoning about a Capability Machine.
    Aïna Linn Georges, Alix Trieu, Lars Birkedal.
    4th Workshop on Principles of Secure Compilation (PriSC), 2020.
    Preprint (.pdf)
• 2019
  • Verifying Constant-Time Implementations by Abstract Interpretation.
    Sandrine Blazy, David Pichardie, Alix Trieu.
    Journal of Computer Security (JCS), 2019.
• 2018
  • A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler.
    Alix Trieu.
    Workshop on Foundations of Computer Security (FCS), 2018.
    Preprint (.pdf)
  • Verifying Constant-Time Implementations in a Verified Compilation Toolchain.
    Alix Trieu.
    PhD Thesis, University of Rennes 1, France.
    Thesis (.pdf)
• 2017
  • Verifying Constant-Time Implementations by Abstract Interpretation.
    Sandrine Blazy, David Pichardie, Alix Trieu.
    22nd European Symposium on Research in Computer Security (ESORICS), 2017.
    Preprint (.pdf)
  • Verified Translation Validation of Static Analyses.
    Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu.
    30th IEEE Computer Security Foundations Symposium (CSF), 2017.
    Preprint (.pdf)
• 2016
  • Formal verification of control-flow graph flattening.
    Sandrine Blazy, Alix Trieu.
    5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), 2016.
    Preprint (.pdf)
• 2015
  • Static conflict detection for a policy language.
    Alix Trieu, Robert Dockins, Andrew Tolmach.
    Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA), 2015.