Alternating Control Flow Reconstruction. / Kinder, Johannes; Kravchenko, Dmitry.

Proc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI 2012). Springer, 2012. p. 267-282.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published

Documents

Abstract

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.
Original languageEnglish
Title of host publicationProc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI 2012)
PublisherSpringer
Pages267-282
DOIs
Publication statusPublished - Jan 2012
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 17557948