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.

2012-2014 Publications

• 2014
  • E. Millon : “Analyse de sécurité de logiciels système par typage statique, Application au noyau Linux”, thesis, defence 07/10/2014, supervision Chailloux, Emmanuel, co-supervision : Zennou, Sarah (2014)
  • P. Manoury, Ph. Baufreton, J.‑L. Dufour, E. Prun, E. Chailloux, G. Henry, F. Thibord, Ph. Wang, E. Millon : “Certification de l’assemblage de composants dans le développement de logiciels critiques”, Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'14), Paris, France, pp. 109-114 (2014)
• 2012
  • E. Millon : “Vérification de code système par typage statique, application au noyau Linux.”, 10^e Symposium sur la Sécurité des Technologies de l'Information et des Communications (SSTIC'12), Rennes, France (2012)