logo EDITE Sujets de doctorat

Analyse statique modulaire précise par interprétation abstraite pour la preuve automatique de correction de programmes et pour l'inférence de contrats

Sujet proposé par
Directeur de thèse:
Encadré par
Doctorant: Matthieu JOURNAULT
Unité de recherche UMR 7606 Laboratoire d'informatique de Paris 6

Domaine: Sciences et technologies de l'information et de la communication

Projet

L'interprétation abstraite [1] est une théorie générale de l'approximation des sémantiques de programmes. Une de ses applications importantes est le développement de méthodes d'analyse statique pour inférer automatiquement des propriétés des programmes. Par construction, les analyses statiques sont approchées, pour être efficaces, mais sûres ; il s'agit donc de calculer des abstractions sur-approximant l'ensemble des comportements du programme, pour que toute propriété prouvée dans l'abstrait soit vraie de toutes les exécutions du programme. Utilisée à l'origine pour des analyses rapides mais nécessitant peu de précision (par exemple des analyses permettant l'optimisation au sein des compilateurs), l'interprétation abstraite est maintenant utilisée pour vérifier formellement la sûreté des programmes. Cette théorie connaît une popularité croissante grâce à ses applications récentes à la conception d'outils effectifs de vérification utilisés dans l'industrie, comme les analyseurs Astrée [3], Polyspace Analyzer [5], Sparrow [7], Clousot [6], etc.

Afin d'être utile, un analyseur visant la vérification de programmes doit être précis, en limitant le nombre de fausses alarmes dues aux sur-approximations. Il doit également être automatique, et suffisamment efficace pour passer à l'échelle des programmes actuels, d'une taille de plusieurs dizaines de millions de lignes. Une solution au problème de l'efficacité est la création d'analyses modulaires [4], capables d'analyser le programme module (fonction, fichier, bibliothèque, etc.) par module, puis de combiner ces résultats pour obtenir l'analyse du programme complet. Une analyse modulaire permet également d'analyser une bibliothèque une seule fois, de manière isolée, puis de réutiliser cette analyse dans chaque client. Les analyseurs actuels ne sont généralement pas à la fois précis, automatiques et modulaires. Par exemple, l'analyseur Astrée [3] n'est pas modulaire : il analyse un code complet de façon monolithique, et réanalyse une fonction à chacun de ses contextes d'appel. Cela lui permet d'être très précis, mais il n'est efficace que sur des programmes où la pile d'appels est limitée. À l'opposé, il est possible d'élaborer un analyseur modulaire efficace en se limitant à des abstractions simples, comme par exemple une analyse d'intervalles (non relationnelle), sans information sur le contexte d'appel, mais ce type d'analyses génère de nombreuses fausses alarmes. Enfin, une analyse précise et modulaire est possible si l'utilisateur fournit explicitement l'interface formelle de chaque module. Le développement de ces interfaces sur des gros programmes a toutefois un coût élevé, et une méthode complètement automatique fonctionnant sur des programmes non annotés est bien plus désirable.

Le but de la thèse est donc le développement d'analyses modulaires efficaces ayant un degré d'automatisme et de précision équivalent aux analyses non-modulaires de l'état de l'art. Nous pourrons nous limiter dans un premier temps aux applications à la preuve d'absence d'erreur à l'exécution dans des programmes C, dont l'analyse non-modulaire est déjà bien maîtrisée, afin de se concentrer sur l'aspect modulaire.

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 Proc. of POPL’77, pages 238-252, 1977.

[2] P. Cousot. Abstracting induction by extrapolation and interpolation. In Proc. of VMCAI’2015, volume 8931 of LNCS, pages 19-42. Springer, 2015.

[3] J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, and X. Rival. Static analysis and verification of aerospace software by abstract interpretation. In AIAA Infotech@Aerospace, number 2010-3385 in AIAA, pages 1–38. AIAA (American Institute of Aeronautics and Astronautics), Apr. 2010.

[4] P. Cousot and R. Cousot. Modular Static Program Analysis, invited paper. In Proc of CC 2002, LNCS 2304, pp. 159–178, Springer.

[5] MathWorks. Polyspace embedded software verification. http://www.mathworks.com/products/polyspace/index.html

[6] F. Logozzo and M. Fähndrich. Code contracts. http://research.microsoft.com/en-us/projects/contracts

[7] K. Yi and al. Sparrow. http://ropas.snu.ac.kr/sparrow/

Enjeux

La travail de recherche consistera à développer de nouvelles techniques permettant l'analyse modulaire, automatique, sûre et précise des programmes, avec comme première application l'analyse des erreurs à l'exécution dans des programmes C. Le travail pourra explorer en particulier les pistes suivantes :

Domaines abstraits

