MINDS @ UW-Madison

An Abstract Domain for Bit-Vector Inequalities

Show full item record


Reps, Thomas; Thakur, Aditya; Sharma, Tushar
University of Wisconsin-Madison Department of Computer Sciences
Apr 16, 2013
modular arithmetic; symbolic abstraction; domain combination; machine code; abstract interpretation
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.
Permanent link
Export to RefWorks 

Part of

Show full item record

Search and browse


Deposit materials

  1. Register to deposit in MINDS@UW
  2. Need deposit privileges? Contact us.
  3. Already registered? Have deposit privileges? Deposit materials.