A Reachability Predicate for Analyzing Low-Level Software

Share

Shaunak Chatterjee, Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), Braga, Portugal.
Outstanding Student Paper Award. Invited for special section submission to the International Journal on Software Tools for Technology Transfer (STTT).
[pdf] [bib]

Abstract: Reasoning about heap-allocated data structures such as linked lists and arrays is challenging. The reachability predicate has proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. Sound and precise analysis for such data structures becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software.
In this paper, we give a novel formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present preliminary experience with a prototype verifier on a set of illustrative C benchmarks.

Bibtex:

@inproceedings{tacas2007-clqr,
  author = {Shaunak Chatterjee and Shuvendu K. Lahiri and
    Shaz Qadeer and Zvonimir Rakamari\'c},
  title = {A Reachability Predicate for Analyzing Low-Level Software},
  booktitle = {Proceedings of the 13th International Conference on
    Tools and Algorithms for the Construction and Analysis of Systems
    (TACAS 2007)},
  series = {Lecture Notes in Computer Science},
  volume = {4424},
  publisher = {Springer},
  editor = {Orna Grumberg and Michael Huth},
  isbn = {978-3-540-71208-4},
  year = {2007},
  pages = {19--33}
}