A Generic Framework for Symbolic Execution:Theory and Applications
Un cadre générique pour exécution symbolique
Résumé
Symbolic execution is one of the most popular techniques used for analyzing programs. It has been used especially for test case generation, but there exist several other applications (e.g. program verification, program debugging, etc.).The doctoral thesis titled A language-independent approach for symbolic execution: theory and applications presents a generic framework for symbolic execution, where the genericity is given by the fact that this framework is based on formal definitions of programming languages. This is an advantage because symbolic execution is implemented at the level of the language definition and is not based on the syntax or on the compiler of a particular language. In this thesis, the symbolic execution framework is formally presented, using algebraic specifications. This allows proving some important properties of symbolic execution:Coverage: for each concrete execution there exists a corresponding symbolic execution on the same program (execution) path. Precision: for each symbolic execution there exists a concrete execution on the same program (execution) path.These two properties are important because, in the case in which, after analyzing a program, certain results are obtained about symbolic executions, they ensure that the results can be correctly transferred to the concrete executions. Moreover, because of these properties, the symbolic execution framework that we propose can be used for program verification.ContributionsThe major contributions of this doctoral thesis are:A formal framework for symbolic execution and an implementation thereof, based on the operational semantics of programming languages:on the theoretical side, we formally define programming languages and symbolic execution and then we prove formally the properties of Coverage and Precision;on the practical side, we present a prototype of this symbolic framework that is implemented on top of the K framework for language definitions and which is based on language transformations;Applications of symbolic execution in program verification:program verification based on Hoare logic, where we show how symbolic execution can be used to verify Hoare triples for a given programming language;program verification based on Reachability Logic, where we present an alternative proof system for Reachability Logic and an inference rule application strategy that allows to automate the checking of Reachability Logic formulae; for this proof system and for the proposed strategy, we have implemented a prototype and we have shown soundness (based on the soundness of the Reachability Logic proof system) and a form of weak completeness (for proving formulae to be false).
L’exécution symbolique représente l’une des techniques les plus populaires utilisées pour l’analyse des programmes. Elle a été employée notamment pour générer des tests de manière automatique ; en plus, elle comporte de nombreuses applications (ex. : la vérification des programmes, le dépannage des programmes, etc.).La thèse de doctorat qui porte le titre « Une approche indépendante du langage de l’exécution symbolique : théorie et applications » présente le cadre générique pour l’exécution symbolique, où le caractère générique est donné par le fait que ce cadre est fondé sur les définitions formelles des langages de programmation. Cela représente un avantage, parce que l’exécution symbolique est implémentée au niveau de la définition du langage de programmation et n’est pas fondée sur la syntaxe ou sur le compilateur d’un certain langage. Dans cette thèse, le cadre d’exécution symbolique est présenté formellement, en utilisant des spécifications algébriques. Cela permet la démonstration de certaines propriétés importantes de l’exécution symbolique :- Coverage : à chaque exécution concrète correspond une exécution symbolique sur le même chemin (d’exécution) du programme.- Precision : à chaque exécution symbolique correspond une exécution concrète sur le même chemin (d’exécution) du programme.Ces deux propriétés sont importantes parce que, au cas où l’on obtient certains résultats qui font référence aux exécutions symboliques, après avoir analysé un programme, elles aident à ce que les résultats puissent être transférés correctement aux exécutions concrètes. En plus, grâce à ces propriétés, le cadre d’exécution symbolique que nous proposons peut être utilisé pour la vérification des programmes.ContributionsLes contributions majeures de cette thèse de doctorat sont :1. Un cadre formel pour l’exécution symbolique et une implémentation de celui-ci, fondé sur la sémantique opérationnelle des langages de programmation :- dans la partie théorique, nous définissons formellement les langages de programmation et l’exécution symbolique ; ensuite, nous démontrons formellement les propriétés Coverage et Precision ;- dans la partie pratique, nous présentons un prototype de ce cadre symbolique, qui est implémenté dans l’environnement pour les définitions de langages K, et qui est fondé sur des transformations de langages ;2. Applications de l’exécution symbolique dans la vérification de programmes :- la vérification de programmes fondée sur la logique Hoare ; dans ce cadre, nous présentons la manière dont on peut utiliser l’exécution symbolique, afin de vérifier des triplets Hoare pour un langage de programmation donné ;- la vérification de programmes fondée sur Reachability Logic ; dans ce cadre, nous présentons un système de déduction alternatif à celui du Reachability Logic, tout comme une stratégie d’application des règles de déduction, qui puisse permettre l’automatisation de la vérification des formules du Reachability Logic ; pour ce système déductif et pour la stratégie proposée, nous avons implémenté un prototype et nous en avons démontré la consistance (fondée sur la consistance du système déductif de Reachability Logic) et une forme de complétude faible (afin de démontrer le caractère faux des formules).
Loading...