Vous êtes ici

Théorie des types pour l’analyse statique modulaire de programmes système

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
https://www.inria.fr/teams/tea
Directeur de thèse
Jean-Pierre Talpin
Co-directeur(s), co-encadrant(s)
David Pichardie
Contact(s)
Sujet de thèse
Descriptif

Etat de l'art

L'analyse statique est une technique de vérification de programme automatique capable de vérifier l'absence d’erreurs de programmation (débordement mémoire, débordement arithmétiques) traditionnellement appliquée sur des programmes impératifs (C, Java) au moyen d’outils comme Verasco, EVA, Astrée, qui ne sont cependant pas modulaire : l'ensemble d'un programme doit être vérifié afin que ses propriétés (flots de données, de contrôle) soient formellement déterminées.

 

Le typage par raffinement permet en principe d'associer une fonction, une procédure ou une variable à un type et une proposition logique (modulo théorie) décrivant précisément (raffinant) son domaine de définition ou/et la transformation opérée sur la mémoire. En ce sens, Frama-C implémente une notion de typage par raffinement (à minima) par la possibilité d’expliciter des assertions sur les pré- et post-conditions qui peuvent ensuite être, pour certaines, validées par analyse statique au moyen du plugin EVA, mais pas de manière modulaire.  Le typage par raffinement est principalement mis en œuvre dans deux langages de programmation fonctionnels : Liquid Haskell et F*.  Liquid Haskell supporte l’inférence la résolution de contraintes automatique (en logique conjonctive de 1er ordre). F* délègue la preuve de propriétés en logique propositionnelle à un solveur SAT et un démonstrateur de théorèmes (Coq).

 

Objectifs

L’objectif du projet est d’utiliser le typage par raffinement pour la vérification de programmes systèmes, écrits majoritairement en langage C.  Plutôt que de typer ainsi les programmes C directement, chose qui serait une tâche complexe (expérience de CSolve), nous voudrions typer les abstractions obtenues à partir de ceux-ci au moyen de l’analyseur statique certifié Verasco, de manière à trouver compromis entre précision (analyse statique) et modularité (typage).  L’introduction de types par raffinement pour typer les propriétés manipulées par un analyseur statique amène à considérer plusieurs verrous scientifiques :

  • Représenter uniformément le domaine sémantique dans lequel sont exprimés le sens des propriétés de l’analyseur et celui des types qui les caractérisent.
  • Définir une relation d’abstraction entre les propriétés de l’analyseur et le domaine des types par raffinement considéré : afin de prouver qu’un type représente bien, fidèlement ou abstraitement, une telle propriété.
  • A l’inverse, définir une relation de concrétisation d’un type par sa représentation formelle dans l’analyseur, en vue de l’utiliser en lieu et place du programme qu’il abstrait.
  • Prouver formellement ou certifier ces relation d’abstraction et de raffinement dans l’analyseur considéré
  • Mettre en œuvre et valider ces résultats de manière expérimentale, en vérifiant la sureté et la sécurité de programmes et librairies système d’un micro noyau.

 

Bibliographie

REFERENCES

  • [Verasco] Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie. A Formally Verified C Static Analyzer. Principles of Programming Languages. ACM, 2015
  • [Liquid Haskell] Patrick Rondon, Ming Kawaguci, Ranjit Jhala. Liquid types. Programming Language Design and Implementation. ACM, 2008
  • [F*] Swamy et al. Dependent Types and Multi-Monadic Effects in F*. Principles of Programming Languages. ACM, 2016
  •  [Frama-C] Frama-C : https://frama-c.com, 2018.
  • [Coq] The Coq proof assistant: https://coq.inria.fr, 2018.
  • [LIO] Deian Stefan, Alejandro Russo, David Mazieres, John C. Mitchell. Flexible Dynamic Information Flow Control in the Presence of Exceptions.  Journal of Functional Programming, 2017.
  • [CSolve] Patrick Rondon, Alexander Bakst, Ming Kawaguchi, and Ranjit Jhala. CSolve: Verifying C with Liquid Types. Computer-Aided Verification. Springer, 2012.
  • [RIOT] The friendly Operating System for the Internet of Things. https://riot-os.org, 2018.
  • [PIP] The PIP proto-kernel. http://pip.univ-lille1.fr, 2018.
  • [SeL4] The SeL4 micro-kernel. https://sel4.systems , 2018.
  • [Cogent] SeL4 proof measurements and estimations. https://ts.data61.csiro.au/projects/TS/pme.pml, 2018.

 

Mots clés: 
Analyse statique, interprétation abstraite, théorie des types dépendants, logique de séparation, modèles mémoire, langages système, langage C.
Lieu: 
IRISA - Campus universitaire de Beaulieu, Rennes