MILLON Etienne

PhD graduated
Team : APR
Departure date : 09/30/2014

Supervision : Emmanuel CHAILLOUX

Co-supervision : ZENNOU Sarah

Security analysis of system code using static typing

Manipulating user-provided pointers in the kernel of an operating system can lead to security flaws if done in an incautious manner. We present an efficient system to detect and prevent this class of erroneous memory manipulation.
At the core of our approach is Safespeak, an imperative language that we equip with a qualified type system, where two kinds of pointers are distinguished: safe pointers, whose value is statically proved to be controlled by the kernel, and unsafe ones, whose value comes from userspace through run-time system calls. Dereferencing unsafe pointers is forbidden in a static manner by the means of a strong type system.
A concrete case study is described based on a bug that affected a video driver in the Linux kernel. We also explain a technique to automatically translate GNU C code to our core language, which will enable us to analyze larger fractions of the kernel in order to find similar vulnerabilities.

Defence : 07/10/2014 - 14h - Site Jussieu 25-26/105

Jury members :

Sandrine Blazy, IRISA [Rapporteur]
Pierre Jouvelot, MINES ParisTech [Rapporteur]
Gilles Muller, Université Pierre et Marie Curie
Vincent Simonet, Google
Emmanuel Chailloux, Université Pierre et Marie Curie
Sarah Zennou, Airbus Group Innovations
Olivier Levillain, ANSSI

2012-2014 Publications