Skip to Main content Skip to Navigation
Reports

Checking C Pointer Programs for Memory Safety

Yannick Moy 1, 2, *
* Corresponding author
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.
Complete list of metadatas

https://hal.inria.fr/inria-00181950
Contributor : Rapport de Recherche Inria <>
Submitted on : Thursday, October 25, 2007 - 10:42:02 AM
Last modification on : Wednesday, October 14, 2020 - 3:41:40 AM
Long-term archiving on: : Tuesday, September 21, 2010 - 2:21:15 PM

File

RR-6334.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00181950, version 2

Collections

Citation

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

Share

Metrics

Record views

270

Files downloads

147