Automatic modular static safety checking for C programs
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
In this PhD thesis, we present automatic and modular solutions to the three main problems that come up when applying deductive verification techniques to C programs, in order to prove the absence of security flaws that exploit memory corruption. These problems are the generation of logical annotations, memory separation and the treatment of unions and casts. Deductive verification relies on the presence of logical annotations in programs. In practice, it is not possible to add all annotations manually. We propose a technique to generate such annotations based on abstract interpretation, weakest precondition calculus and quantifier elimination. When programs contain pointers, deductive verification is precise enough only if memory regions pointed-to are disjoint. We propose a technique to separate memory regions based on a contextual version of Steensgaard's alias analysis, whose correction is guaranteed by generating additional preconditions. When programs contain unions and casts, the usual hypothesis made in deductive verification that fields of structures are separated is not valid anymore. We propose a classification of unions and casts, as well as a combination of typed memory model and byte-level memory model, that validates the usual hypothesis of field separation. We have implemented these techniques in Frama-C and Why platforms. By applying them to the verification of existing libraries for strings, we both managed to find memory safety bugs in the original versions and to check the safety of corrected versions of the same libraries.
Abstract FR:
Cette thèse propose des solutions automatiques et modulaires aux trois problèmes principaux à résoudre pour appliquer les techniques de preuve déductive aux programmes C, dans le but de prouver l'absence de faille de sécurité exploitant une corruption mémoire. Ces problèmes sont la génération d'annotations logiques, la séparation mémoire et la prise en compte des unions et des casts. La preuve déductive repose sur la présence d'annotations logiques dans les programmes, qu'il n'est pas possible en pratique d'ajouter à la main en totalité. Nous proposons une méthode de génération d'annotations logiques basée sur les techniques d'interprétation abstraite, de calcul de plus faibles préconditions et d'élimination de quantificateurs. En présence de pointeurs, la preuve déductive n'est suffisamment précise que si les régions mémoires pointées sont disjointes. Nous proposons une méthode de séparation des régions mémoires basée sur une version contextuelle de l'analyse de Steensgaard, dont la correction est assurée par la génération de préconditions supplémentaires. En présence d'unions et de casts, les hypothèses habituelles de séparation entre champs de structures faites en preuve déductive ne sont plus valables. Nous proposons une classification des unions et des casts en C, ainsi qu'une articulation entre modèle mémoire typé et modèle mémoire bas-niveau qui permettent de retrouver les hypothèses habituelles de séparation. L'implantation de ces techniques dans les plate-formes Frama-C et Why a permis entre autre de trouver des bugs de sûreté mémoire et de vérifier les versions corrigées de bibliothèques existantes de chaînes de caractères.