Reachability analysis of rewriting for software verification
Analyse d'atteignabilité en réécriture pour la vérification de programmes
Résumé
This work is about proving safety properties on programs. Such proof can be done by showing that "forbidden" program states, violating the property, are unreachable. For proving this kind of properties, we propose a semi-automatic verification technique which attempts to combine some of the advantages of model-checking, abstract interpretation and interactive proof. This technique is based on so-called tree automata completion. Like model-checking, this technique automatically proves safety of finite systems and of some classes of infinite systems having a regular representation. Outside of those classes and like abstract interpretation, tree automata completion permits to safely and finitely over-approximate the behavior of infinite state systems. At last, when the approximations are too coarse, we propose ways to interactively refine them and, when possible, finish the proof. Tree automata completion is based on Term Rewriting Systems which are one of the core technique of automated deduction. We use them to model programs: a program configuration is a term and transitions between configurations are represented by rewrite rules. On those models, proving safety consists in achieving reachability analysis, i.e. proving that "forbidden" terms are unreachable by rewriting initial ones. Sets of reachable terms are represented using tree automata and effectively computed using tree automata completion. This technique has been used for the verification of cryptographic protocols (it is part of one of the AVISPA tools) and for the fast prototyping of static analysis of Java bytecode programs.
Ce travail s'intéresse à la preuve de propriétés de sûreté sur les programmes. Prouver de telles propriétés revient généralement à démontrer que les configurations critiques ne sont jamais atteintes lors de l'exécution du programme. Pour ces propriétés, nous proposons une technique de vérification semi-automatique qui tente de combiner les avantages du model-checking, interprétation abstraite et preuve interactive. Comme en model-checking, cette technique permet de prouver automatiquement des propriétés de sûreté sur les systèmes finis, ainsi que sur certaines classes de systèmes infinis ayant une présentation finie. En dehors de ces classes et comme en interprétation abstraite, notre technique permet d'approcher le comportement infini d'un système par une sur-approximation sûre. Enfin, lorsque les approximations sont trop grossières, il nous est possible d'intervenir manuellement sur la définition des approximations afin de les raffiner et, si cela est possible, de mener la preuve à son terme. Cette approche est basée sur les systèmes de réécriture qui sont un des outils centraux de la déduction automatique. Nous les utilisons comme formalisme pour représenter les programmes: une configuration de programme est représentée par un terme et les transitions entre configurations par des règles de réécriture. Sur de tels modèles, prouver la sûreté d'un programme revient à faire une analyse d'atteignabilité, c.-à-d. vérifier que les termes représentant les configurations critiques sont inatteignables par réécriture des termes initiaux. L'ensemble des termes atteignables est représenté par un automate d'arbre. La construction de cet automate est effectuée en utilisant un algorithme de complétion spécifique. Pour la définition des approximations, nous avons proposé deux langages spécifiques, l'un calqué sur la structure des automates et l'autre utilisant des équations sur les termes. Ce dernier permet, en particulier, d'estimer la précision des approximations construites par rapport à la réécriture modulo équations. Cette technique a été expérimentée pour la vérification de protocoles cryptographiques ainsi que pour le protoypage rapide d'analyses statiques de programmes Java byte code.
Loading...