Alix Trieu

I am currently a Postdoc since January 2019 working with Aslan Askarov in the Logic and Semantics group at 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.

• 2020
  • Formal Verification of a Constant-Time Preserving C Compiler.
    with Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte and David Pichardie.
    47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2020.
    Project page
• 2019
  • Verifying Constant-Time Implementations by Abstract Interpretation.
    with Sandrine Blazy and David Pichardie.
    Journal of Computer Security (JCS), 2019.
• 2018
  • Verifying Constant-Time Implementations in a Verified Compilation Toolchain.
    PhD Thesis, University of Rennes 1, France.
• 2017
  • Verifying Constant-Time Implementations by Abstract Interpretation.
    with Sandrine Blazy and David Pichardie.
    22nd European Symposium on Research in Computer Security (ESORICS), 2017.
    Project page
  • Verified Translation Validation of Static Analyses.
    with Gilles Barthe, Sandrine Blazy, Vincent Laporte and David Pichardie.
    30th IEEE Computer Security Foundations Symposium (CSF), 2017.
    Project page
• 2016
  • Formal verification of control-flow graph flattening.
    with Sandrine Blazy.
    5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), 2016.
    Project page
• 2015
  • Static conflict detection for a policy language.
    with Robert Dockins and Andrew Tolmach.
    Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA), 2015.