Description
Date depot: 1 janvier 1900
Titre: Analyse statique modulaire précise par interprétation abstraite pour la preuve automatique de correction de programmes et pour l'inférence de contrats
Directeur de thèse:
Antoine MINE (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
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/
Doctorant.e: Journault Matthieu