More Web Proxy on the site http://driver.im/

Article

Interprocedural control flow reconstruction

Authors:

Andrea Flexeder,

Bogdan Mihaila,

Michael Petter,

Helmut SeidlAuthors Info & Claims

APLAS'10: Proceedings of the 8th Asian conference on Programming languages and systems

Pages 188 - 203

Published: 28 November 2010 Publication History

Abstract

In this paper we provide an interprocedural algorithm for reconstructing the control flow of assembly code in presence of indirect jumps, call instructions and returns. In case that the underlying assembly code is the output of a compiler, indirect jumps primarily originate from high-level switch statements. For these, our methods succeed in resolving indirect jumps with high accuracy. We show that by explicitly handling procedure calls, additional precision is gained at calls to procedures exiting the program as well as through the analysis of side-effects of procedures onto the local state of the caller. Our prototypical implementation applied to real-world examples shows that this approach yields reliable and meaningful results with decent efficiency.

References

[1]

DCC decompiler, http://www.itee.uq.edu.au/~cristina/dcc.html

[2]

IDAPro disassembler, http://www.hex-rays.com/idapro/

[3]

Sicherheitsgarantien Unter REALzeitanforderungen, http://www.sureal-projekt.org/

[4]

VoTUM, http://www2.in.tum.de/votum

[5]

Balakrishnan, G.: WYSINWYX: What You See Is Not What You eXecute. PhD thesis, University of Wisconsin, Madison, WI, USA (August 2007).

Digital Library

[6]

Balakrishnan, G., Reps, T.W.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221-239. Springer, Heidelberg (2006).

Digital Library

[7]

Brauer, J., King, A.: Automatic abstraction for intervals using boolean formulae. In: Static Analysis Symposium (SAS 2010), Perpignan, France. LNCS. Springer, Heidelberg (2010).

Digital Library

[8]

Cifuentes, C.: Reverse Compilation Techniques. Ph.D. thesis, Queensland University of Technology (July 1994).

[9]

Cifuentes, C., Emmerik, M.V.: Recovery of jump table case statements from binary code. Science of Computer Programming 40, 171-188 (2001).

Digital Library

[10]

Cifuentes, C., Simon, D., Fraboulet, A.: Assembly to high-level language translation. In: ICSM, pp. 228-237 (1998).

Digital Library

[11]

Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269-295. Springer, Heidelberg (1992).

Digital Library

[12]

Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise WCET determination for a real-life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 469-485. Springer, Heidelberg (2001).

Digital Library

[13]

Flexeder, A., Petter, M., Seidl, H.: Analysis of Executables for WCET Concerns. Technical Report TUM-I0838, Technische Universität München (2008).

[14]

Kinder, J., Veith, H.: Jakstab: A static analysis platform for binaries. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 423-427. Springer, Heidelberg (2008).

Digital Library

[15]

Kinder, J., Veith, H., Zuleger, F.: An abstract interpretation-based framework for control flow reconstruction from binaries. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 214-228. Springer, Heidelberg (2009).

Digital Library

[16]

Levine, J.R.: Linkers and Loaders. Morgan Kaufmann Publishers Inc., San Francisco (1999).

Digital Library

[17]

Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: 31st ACM Symp. on Principles of Programming Languages (POPL), pp. 330-341 (2004).

Digital Library

[18]

Myreen, M.O.: Formal verification of machine-code programs. PhD thesis, University of Cambridge (2008).

[19]

Ramon, F.B., Moore, E.: Methods and Applications of Interval Analysis (SIAM Studies in Applied and Numerical Mathematics) (Siam Studies in Applied Mathematics, 2). Soc. for Industrial & Applied Math. (1979).

Digital Library

[20]

Reps, T., Balakrishnan, G., Lim, J.: Intermediate-representation recovery from low-level code. In: PEPM 2006: Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, pp. 100-111 (2006).

Digital Library

[21]

