Élagage d’invariants de programmes
Institution:
Rennes 1Disciplines:
Directors:
Abstract EN:
Cette thèse s'intéresse à l'obtention de certificats pour le Proof-Carrying Code qui soient à la fois petits et faciles à vérifier. Nous proposons des méthodes pour obtenir de petits témoins d'une propriété de sûreté dans le contexte de l'Abstraction-Carrying Code. Dans le cas distributif, le plus faible témoin (c'est à dire, le plus petit) peut être calculé. Dans le cas général, nous proposons une technique d'élagage pour affaiblir un témoin donné. Cette technique est appliquée au domaine abstrait des polyèdres convexes, dans le cas intraprocédural puis interprocéedural. Une autre application est présentée, qui permet d'enrichir la vérification « lightweight » de bytecode en incluant les appels de méthodes d'interfaces, sans compliquer le vérifieur. Nous présentons différents algorithmes de reconstruction qui généralisent les algorithmes de vérification existants. Enfin, pour faciliter l'utilisation des Binary Decision Diagrams en analyse statique (et donc pour l'Abstraction-Carrying Code), nous prouvons la correction d'une formulation relationnelle de la sémantique de plus petit point fixe des programmes logiques définis et "range-restricted''.
Abstract FR:
This thesis addresses the generation of certificates for Proof-Carrying Code that are both small and easy to check. We propose methods for obtaining small witnesses of a safety property in the context of Abstraction-Carrying Code. In the distributive case, the weakest witness (\emph{i. E. }, the smallest) may be computed. For the general case, we propose a pruning technique for weakening a given witness. This technique is applied to the abstract domain of convex polyhedra, in the intraprocedural and then interprocedural case. Another application is presented, which allows the lightweight bytecode verification to be enriched by including interface method calls, without making the checker more complex. We present various reconstruction algorithms which generalise existing checking algorithms. Finally, to facilitate the use of Binary Decision Diagrams in static analysis (and thus for Abstraction-Carrying Code), we prove the soundness of a relational formulation of the least fixpoint semantics of definite range-restricted logic programs.