Verifying the absence of vulnerabilities in executable programs (binaries) requires a precise static analysis that combines several abstract domains to infer targets of indirect jumps, bounds for array accesses, precise points-to information, etc. A particular challenge for such a complex analysis is the size of the input: Each source code line translates to several machine instructions; the semantics of a machine instruction, in turn, is expressed using several operations in an intermediate representation (IR), so that a code increase by a factor of 10 is not unusual. We show that applying a few classic program optimizations to this IR leads to a considerable size reduction and, thereby, to a faster analysis. Moreover, fusing several IR instructions also recovers some of the original high-level computation. As a consequence, fewer domains need to be implemented in the static analyzer to achieve the required level of precision. This work presents the front-end that generates and optimizes the IR. Additionally, we present a static analysis tool based on our IR that is used to measure the size and precision improvements.     «

Verifying the absence of vulnerabilities in executable programs (binaries) requires a precise static analysis that combines several abstract domains to infer targets of indirect jumps, bounds for array accesses, precise points-to information, etc. A particular challenge for such a complex analysis is the size of the input: Each source code line translates to several machine instructions; the semantics of a machine instruction, in turn, is expressed using several operations in an intermediate re...     »