Schwarz, B., Debray, S., Andrews, G.: Disassembly of executable code revisited. In: WCRE 2002: Proceedings of the Ninth Working Conference on Reverse Engineering (WCRE 2002), Washington, DC, USA, p. 45. IEEE Computer Society, Los Alamitos (2002).

Digital Library

[22]

Simon, A.: Splitting the control flow with boolean flags. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 315-331. Springer, Heidelberg (2008).

Digital Library

[23]

Sobek, S., Burke, K.: PowerPC Embedded Application Binary Interface (EABI): 32-Bit Implementation. Freescale Semiconductor (2004), http://www.freescale.com/files/32bit/doc/app_note/PPCEABI.pdf

[24]

Theiling, H.: Extracting safe and precise control flow from binaries. In: RTCSA 2000: Proceedings of the Seventh International Conference on Real-Time Systems and Applications, Washington, DC, USA, p. 23. IEEE Computer Society, Los Alamitos (2000).

Digital Library

[25]

Theiling, H.: Control Flow Graphs for Real-Time System Analysis. PhD thesis, Universität des Saarlandes (2003).

Cited By

Flexeder APetter MSeidl H(2011)Side-effect analysis of assembly codeProceedings of the 18th international conference on Static analysis10.5555/2041552.2041562(77-94)Online publication date: 14-Sep-2011
https://dl.acm.org/doi/10.5555/2041552.2041562
Reinbacher TBrauer JHorauer MSteininger AKowalewski S(2011)Past time LTL runtime verification for microcontroller binary codeProceedings of the 16th international conference on Formal methods for industrial critical systems10.5555/2037070.2037075(37-51)Online publication date: 29-Aug-2011
https://dl.acm.org/doi/10.5555/2037070.2037075
Reinbacher TBrauer JChakraborty SJerraya ABaruah SFischmeister S(2011)Precise control flow reconstruction using boolean logicProceedings of the ninth ACM international conference on Embedded software10.1145/2038642.2038662(117-126)Online publication date: 9-Oct-2011
https://dl.acm.org/doi/10.1145/2038642.2038662

Interprocedural control flow reconstruction
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Pushdown control-flow analysis for free
POPL '16

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Interprocedural Pointer Analysis in Goanna

Goanna is an industrial-strength static analysis tool used in academia and industry alike to find bugs in C/C++ programs. Unlike existing approaches, Goanna uses the off-the-shelf model checker NuSMV as its core analysis engine on a syntactic flow-...
Pushdown control-flow analysis for free
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

APLAS'10: Proceedings of the 8th Asian conference on Programming languages and systems

November 2010

456 pages

ISBN:364217163X

Editor:
Kazunori Ueda
Dept. of Computer Science and Engineering, Waseda University, Tokyo, Japan

Sponsors

AAFS: Asian Association for Foundation of Software
Shanghai Jiao Tong University: Shanghai Jiao Tong University

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 28 November 2010

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Flexeder APetter MSeidl H(2011)Side-effect analysis of assembly codeProceedings of the 18th international conference on Static analysis10.5555/2041552.2041562(77-94)Online publication date: 14-Sep-2011
https://dl.acm.org/doi/10.5555/2041552.2041562
Reinbacher TBrauer JHorauer MSteininger AKowalewski S(2011)Past time LTL runtime verification for microcontroller binary codeProceedings of the 16th international conference on Formal methods for industrial critical systems10.5555/2037070.2037075(37-51)Online publication date: 29-Aug-2011
https://dl.acm.org/doi/10.5555/2037070.2037075
Reinbacher TBrauer JChakraborty SJerraya ABaruah SFischmeister S(2011)Precise control flow reconstruction using boolean logicProceedings of the ninth ACM international conference on Embedded software10.1145/2038642.2038662(117-126)Online publication date: 9-Oct-2011
https://dl.acm.org/doi/10.1145/2038642.2038662

View Options

View options

Media

Figures

Other

Tables

View Table of Contents