Model Checking Pointer Safety in Compiled Programs

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.