Alternating Control Flow Reconstruction

Unresolved indirect branch instructions are a major obstacle for statically reconstructing a control flow graph (CFG) from machine code. If static analysis cannot compute a precise set of possible targets for a branch, the necessary conservative over-approximation introduces a large amount of spurious edges, leading to even more imprecision and a degenerate CFG. In this paper, we propose to leverage under-approximation to handle this problem. We provide an abstract interpretation framework for control flow reconstruction that alternates between over- and under-approximation. Effectively, the framework imposes additional preconditions on the program on demand, allowing to avoid conservative over-approximation of indirect branches. We give an example instantiation of our framework using dynamically observed execution traces and constant propagation. We report preliminary experimental results confirming that our alternating analysis yields CFGs closer to the concrete CFG than pure over- or under-approximation.


Editor(s):
Kuncak, Viktor
Rybalchenko, Andrey
Published in:
Proc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI 2012), 267-282
Presented at:
13th Int. Conf. Verification, Model Checking, and Abstract Interpretation, Philadelphia, PA, January 22-24, 2012
Year:
2012
Publisher:
Berlin, Springer
ISBN:
978-3-642-27939-3
Keywords:
Laboratories:




 Record created 2011-11-05, last modified 2018-03-17

Postprint:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)