Marc Pegon - Analyse de programmes par interprétation abstraite

De Ensiwiki
Aller à : navigation, rechercher


Analyse de programmes par interprétation abstraite

Labo VERIMAG
Equipe Synchrone
Encadrants Matthieu.Moy@grenoble-inp.fr,David.Monniaux@imag.fr

Etudiant

Pegon Marc, Ingéniérie des Systèmes d'Information


Introduction

Les logiciels informatiques étant de plus en plus complexes, il est d'autant plus difficile d'en assurer la qualité. De plus, dans certains secteurs industriels comme l'avionique, certains logiciels sont intégrés dans des systèmes critiques, et doivent donc être particulièrement fiables.

Introduite pour la première fois en 1977 par Patrick Cousot, l'interprétation abstraite [1][3] fait partie des méthodes d'analyse statique, qui permettent d'obtenir des informations sur un programme sans l'exécuter réellement. Différents outils d'analyse de programmes utilisés dans l'industrie sont basés sur l'interprétation abstraite (mais combinent également d'autres méthodes d'analyse), comme Astrée [2] ou PolySpace.

Ma contribution est d'avoir écrit en C/C++ un analyseur simple de programmes C basé sur l'interprétation abstraite, à l'aide des outils de compilation de LLVM [5] et de la bibliothèque numérique Apron [4].

Eléments de prérequis

Interprétation abstraite

On considère les programmes où toutes les variables sont numériques. On cherche à prouver automatiquement des propriétés de sûreté sur les programmes, c'est-à-dire informellement des propriétés indiquant que « quelque chose de mauvais ne peut jamais se produire ». Par exemple « à la ligne 10 du programme, la variable x n'est jamais nulle » est une propriété de sûreté. Pour prouver qu'un programme ne viole pas cette propriété, il suffit de vérifier qu'aucune trace d'exécution ne permet d'atteindre l'état « à la ligne 10, x = 0 ».

L'idéal serait de pouvoir déterminer en chaque point du programme l'ensemble des valeurs prises par les variables. Mais en théorie (et a fortiori en pratique) ce problème est trop complexe. On a donc recours à une approximation (abstraction) des états du programme.

