Interprétation abstraite : application à la vérification et à l'analyses statique (48h, 6 ECTS)
Responsables : Patrick Cousot et Radhia Cousot
Lieu : École normale supérieure, Salle Samuel Beckett, 8h45-11h45
Plan du cours et intervenants (le cours commence le 2 Octobre 2009)
Fondements (Patrick Cousot)
Analyses statiques et vérification (Julien Bertrane, Radhia Cousot, Jérôme Feret, Antoine Miné)
Objectifs
L'analyse statique de programmes consiste à vérifier statiquement
(sans les exécuter) des propriétés dynamiques (à l'exécution) des
programmes.
Les classes de propriétés à vérifier sont très diverses comme la
sûreté (par exemple, absence d'erreurs à l'exécution), la
vivacité (par exemple, garantie de réponse à un signal), la
sécurité (par exemple, confidentialité d'informations traitées par
un programme), etc.
La grande difficulté pour démontrer automatiquement ces propriétés
dynamiques est de trouver les arguments inductifs pour faire la preuve
(par exemple, par induction sur le nombre de pas de calcul). Diverses
solution sont possibles : demander à l'utilisateur (méthodes
déductives), utiliser un modèle finitaire (vérification exhaustive)
ou calculer l'argument inductif par approximation de la sémantique du
programme (en utilisant les techniques d'approximation de point fixe
de l'interprétation abstraite).
Le cours explore cette dernière technique, en rappelle rapidement les
bases, afin d'explorer un certain nombre d'abstractions infinitaires
qui permettent de traiter un grand nombre d'applications à systèmes
d'états infinis, qu'elles soient émergentes, classiques ou
industrialisées.
Plan du cours (à titre indicatif)
Introduction à l'interprétation abstraite ;
Domaines abstraits numériques ;
Domaines abstraits symboliques ;
Combinaison et raffinement de domaines abstraits ;
Conception d'un analyseur statique par interprétation abstraite ;
Analyse statique de programmes séquentiels, procéduraux, récursifs, modularité ;
Domaines abstraits probabilistes ;
Vérification de la sécurité de protocoles cryptographiques ;
Estimation de la précision de logiciels numériques ;
Analyse statique de programmes paralléles asynchrones ;
Analyse statique de programmes distribués ;
Analyse statique de code mobile ;
Vérification de systèmes complexes intégrés sur puces ;
Vérification par abstraction paramétrée de prédicats ;
Vérifications statiques sur des logiciels critiques embarqués temps-réel ;
Sujets pratiques et théoriques ouverts en analyse statique par interprétation abstraite, perspectives.
Bibliographie
B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, X. Rival. A static analyzer for large safety-critical software. PLDI 2003, ACM Press, 2003, pp. 196-207.
P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303--342. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, USA, 1981.
P. Cousot. Verification by Abstract Interpretation. In International symposium on verification (theory & practice) celebrating Zohar Manna's 10000002-th birthday, N. Dershowitz (Ed.), vol. 2472 of Lecture Notes in Computer Science, Springer, Berlin, 2003.
J. Feret. Dependency Analysis of Mobile Systems. In European Symposium on Programming (ESOP'02). D. Le Métayer (Ed.), vol. 2305 of Lecture Notes in Computer Science, pp. 314--330, Springer, Berlin, 2002.
A. Miné. A Few Graph-Based Relational Numerical Abstract Domains. In Static Analysis Symposium SAS'02, M. Hermenegildo and G. Puebla (Eds.), LNCS 2477, 117--132, Springer 2002.
