Static Analysis

Static analysis is not the only way to verify universal (forall-paths) properties of programs: program verification can also be performed dynamically. As a recent milestone, we were able to prove, for the first time in 2013, attacker memory safety of an entire operating-system image parser, namely the ANI Windows image parser, using compositional exhaustive testing (implemented in the dynamic test generation tool SAGE and using the Z3 SMT solver), i.e., no static analysis whatsoever. However, several key verification steps were performed manually, and these verification results depend on assumptions regarding inputdependent loop bounds, fixing a few buffer-overflow bugs, and excluding some code parts that are not memory safe by design. This talk will discuss dynamic program verification, and its strengths and weaknesses. Higher-Order Model Checking: From Theory