| Summary: | 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 b,een highlighted by the growing relevance of security, of reliability and of 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 serves this purpose and has been widely adopted in both academic and industrial circles. Yet, since its introduction in 1977, standard abstract interpretation has been 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 to be a survey of the application 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 can be used to infer ranges of register values which, amongst others, are useful for control flow recovery and for detecting binary vulnerabilities, such as buffer and heap overflows.
|
|---|
