Automatic modular static safety checking for C programs

Abstract

Cette these propose des solutions automatiques et modulaires aux trois problemes principaux a resoudre pour appliquer les techniques de preuve deductive aux programmes C, dans le but de prouver l'absence de faille de securite exploitant une corruption memoire. Ces problemes sont la generation d'annotations logiques, la separation memoire et la prise en compte des unions et des casts. La preuve deductive repose sur la presence d'annotations logiques dans les programmes, qu'il n'est pas possible en pratique d'ajouter a la main en totalite. Nous proposons une methode de generation d'annotations logiques basee sur les techniques d'interpretation abstraite, de calcul de plus faibles preconditions et d'elimination de quantificateurs. En presence de pointeurs, la preuve deductive n'est suffisamment precise que si les regions memoires pointees sont disjointes. Nous proposons une methode de separation des regions memoires basee sur une version contextuelle de l'analyse de Steensgaard, dont la correction est assuree par la generation de preconditions supplementaires. En presence d'unions et de casts, les hypotheses habituelles de separation entre champs de structures faites en preuve deductive ne sont plus valables. Nous proposons une classification des unions et des casts en C, ainsi qu'une articulation entre modele memoire type et modele memoire bas-niveau qui permettent de retrouver les hypotheses habituelles de separation. L'implantation de ces techniques dans les plate-formes Frama-C et Why a permis entre autre de trouver des bugs de surete memoire et de verifier les versions corrigees de bibliotheques existantes de chaines de caracteres.