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.

Research

[NEW] Proving capability safety in the presence of indirect sentries

I will be giving 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. A technical report will be available soon. The slides from the POCL talk are 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 worked a few months with Thomas Genet on the integration of Timbuk4 to the OCaml interpreter. A report may be found here.
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.

School projects

A handful of my exciting school projects at university:

Formalization of System F type safety using a logical relation in Coq (check out the Github repository and the written report ! )

I am very excited about logical relations. For an introduction to logical relations, I recommend to read the OPLSS 2023 lecture notes of the logical course taught by Amal Ahmed, and An Introduction to Logical Relations - Lau Skorstengaard.

MyCSV: A DSL to manipulate CSV file
A compiler from a subset of C to a three-addresses like C code
A compiler from VSL+ to LLVM IR

Contacts

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