An Abstract Domain for Bit-Vector Inequalities

Tushar Sharma, Aditya Thakur, and Thomas Reps
University of Wisconsin

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.)