LIP6 CNRS Sorbonne Université
Direct Link LIP6 » Actualité » Doctorants

PAROLINI Francesco

Doctorant
Équipe : APR
Date d'arrivée : 01/10/2020
Localisation : Campus Pierre et Marie Curie
    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

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.

 Mentions légales
Carte du site |