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

Standard

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

Harvard

Kinder, J & Kravchenko, D 2012, Alternating Control Flow Reconstruction. in Proc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI 2012). Springer, pp. 267-282. https://doi.org/10.1007/978-3-642-27940-9_18

APA

Kinder, J., & Kravchenko, D. (2012). Alternating Control Flow Reconstruction. In Proc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI 2012) (pp. 267-282). Springer. https://doi.org/10.1007/978-3-642-27940-9_18

Vancouver

Kinder J, Kravchenko D. Alternating Control Flow Reconstruction. In Proc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI 2012). Springer. 2012. p. 267-282 https://doi.org/10.1007/978-3-642-27940-9_18

Author

Kinder, Johannes ; Kravchenko, Dmitry. / Alternating Control Flow Reconstruction. Proc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI 2012). Springer, 2012. pp. 267-282

BibTeX

@inproceedings{ab2d09ce9ee14b25b88fa549d68b3630,
title = "Alternating Control Flow Reconstruction",
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.",
author = "Johannes Kinder and Dmitry Kravchenko",
year = "2012",
month = jan,
doi = "10.1007/978-3-642-27940-9_18",
language = "English",
pages = "267--282",
booktitle = "Proc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI 2012)",
publisher = "Springer",

}

RIS

TY - GEN

T1 - Alternating Control Flow Reconstruction

AU - Kinder, Johannes

AU - Kravchenko, Dmitry

PY - 2012/1

Y1 - 2012/1

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

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

U2 - 10.1007/978-3-642-27940-9_18

DO - 10.1007/978-3-642-27940-9_18

M3 - Conference contribution

SP - 267

EP - 282

BT - Proc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI 2012)

PB - Springer

ER -