An Abstract Domain for Bit-Vector Inequalities
Tushar Sharma, Aditya Thakur, and Thomas Reps
This paper advances the state of the art in abstract interpretation of
machine code. It tackles two of the biggest challenges in machine-code
analysis: (1) holding onto invariants about values in memory, and
(2)identifying affine-inequality invariants while handling overflow in
arithmetic operations over bit-vector data-types.
Most current approaches either capture relations only among registers
(and ignore memory entirely), or make potentially unsound assumptions
when handling memory. Furthermore, existing bit-vector domains are
able to represent either relational affine equalities or
non-relational inequalities (e.g., intervals).
The key insight to tackling both challenges is to define a new domain
combinator (denoted by V), called the view-product combinator. V
constructs a reduced product of two domains in which shared
view-variables are used to communicate information among the
domains. V applied to a non-relational memory domain and a relational
bit-vector affine-equality domain constructs the Bit-Vector
Memory-Equality Domain (BVME), a domain of bit-vector
affine-equalities over memory and registers. V applied to the BVME
domain and a bit-vector interval domain constructs the Bit-Vector
Memory-Inequality Domain, a domain of relational bit-vector
affine-inequalities over memory and registers.
(Click here to access the paper:
PDF.)
University of Wisconsin