Direction de recherche : Antoine MINÉ

Analyse statique de propriétés de sécurité des logiciels par interprétation abstraite

Cette thèse vise à développer et à mettre en œuvre des techniques formelles capable de prouver l’absence de vulnérabilités liées à la sécurité dans les systèmes logiciels. Nous concentrons notre attention sur deux cas notables: les attaques Déni de Service liées aux Expressions Régulières (ReDoS), et les erreurs à l’exécution qui peuvent être déclenchées par un attaquant. Pour chaque cas, nous étudions d’abord le cadre théorique pour caractériser précisément la vulnérabilité que nous considérons. Ensuite, nous développons des analyses sûres et automatiques, qui peuvent prouver l’absence de vulnérabilités sans requérir d’interaction ou d’annotations de l’utilisateur.
Les langages de programmation modernes fournissent souvent des fonctions permettant de manipuler les expressions régulières. Lorsqu’elles offrent une prise en charge de fonctionnalités avancées, l’algorithme de correspondance a une complexité en temps dans le pire des cas exponentielle: pour certaines expressions régulières dites vulnérables, un attaquant peut alors créer des chaînes ad hoc pour forcer le moteur de recherche d’expressions régulières à présenter un comportement exponentiel et ainsi réaliser une attaque ReDoS. Dans la première partie de cette thèse, nous proposons une nouvelle sémantique pour la procédure de correspondance des expressions régulières qui caractérise précisément le comportement des moteurs de recherche d’expressions régulières réels. En exploitant une telle caractérisation, nous définissons formellement les vulnérabilités ReDoS en termes de taille des arbres de correspondance. Ensuite, nous proposons une analyse sûre qui extrait une surapproximation de l’ensemble des mots pouvant entraîner un comportement exponentiel du moteur de recherche d’expressions régulières. Nous avons implémenté notre analyse dans un outil appelé RAT, et en le comparant à sept autres détecteurs sur un large ensemble de 74,669 expressions régulières, nous avons constaté que RAT est le seul détecteur à ne pas générer de faux négatifs. De plus, RAT est plus rapide, souvent de plusieurs ordres de grandeur, que la plupart des autres outils.
Les erreurs à l’exécution pouvant être déclenchées par un attaquant sont sensiblement plus dangereuses que d’autres, car elles entraînent non seulement un échec du programme, mais peuvent également être exploitées et conduire à des violations de sécurité. Dans la deuxième partie de cette thèse, nous concentrons notre attention sur le développement d’une technique capable de prouver l’absence d’erreurs à l’exécution pouvant être déclenchées par un attaquant. Nous introduisons une nouvelle propriété appelée non-exploitabilité, qui caractérise précisément l’ensemble des programmes dont la correction ne peut pas être altérée par un utilisateur externe. Ensuite, nous donnons une caractérisation alternative de la non-exploitabilité en termes de variables teintées (c’est-à-dire contrôlées par l’utilisateur). En nous appuyant sur cette caractérisation, nous proposons une analyse par interprétation abstraite qui combine une analyse sémantique de teinte avec une analyse numérique. Les invariants numériques déduits par le domaine numérique améliorent la précision de l’analyse de teinte. Pour démontrer l’utilité de notre technique, nous avons implémenté notre analyse pour un large sous-ensemble de C. Nous avons comparé l’analyseur original avec la version modifiée par la non-exploitabilité sur un grand ensemble de 77 programmes réels extraits du package Coreutils, auxquels nous avons ajouté 13,261 cas de tests issus de la suite de tests Juliet. Dans nos expériences, nous avons constaté que notre analyse peut systématiquement prouver que plus de 70% des alarmes soulevées par l’analyseur original ne sont pas exploitables.

Publications 2022-2024

• 2024
  • F. Parolini : “Static Analysis for Security Properties of Software by Abstract Interpretation”, soutenance de thèse, soutenance 26/06/2024, direction de recherche Miné, Antoine (2024)
  • R. Monat, M. Milanese, F. Parolini, J. Boillot, A. Ouadjaout, A. Miné : “Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)”, Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024, vol. 14572, Lecture Notes in Computer Science, Luxembourg City, Luxembourg, pp. 387-392, (Springer Nature Switzerland) (2024)
• 2023
  • F. Parolini, A. Miné : “Sound Abstract Nonexploitability Analysis”, (2023)
  • F. Parolini, A. Miné : “Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks (Extended Version)”, Science of Computer Programming, vol. 229, pp. 102960, (Elsevier) (2023)
• 2022
  • F. Parolini, A. Miné : “Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks”, (2022)