Les domaines abstraits forment le cœur de toute interprétation abstraite [1]. Il s'agit d'ensembles de propriétés, avec un encodage mémoire, munis d'opérateurs sémantiques abstraits, et des algorithmes associés, permettant de simuler l'effet du programme sur la représentation abstraite. De nombreux domaines abstraits ont déjà été proposés (en particulier pour les propriétés numériques) ; néanmoins, leur utilisation dans le cadre d'une analyse modulaire pose de nouveaux défis. La tâche consiste donc à introduire des nouveaux domaines, mieux adaptés, permettant par exemple de :
  • raisonner de manière paramétrique vis à vis de l'environnement d'entrée, inconnu, ce qui nécessite l'emploi de domaines symboliques ;
  • représenter fidèlement un ensemble de contextes d'utilisation hétérogènes de la fonction, nécessitant l'emploi de domaines de propriétés disjonctives et de partitionnement ;
  • représenter des objets d'ordre supérieur, comme des fonctions ou des relations, au lieu de représenter des ensemble d'environnements.
  • Abstraction des contextes

    Une analyse modulaire peut être amenée à analyser une fonction isolée, sans aucune information sur son contexte d'appel. Néanmoins, une telle analyse peut s'avérer peu précise et inefficace car elle sur-approxime de manière grossière les états du programme en entrée de la fonction. La tâche consiste donc à développer des méthodes permettant d'inférer, avant l'analyse d'une fonction, des informations sur les contextes d'appel possibles. L'analyse permettrait, entre autre, d'éviter de confondre les appels corrects à la fonction et ceux, incorrects, générant une corruption de l'état du programme. De manière générale, elle pourrait guider le partitionnement utilisé lors de l'analyse de la fonction. Notons que l'analyse d'une fonction n'est valide que dans le cadre de son contexte abstrait ; un contexte trop large réduit la précision de l'analyse, mais un contexte trop restreint réduit la possibilité de réutiliser le résultat de l'analyse d'une fonction. La tâche a pour but le développement d'abstractions adéquates des contextes d'appel, et des méthodes d'extrapolation et de généralisation des contextes permettant d'augmenter la réutilisabilité des analyses de fonctions sans pour autant sacrifier la précision.

    Inférence de contrats et d'interfaces

    L'analyse des contextes d'appel réels d'une fonction n'est pas toujours possible. C'est par exemple le cas lors de l'analyse d'une bibliothèque en isolation, sans connaître le code du client. Néanmoins, l'analyse des fonctions de la bibliothèque en faisant l'hypothèse qu'aucune erreur ne se produit permet d'inférer des informations précieuses sur les contextes d'utilisation valides. La tâche aura donc pour but de développer une analyse de ces contextes inférés. Notons qu'il s'agit d'une analyse en arrière, partant d'une conclusion raisonnable (le programme ne fait pas d'erreur) pour en déduire des conditions suffisantes en entrée de la fonction. Une application importante est la génération automatique de contrats de fonctions et d'interfaces, évitant ainsi l'annotation manuelle des programmes.

    Stratégies d'itération inter-modules

    Idéalement une analyse modulaire permettrait de décomposer l'analyse d'un programme en l'analyse de ses modules, chaque module étant analysé une seule fois et en isolation. En réalité, l'analyse modulaire réduit, mais n'élimine pas le couplage entre les modules. Des dépendances peuvent provenir de l'analyse des contextes d'appel, ainsi que de la présence de procédures récursives. Celles-ci sont résolues classiquement en itérant les analyses de modules dans un ordre bien choisi, jusqu'à obtention d'un point fixe. La tâche a pour but de définir de nouvelles méthodes d'itération et de propagation des résultats d'analyse entre les modules. Par ailleurs, nous pourrons envisager le cas où les modules sont analysés, pour plus d'efficacité, de manière concurrente, sur une machine multi-cœurs ou dans le cadre d'un calcul distribué.

    Validation théorique et expérimentale

    Le projet mêlera des aspects théoriques et fondamentaux dans le domaine de l'interprétation abstraite, ainsi que des aspects appliqués : l'implantation des solutions retenues et l'expérimentation dans le cadre d'analyses statiques de programmes réels. Les méthodes développées devront être bien définies formellement, ainsi que prouvées correctes en utilisant le cadre théorique de l'interprétation abstraite. Elles devront être motivées par l'analyse de cas d'étude réels. Les méthodes feront l'objet d'une implantation logicielle qui sera une des bases de la plateforme MOPSA, une plateforme générale d'analyse statique en cours de développement.

    Impact

    Les résultats de cette thèse devraient aboutir au développement d'analyseurs statiques plus précis et plus efficaces, et permettre la vérification formelle de programmes qui ne peuvent pas être actuellement considérés par l'état de l'art. La thèse peut donc avoir un impact important sur l'amélioration de la sûreté de fonctionnement des logiciels.

    Remarques additionnelles

    La thèse est proposée dans le cadre du projet ERC MOPSA. Elle se déroulera dans le laboratoire LIP6 de l'UPMC, dans l'équipe APR, spécialisée en analyse de programmes.