Internships

DeepMind: Working on a Python JIT (March - August 2021)

I worked on JIT compiler for Python targeting x86_64 named S6 under the supervision of James Molloy. This is different from PyPy because S6 use the original CPython runtime and from the user point of view is just a plain library. Unfortunately, the project was cancelled due to a change in business priorities.

REMS: Translation validation infrastructure (Janury - July 2020)

I worked for 7 months with Peter Sewell on a translation validation project. The goal was to improve on the results about translation validation in the PhD thesis of Thomas Sewell by using DWARF debugging information. Translation validation is a technique to replace compiler verification. The goal is to verify that a single compilation of a program by checking (as automatically as possible) that the target (binary) program has the same semantics has the source program.

In my attempt to do that, I used the Isla symbolic evaluation engine to build up a system capable of executing entire C functions. I then added several simplification steps in order to run a custom assembly type system of the binary to propagate DWARF type information. I stopped there because of a lack of time.

EMSEC: side channels and binary analysis (September - December 2019)

I worked for three months with Clémentine Maurice and Sam Thomas to experiment with side-channel microarchitectural attacks and binary analysis.

During that time I experimented with dynamic binary analysis, to discover where common web server such as Apache and Nginx store HTTP Basic Auth passwords. This was done by instrumenting the Binary with Intel PIN. This was very interesting, because the instrumentation code, while in user-space, must still run in some kind of free-standing environment because it must not interact with the standard library use of the main program. Sometimes it is even worse, as I had no access to atomic and thus needed to roll my own (luckily TSO is not that hard a model to program with).

The other thing I then did is study the SmotherSpectre which is based on port contention across hyper-thread on Intel hardware. I try to see how to apply it to recover the password detected in the first half of the project. I wrote some kind of gadget detection software to try to detect automatically gadget usable for exploitation. Given the existence of techniques to break ASLR and my limited time, I work in a ASLR-less setting. I quickly, in the last weeks, tried to apply the technique with the detected gadgets, but although I had some statistically significant results (more than just randomness), the user would have need to enter their password more than a million time, to be able to learn a significant part of it, which make this attack infeasible in practice. The internship was still a very interesting experience.

Physics: experience in numerical computing, applied to physics (July 2019)

I did an internship with Igor Dotsenko and Pierre Rouchon to get both my bachelors in Maths and in physics by writing a thesis that double as an internship report. In physics worked with a quantum cavity electrodynamics that is featured in this paper. I mostly worked on the reconstruction of quantum states from statistical data obtained at the output of the experiment. This reconstruction involved fancy asymptotic integral evaluation that worked on with Pierre on the maths side.

SeL4: Fixing long standing issue (April - August 2018)

I worked 4 months at Trustworthy Systems on the SeL4 project supervised by Rafal Kolanski and Mattew Brecknell.

The goal of this internship was to fix a long standing issue in the SeL4 kernel where a specific system call named "Call" was forbidden between compartment by the security proof but was the main way of communication intended by the kernel team, and thus the only heavily optimized system call of the SeL4 kernel. I update the access right system (capabilities permission bits) to allow process to "Call" between compartment without actually relaxing any security property. I implement those new permission bits in C (only about 30 lines of C) and then repaired the proof of security (more than 8000 lines of Isabelle).

IMDEA: MPC verification attempt (June - July 2017)

TODO