Direction de recherche : Emmanuel CHAILLOUX

Co-encadrement : ZENNOU Sarah

Analyse de sécurité de logiciels système par typage statique, Application au noyau Linux

Les noyaux de système d'exploitation manipulent des données fournies par les programmes utilisateur via les appels système. Si elles sont manipulées sans prendre une attention particulière, une faille de sécurité connue sous le nom de Confused Deputy Problem peut amener à des fuites de données confidentielles ou l'élévation de privilège d'un attaquant.
Le but de cette thèse est d'utiliser des techniques de typage statique afin de détecter les manipulations dangereuses de pointeurs contrôlés par l'espace utilisateur.
On commence par isoler un sous-langage sûr nommé Safespeak du langage C dans lequel sont écrits la plupart des systèmes d'exploitation. Sa sémantique opérationnelle et un système de types sont décrits, et les propriétés classiques de sûreté du typage sont établies.
On ajoute ensuite à Safespeak la notion de valeur provenant de l'espace utilisateur. La sûreté du typage est alors brisée, mais on peut la ré-établir en donnant un type particulier aux pointeurs contrôlés par l'espace utilisateur, ce qui force leur déférencement à se faire de manière contrôlée. Cette technique permet de détecter un bug qui a frappé un pilote de carte graphique AMD dans le noyau Linux.
Ces travaux ouvrent des perspectives sur deux points. Il est possible d'appliquer cette analyse à d'autres interfaces du noyau Linux qui communiquent avec l'espace utilisateur. De plus, cette technique revient à séparer l'interface des types de leur interface. Ce concept de types abstraits étant absent de C, de nombreuses erreurs de programmation peuvent également être vérifiées à l'aide de cette méthode.

Publications 2012-2014

• 2014
  • E. Millon : “Analyse de sécurité de logiciels système par typage statique, Application au noyau Linux”, thèse, soutenance 10/07/2014, direction de recherche Chailloux, Emmanuel, co-encadrement : 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)