Past Research Experience

Internship supervised by Yannick Zakowski — Report

Vellvm is a formalization in the Coq proof assistant of the LLVM IR, used to prove correct compilation passes, front-ends in particular. LLVM IR requires that the labels of the blocks of code constituting the CFG be unique. To simplify the code generation in Vellvm and optimizations on the control-flow graph, we present a design-specific language, CFLang, which ensures by construction the well-formedness of the generated graph. For each combinator, we provide their characteristic semantic equation and we illustrate the usability of our DSL by writing a compiler from IMP to VIR and validate the well-formedness of the generated code as well as its correctness.

Internship supervised by Sebastien Bardin and Lesly-Ann Daniel — Report available on demand

The constant-time property is a cryptographic property efficient to counter-measure timing attacks, a side-channel attack. Yet, constant-time programming is complex and is not always preserved by the compiler, therefore source code analysis is not sufficient. A solution is to analyze constant-time at binary level. Current state-of-the-art tools as Relational Symbolic Execution suffer of scaling issues at binary level. We propose an optimization of Relational Symbolic Execution which allows to spare SMT-solver calls for cryptographic code and a prototype implementation on the top of Binsec/Rel.

Supervised by Thomas Genet — Gitlab Repository — Report

Timbuk4 is a lightweight verification tool for functional program. It allows to non-expert developer to have a formal verification tool. I worked on the integration of Timbuk4 in the OCaml interpreter. Since OCaml language uses ordered pattern-matching, Timbuk4 uses unordered rewriting system. The aim of the project was to find a way to transform ordered pattern-matching into unordered rewriting system and to integrate this transformation into the OCaml interpreter.