June Rousseau — Ph.D Student in Computer Science

Biography

I am a Ph.D student in the Logic and Semantic team at Aarhus University (Denmark), under the supervision of Lars Birkedal and Jean Pichon. I am also a student at the Ecole Normale Supérieure Rennes (France). My Curriculum Vitae is available here.

I am interested in logic, software verification, and semantic of programming languages, in particular for application in security.

My research focuses on formal verification of CHERI-like capability machine. In particular, I am interested to bridge the gap between the formal model of Cerise and a more realistic machine.

Publications

See DBLP.

Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly, Maxime Legoupil, June Rousseau, Aina Linn Georges, Jean Pichon-Pharabod, Lars Birkedal, in OOPSLA 2024 [ pdf | doi ]

Research

Proving capability safety in the presence of indirect sentries

I gave be a presentation at POCL24, about extending Cerise with Indirect Sentries and the formal study we performed. The Coq implementation is available here. A technical report is available here.

Concurrent Cerise

Internship supervised by Lars Birkedal and Aïna-Linn Georges — Report and Slides

Cerise is a program logic implemented in the Coq proof assistant, built on top of the Iris separation logic framework. Cerise is able to prove strong properties of CHERI-like machine, involving interactions between known code and unknown, arbitrary code. Because real-world capability machines are complex, Cerise uses a model of a simplified single-core capability machine, with a small set of instructions. We propose Concurrent Cerise, a program logic for multi-core capability machine, with a sequentially consistent memory model and show that reasoning about the security properties is orthogonal to the concurrent behaviours.

Exercises to learn Cerise

Cerise is a framework to reason formally reason about programs running on capability machine. Cerise in mechanized in Coq. The extended journal paper gives a pedagogical approach of Cerise on paper. I designed some exercises to get familiar with the Coq implementation. Knowledge of using Iris in Coq are expected. The exercises sheet is available here. The Coq implementation of the exercises are available here. The solutions of the exercises are available on demand. Feel free to reach me out and ask any questions !

Past Research Experiences

I did a 4-months internship supervised by Sebastien Bardin and Lesly-Ann Daniel, and worked on optimization of Relation Symbolic Execution for Binsec/Rel.
I worked with Yannick Zakowski and proposed a DSL, CFLang, to simplify code generation. in the Vellvm Project. A report may be found here.

Contacts

Email: {firstname}.{lastname}[at]cs[dot]au[dot]dk
Github
GPG public key