Vérification de programmes en code octet et ses applications
Institution:
NiceDisciplines:
Directors:
Abstract EN:
Program verification techniques based on programming logics and verification condition generators provide a powerful means to reason about programs. Whereas these techniques have very often been employed in the context of high-level languages in order to benefit from their structural nature. It is often required, especially in the context of mobile code, to prove the correctness of compiled programs. Thus it is highly desirable to have a means of bringing the benefits of source code verification to code consumers. We propose a mechanism that allows to transfer evidence from source programs to compiled programs. It builds upon a specification language for bytecode, a verification condition generator that operates on annotated programs, and a compiler that transforms source annotations into bytecode annotations. We show that the verification condition generator is sound, and that the proof bytecode level nearly coincides. We illustrate the benefits of oue framework in two case studies.
Abstract FR:
Les techniques de vérification basées sur les logiques de programmation ainsi que sur les générateurs de conditions de vérification permettent de raisonner de manière efficace sur les programmes. Bien que ces techniques aient souvent été utilisées avec des langages de haut niveau pour bénéficier de leurs structures, il est souvent nécessaire, plus spécifiquement dans le contexte du code mobile, de prouver la correction de programmes déjà compilés. C’est pourquoi il est très intéressant d’avoir un moyen pour utiliser la vérification de code source au niveau de l’utilisateur de code. Nous proposons un mécanisme qui permet de transférer des informations depuis le programme source vers le programme compilé. Il est construit autour d’un langage de spécification pour le code binaire, un générateur de conditions de vérification qui s’utilise sur des programmes annotés et un compilateur qui transforme les annotations au niveau du code source en des annotations au niveau du code binaire. Nous montrons que le générateur des conditions de vérification est correct et que les obligations de preuves au niveau du source et du code binaire sont presque les mêmes. Nous illustrons les bénéfices de notre démarche par deux études de cas.