Par exemple, on peut calculer en chaque point du programme un intervalle de valeurs pour chaque variable x (qui contient l'ensemble des valeurs réellement prises par x en ce point). Pour cela, il suffit d'explorer tous les chemins d'exécution possibles en propageant les intervalles.

Analyse d'intervalles sur un programme sans boucle

Pour les programmes avec boucles, les chemins d'exécution sont infinis ; on parcourt le programme jusqu'à ce que les intervalles obtenus soient des invariants.

Dans le cas général, on n'obtient pas d'invariant en un nombre fini d'itérations, et on a donc recours à des opérateurs d'élargissement [6], qui, appliqués en tête des boucles, garantissent l'obtention d'invariants en temps fini. Informellement, ces opérateurs « extrapolent » des invariants d'après la variation des intervalles calculés. Par exemple si en un point de programme on calcule successivement les intervalles [2, 4] puis [2, 6], pour une variable, on peut proposer l'intervalle [2, +\infty] comme invariant potentiel.

Analyse d'intervalles sur un programme avec boucle, avec élargissement en tête de boucle. Les intervalles sont donnés pour x, avec une couleur différente par pas de calcul

Les invariants obtenus à l'aide d'élargissements étant généralement trop larges pour montrer des propriétés intéressantes, ceux-ci sont réduits après coup par un nouveau parcours du programme.

Analyse d'intervalles sur un programme avec boucle, avec élargissement puis réduction des intervalles. Les intervalles sont donnés pour x, avec une couleur différente par pas de calcul
Polyèdre 2D représentant un ensemble de valeurs possibles pour les variables x et y
Illustre les limitations du domaine des intervalles. On aimerait obtenir z=0



Nous avons utilisé l'approximation des intervalles pour illustrer le principe de l'interprétation abstraite, mais en pratique pour ce TER, nous avons travaillé sur des polyèdres convexes, qui donnent de meilleurs résultats. En effet, à l'inverse des intervalles, les polyèdres convexes permettent de représenter des relations entre les variables sous la forme d'inégalités linéaires (par exemple 2x + y \le 3 \wedge 2y - z \ge 5).

LLVM

On a utilisé les outils de compilations fournis par la bibliothèque LLVM pour convertir du code C en une représentation plus pratique pour l'analyse (bitcode LLVM). Typiquement, le programme est représenté par un graphe de flot contrôle dont :

  • les noeuds sont des blocs de base, c'est-à-dire une suite d'instructions s'exécutant toujours consécutivement (sans sauts)
  • les arcs représentent les sauts du programme
A gauche un programme C et à droite sa représentation sous forme d'un graphe de flot de contrôle

Apron

Apron est une bibliothèque permettant d'effectuer des calculs dans différents domaines abstraits, comme les intervalles ou les polyèdres convexes. Elle fait en réalité office d'interface entre plusieurs librairies de calcul~: elle fournit des fonctions génériques pour l'interprétation abstraite, indépendantes du domaine numérique.

Il suffit de préciser au départ sur quel domaine on décide de mener l'analyse, et Apron se chargera d'utiliser les fonctions de calcul appropriées. Par exemple, même si notre analyseur travaille à partir du domaine des polyèdres convexes, il suffit de changer une seule ligne de code dans le programme pour travailler à partir des intervalles, des octaèdres, etc.

L'avantage d'utiliser Apron est donc que si de nouveaux domaines abstraits, meilleurs que les polyèdres, sont mis au jour et intégrés à Apron, il n'y aura en pratique rien à changer pour que notre analyseur puisse les utiliser.

Travail réalisé

L'objectif de ce TER était d'écrire un analyseur de programmes C à l'aide de LLVM et Apron. Concrètement, l'analyseur calcule au niveau de chaque bloc (plus précisément en fin de bloc, juste avant le saut) un polyèdre, qui est une approximation supérieure des états possibles du programme au niveau de ce bloc.

Pour cela, l'analyse doit parcourir le graphe de flot de contrôle tant que les polyèdres calculés à la fin de chaque bloc (juste avant le saut) ne sont pas stabilisés. Nous donnons ci-desous une version simplifiée de l'algorithme appliqué au niveau des blocs pour mettre à jour ces polyèdres. La version complète ainsi que le détail du traitement des instructions du bitcode LLVM sont donnés dans le rapport.

Un bloc de base, ses prédécesseurs et ses successeurs



  • Affecter dans poly l'enveloppe convexe des polyèdres des blocs prédécesseurs de b (vide pour les prédécesseurs non visités)
  • Transformer poly en fonction des instructions de b
  • Si b est en tête de boucle alors
    • Elargir poly en fonction du polyèdre calculé lors de la dernière visite de b, prec_poly
  • Si poly est égal à prec_poly alors
    • Visiter les successeurs de b dont le polyèdre n'est pas stabilisé
  • Sinon
    • Visiter tous les successeurs de bb

L'analyseur s'arrête ainsi lorsque tous les polyèdres sont stabilisés. S'ensuit une phase de réduction des invariants obtenus, par un nouveau parcours du graphe de contrôle.

Conclusions

Nous avons montré qu'il était possible de réaliser un analyseur simple de programmes C par interprétation abstraite rapidement, en se basant sur les bons outils. L'analyseur produit présente certes un certain nombre de limitations :

  • Seules la fonction main est analysée
  • Seules les variables numériques entières sont gérées (et considérées comme des entiers non bornés de \mathbb{Z})
  • Pas d'analyse sur la mémoire (pointeurs, tableaux, ...)

Il permet tout de même de montrer des propriétés non triviales sur des programmes simples.

Références

[1] P. Cousot and R. Cousot. Abstract interpretation : a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, 1977. ACM Press, New York, NY.

[2] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. The ASTRÉE Analyser. In M. Sagiv, editor, Proceedings of the European Symposium on Programming (ESOP’05), volume 3444 of Lecture Notes in Computer Science, pages 21–30, Edinburgh, Scotland, April 2–10 2005.

[3] B. Jeannet. Partitionnement Dynamique dans l’Analyse de Relations Linéraires et Application à la Vérification de Programmes Synchrones. PhD thesis, Institut National Polytechnique de Grenoble, September 2000.

[4] B. Jeannet and A. Miné. Apron : A library of numerical abstract domains for static analysis. In Proc. of the 21th Int. Conf. on Computer Aided Verification (CAV 2009), volume 5643 of Lecture Notes in Computer Science, pages 661–667, Grenoble, France, June 2009. Springer.

[5] Chris Lattner and Vikram Adve. LLVM : A Compilation Framework for Lifelong Program Analysis & Transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO’04), Palo Alto, California, Mar 2004.

[6] David Monniaux. A minimalistic look at widening operators. Higher order and symbolic computation, 22(2) :145–154, dec 2009.

Documents additionnels