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.

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

Download (2751Kb)


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)
Identification Number/EthosID: uk.bl.ethos.516419
Depositing User: Jan Tobias Muehlberg
Date Deposited: 18 May 2010 10:45
Last Modified: 08 Sep 2016 12:15
URI: http://etheses.whiterose.ac.uk/id/eprint/841

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)