Checking C Pointer Programs for Memory Safety

Yannick Moy 1, 2, *
* Auteur correspondant
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : We propose an original approach for checking memory safety of C pointer programs possibly including pointer arithmetic and sharing (but no casts, structures, double indirection or memory deallocation). This involves first identifying aliasing and strings, which we do in a local setting rather than through a global analysis as it is done usually. Our separation analysis in particular is a totally new treatment of non-aliasing. We present for the first time two abstract lattices to deal with local pointer aliasing and local pointer non-aliasing in an abstract interpretation framework. The key feature of our work is to combine abstract interpretation techniques and deductive verification. The approach is modular and contextual, thanks to the use of Hoare-style annotations (pre- and postconditions), allowing to verify each C function independently. Abstract interpretation techniques are used to automatically generate such annotations, in an idiomatic way: standard practice of C programming is identified and incorporated as heuristics. Abstract interpretation and deductive verification are both used to check these annotations in a sound way. Our first contribution is the design of an abstract domain for implications, which makes it possible to build efficient contextual analyses. Our second contribution is an efficient back-and-forth propagation method to generate contextual annotations in a modular way, in the framework of abstract interpretation. Thanks to previously unknown loop refinement operators, this propagation method does not require iterating around loops. We implemented our method in Caduceus, a tool for the verification of C programs, and successfully verified automatically the C standard string library functions.
Type de document :
Rapport
[Research Report] RR-6334, INRIA. 2007, pp.54
Liste complète des métadonnées

https://hal.inria.fr/inria-00181950
Contributeur : Rapport de Recherche Inria <>
Soumis le : jeudi 25 octobre 2007 - 10:42:02
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : mardi 21 septembre 2010 - 14:21:15

Fichier

RR-6334.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00181950, version 2

Citation

Yannick Moy. Checking C Pointer Programs for Memory Safety. [Research Report] RR-6334, INRIA. 2007, pp.54. 〈inria-00181950v2〉

Partager

Métriques

Consultations de la notice

198

Téléchargements de fichiers

83