White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Model Checking Pointer Safety in Compiled Programs

Muehlberg, Jan Tobias (2009) Model Checking Pointer Safety in Compiled Programs. PhD thesis, University of York.

This is the latest version of this item.

[img] Text (PhD Thesis: Model Checking Pointer Safety in Compiled Programs, Jan Tobioas Muehlberg)
thesis.pdf
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (2751Kb)

Abstract

This thesis introduces a novel technique for the automated analysis of compiled programs, which is focused on, but not restricted to, pointer safety properties. Our approach, which we refer to as Symbolic Object Code Analysis (SOCA), employs bounded symbolic execution, and uses an SMT solver as execution and verification engine. Analysing the object code enables us to bypass limitations of other software model checkers with respect to the accepted input language, so that analysing code sections written in inline assembly does not represent a barrier for us. Our technique is especially designed for programs employing complex heap-allocated data structures and provides full counterexample paths for each error found. In difference to other verification techniques, our approach requires only a bare minimum of manual modelling efforts. While generating counterexamples is often impossible for static analysis techniques due to precision loss in join and widening operations, traditional model checking requires the manual construction of models or the use of techniques such as predicate abstraction which do not work well in the presence of heap-allocated data structures. Hence, symbolic execution is our method of choice over static analysis and model checking. We also present the SOCA Verifier as a prototypical implementation of our technique. We show that the SOCA Verifier performs competitively with state-of-the-art software model checkers with respect to error detection and false positive rates. Despite only employing path-sensitive and heap-aware program slicing, the SOCA Verifier is further shown to scale well in an extensive evaluation using 250 Linux device drivers. An in-depth case study on the Linux Virtual File System illustrates that the SOCA technique can be applied to verify program properties beyond pointer safety. Our evaluation testifies SOCA's suitability as an effective and efficient bug-finding tool.

Item Type: Thesis (PhD)
Keywords: model checking; symbolic execution; program slicing; case study; linux device drivers; linux virtual file system; object code analysis; soca
Academic Units: The University of York > Computer Science (York)
Depositing User: Jan Tobias Muehlberg
Date Deposited: 18 May 2010 10:45
Last Modified: 08 Aug 2013 08:44
URI: http://etheses.whiterose.ac.uk/id/eprint/841

Available Versions of this Item

  • Model Checking Pointer Safety in Compiled Programs. (deposited 18 May 2010 10:45) [Currently Displayed]

Actions (repository staff only: login required)