abstract.tex

In the past few years, there has been increased interest in automating
the reverse engineering and verification of binary executable code. The
importance of this subject has been highlight by the growing relevance
of security, reliability and legacy code. Since dynamic analysis is of
limited use for whole-program analyses, there has been a renewed
enthusiasm for the development of automated static analyses, which can
prove a property holds over all paths of the program. The abstract
interpretation framework exists for exactly this purpose, and has been
widely adopted in both academic and industrial circles. Yet, since its
introduction in 1977, standard abstract interpretation is still
formulated as the least solution of a set of fixpoint equations.

The work in this thesis deviates from the standard approach to static
analysis, proposing that recent advances in decision procedures could be
leveraged to tackle the problem.  The thesis can be considered a survey
of the applications of Boolean satisfiability (SAT) and linear
optimisation to the problem of static analysis, specifically range
analysis of binary executable code. It is shown (with experimental
results) that SAT and linear optimisation are particularly well suited to
inferring ranges of register values which, amongst others, are
useful for control flow recovery and for detecting binary vulnerabilities,
such as buffer and heap overflows.