Title :
A non-convex abstract domain for the value analysis of binaries
Author :
Mattsen, Sven ; Wichmann, Arne ; Schupp, Sibylle
Author_Institution :
Hamburg Univ. of Technol., Hamburg, Germany
Abstract :
A challenge in sound reverse engineering of binary executables is to determine sets of possible targets for dynamic jumps. One technique to address this challenge is abstract interpretation, where singleton values in registers and memory locations are overapproximated to collections of possible values. With contemporary abstract interpretation techniques, convexity is usually enforced on these collections, which causes unacceptable loss of precision. We present a non-convex abstract domain, suitable for the analysis of binary executables. The domain is based on binary decision diagrams (BDD) to allow an efficient representation of non-convex sets of integers. Non-convex sets are necessary to represent the results of jump table lookups and bitwise operations, which are more frequent in executables than in high-level code because of optimizing compilers. Our domain computes abstract bitwise and arithmetic operations precisely and looses precision only for division and multiplication. Because the operations are defined on the structure of the BDDs, they remain efficient even if executed on very large sets. In executables, conditional jumps require solving formulas built with negation and conjunction. We implement a constraint solver using the fast intersection and complementation of BDD-based sets. Our domain is implemented as a plug-in, called BDDStab, and integrated with the binary analysis framework Jakstab. We use Jakstab´s k-set and interval domains to discuss the increase in precision for a selection of compiler-generated executables.
Keywords :
binary decision diagrams; concave programming; program diagnostics; reverse engineering; storage management; table lookup; BDDStab; abstract bitwise operation; arithmetic operation; binary analysis framework Jakstab; binary decision diagram; binary executable; compiler-generated executable; constraint solver; contemporary abstract interpretation technique; high-level code; memory location; nonconvex abstract domain; nonconvex sets; optimizing compiler; plug-in; registers; reverse engineering; table lookup; value analysis; Abstracts; Algorithm design and analysis; Assembly; Boolean functions; Concrete; Data structures; Registers;
Conference_Titel :
Software Analysis, Evolution and Reengineering (SANER), 2015 IEEE 22nd International Conference on
Conference_Location :
Montreal, QC
DOI :
10.1109/SANER.2015.7081837