PAROLINI Francesco
Équipe : APR
Date d'arrivée : 01/10/2020
- Sorbonne Université - LIP6
Boîte courrier 169
Couloir 25-26, Étage 3, Bureau 303
4 place Jussieu
75252 PARIS CEDEX 05
Tel: 01 44 27 88 16, Francesco.Parolini (at) nulllip6.fr
https://lip6.fr/Francesco.Parolini
Direction de recherche : Antoine MINÉ
Analyse statique de propriétés de sécurité des logiciels par interprétation abstraite
Le but de cette thèse est le développement des méthodes sémantiques sûres d'analyse statique par interprétation abstraite pour les proprietés de sécurité.
L'analyse statique par interprétation abstraite a été appliquée avec succès à la vérification de propriétés de sûreté de fonctionnement, qui concernent essentiellement l'absence d'erreur à l'exécution. Toutefois, étendre ces méthodes à la vérification de propriétés plus complexes tout en ciblant les logiciels réalistes et en permettant le passage à l'échelle est une tâche difficile. Dans cette thèse, nous considérons une telle extension pour les propriétés de sécurité des programmes, qui sont particulièrement importantes dans l'industrie. Une première catégorie de propriété concernent les flots d'information, et la vérification qu'un utilisateur non autorisé ne peut pas accéder à des données privées. Les analyses existantes de type "coloration" (taint analysis) ignorent soit les flots implicites d'information, soit les valeurs précises des variables. Un axe de recherche consistera à faire bénéficier ces analyses des domaines abstraits de sûreté existants pour concevoir des analyses sûres et précises. Des extensions possibles consistent à formaliser et analyser le phénomène de déclassification, et d'inférer les fonctions de sanitation sans se reposer sur les informations fournies par l'utilisateur.
Afin de réduire le taux de fausses alarmes et d'améliorer l'information de l'analyseur, une piste de recherche consiste à considérer uniquement les erreurs exploitables par un attaquant. La thèse étudiera les liens entre cette nouvelle notion et le concept d'analyse de responsabilité proposée récemment par P. Cousot. Elle développera une formalisation sémantique de cette notion puis des abstractions permettant d'obtenir des analyses statiques sûres.
Publications 2022-2024
-
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)