Analyse Statique de Types Algébriques et de Tableaux/Static Analysis of Algebraic Data Types and Arrays

Résumé :

Pour assurer l'absence d'erreurs dans les logiciels critiques, la vérification formelle peut s'appuyer sur des méthodes d'analyse statique, telle que l'interprétation abstraite, qui déduisent des propriétés sur les programmes à partir de leur code source.
Cependant, les domaines d'interprétation abstraite existants se concentrent majoritairement sur des programmes où les variables contiennent des nombres ou des pointeurs. Cette thèse étudie la possibilité de développer une interprétation abstraite
pour des langages de programmation où les variables contiennent des valeurs de types algébriques, ou des tableaux de telles valeurs.
Nous présentons une façon générique d'étendre les domaines numériques existants pour calculer des résumés du comportement entrée-sortie des fonctions manipulant des valeurs de types algébriques et des tableaux; pourvu que les types algébriques en question soient non-récursifs.
L'aspect entrée-sortie de notre analyse lui permet d'être modulaire, n'analysant qu'une seule fois chaque fonction. Un prototype de notre analyse pour les types algébriques (mais pas pour les tableaux) a été implémenté en OCaml et testé sur 43 exemples, dont certains inspirés du code du micro-noyeau seL4.

Abstract:
Strong security guarantees are needed for critical software. Formal methods, such as interactive theorem proving, provide such guarantees, but may require a significant amount of human effort. Other static analysis methods, such as abstract interpretation, allow to alleviate part of the human effort required by interactive theorem proving.
In this thesis, we look at how to develop a static analyser based on abstract interpretation for programs that manipulate both algebraic types and arrays, as some critical software do. The long-term goal being to integrate this abstract interpreters into a theorem prover.
Our analysis for algebraic types extends the already existing abstract numeric domains, by replacing their variables with pairs of a variable and an access path. This analysis has been proven correct on paper, and we have developed a prototype implementation in OCaml.
Our analysis for arrays extends an approach by segmentation that Cousot, Cousot and Logozzo introduced in 2011; but differs in three main ways: we allow for arrays to contain values from algebraic types, we are able to express relations between the array contents and other program variables, and we redefined segmentation pre-order so that concretisation is monotonic with respect to the pre-order.

Un pot suivra en salle Oléron

---------

ATTENTION dans le cadre du plan VIGIPIRATE : l’accès du public à cette soutenance est contraint à une inscription préalable obligatoire auprès de lydie [*] mabilinria [*] fr
L’accès ne sera pas autorisé sans inscription préalable. Par ailleurs, les visiteurs ne porteront ni bagage ni sac.