Skip to main content
SpringerLink
Log in

Recovering High-Level Conditions from Binary Programs

  • Conference paper
  • First Online:
FM 2016: Formal Methods (FM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9995))

Included in the following conference series:

Abstract

The need to get confidence in binary programs without access to their source code has pushed efforts forward to directly analyze executable programs. However, low-level programs lack high-level structures (such as types, control-flow graph, etc.), preventing the straightforward application of source-code analysis techniques. Especially, conditional jumps rely on low-level flag predicates, whereas they often encode high-level “natural” conditions on program variables. Most static analyzers are unable to infer any interesting information from these low-level conditions, leading to serious precision loss compared with source-level analysis. In this paper, we propose template-based recovery, an automatic approach for retrieving high-level predicates from their low-level flag versions. Especially, the technique is sound, efficient, platform-independent and it achieves very high ratio of recovery. This method allows more precise analyses and helps to understand machine encoding of conditionals rather than relying on error-prone human interpretation or (syntactic) pattern-based reasoning.

Work partially funded by ANR, grant 12-INSE-0002.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bjørner, D., Broy, M., Pottosin, I.V. (eds.) Formal Methods in Programming and Their Applications, vol. 735, pp. 128–141. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  2. Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24756-2_1

    Chapter  Google Scholar 

  3. Bardin, S., Delahaye, M., David, R., Kosmatov, N., Papadakis, M., Traon, Y.L., Marion, J.: Sound and quasi-complete detection of infeasible test requirements. In: ICST 2015, pp. 1–10. IEEE, Graz (2015)

    Google Scholar 

  4. Bardin, S., Herrmann, P.: Structural testing of executables. In: ICST 2008. IEEE, Los Alamitos (2013)

    Google Scholar 

  5. Balakrishnan, G., Reps, T.: DIVINE: DIscovering variables IN executables. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 1–28. Springer, Heidelberg (2007). doi:10.1007/978-3-540-69738-1_1

    Chapter  Google Scholar 

  6. Bardin, S., Herrmann, P., Leroux, J., Ly, O., Tabary, R., Vincent, A.: The BINCOA framework for binary code analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 165–170. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_13

    Chapter  Google Scholar 

  7. Bardin, S., Herrmann, P., Védrine, F.: Refinement-based CFG reconstruction from unstructured programs. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 54–69. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18275-4_6

    Chapter  Google Scholar 

  8. Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.J.: BAP: a binary analysis platform. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 463–469. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_37

    Chapter  Google Scholar 

  9. Brauer, J., King, A.: Transfer function synthesis without quantifier elimination. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 97–115. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19718-5_6

    Chapter  Google Scholar 

  10. Brauer, J., King, A.: Automatic abstraction for intervals using boolean formulae. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 167–183. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15769-1_11

    Chapter  Google Scholar 

  11. Blazy, S., Laporte, V., Pichardie, D.: Verified abstract interpretation techniques for disassembling low-level self-modifying code. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 128–143. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08970-6_9

    Google Scholar 

  12. Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 5–23. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24723-4_2

    Chapter  Google Scholar 

  13. Balakrishnan, G., Reps, T.W.: WYSINWYX: what you see is not what you eXecute. ACM Trans. Program. Lang. Syst. 36, 23:1–23:84 (2010)

    Google Scholar 

  14. Reinbacher, T., Brauer, J.: Precise control flow reconstruction using boolean logic. In: EMSOFT 2011. ACM (2011)

    Google Scholar 

  15. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Symposium on Principles of Programming Languages, POPL, pp. 238–252. ACM (1977)

    Google Scholar 

  16. Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Logic Comput. 2, 511–547 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  17. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31987-0_3

    Chapter  Google Scholar 

  18. Dullien, T., Porst, S.: REIL: a platform-independent intermediate representation of disassembled code for static code analysis. In: CanSecWest (2009). http://www.zynamics.com/downloads/csw09.pdf

  19. Djoudi, A., Bardin, S.: BINSEC: binary code analysis with low-level regions. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 212–217. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_17

    Google Scholar 

  20. David, R., Bardin, S., Ta, T.D., Feist, J., Mounier, L., Potet, M., Marion, J.: BINSEC/SE: a dynamic symbolic execution toolkit for binary-level analysis. In: SANER (2016)

    Google Scholar 

  21. Intel\(\textregistered \) 64 and IA-32 Architectures Software Developer’s Manual. Order Number: 32546

    Google Scholar 

  22. Kinder, J., Kravchenko, D.: Alternating control flow reconstruction. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 267–282. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27940-9_18

    Chapter  Google Scholar 

  23. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27, 573–609 (2015)

    Article  MathSciNet  Google Scholar 

  24. Kinder, J., Zuleger, F., Veith, H.: 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 (2008). doi:10.1007/978-3-540-93900-9_19

    Chapter  Google Scholar 

  25. Logozzo, F., Fähndrich, M.: On the relative completeness of bytecode analysis versus source code analysis. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 197–212. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78791-4_14

    Chapter  Google Scholar 

  26. Mycroft, A.: Type-based decompilation (or program reconstruction via type reconstruction). In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 208–223. Springer, Heidelberg (1999). doi:10.1007/3-540-49099-X_14

    Chapter  Google Scholar 

  27. Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2005). doi:10.1007/11609773_23

    Chapter  Google Scholar 

  28. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag New York, Inc., New York (1999)

    Book  MATH  Google Scholar 

  29. Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Signedness-agnostic program analysis: precise integer bounds for low-level code. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 115–130. Springer, Heidelberg (2012). doi:10.1007/978-3-642-35182-2_9

    Chapter  Google Scholar 

  30. https://samate.nist.gov/SARD/testsuite.php

  31. Sepp, A., Mihaila, B., Simon, A.: Precise static analysis of binaries by extracting relational information. In: WCRE 2011. IEEE, Los Alamitos (2011)

    Google Scholar 

  32. Yadegari, B., Johannesmeyer, B., Whitely, B., Debray, S.: A generic approach to automatic deobfuscation of executable code. In: SP 2015. IEEE (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CEA, LIST, Université Paris-Saclay, Gif-sur-Yvette, France

    Adel Djoudi & Sébastien Bardin

  2. Lix, École Polytechnique, CNRS, Université Paris-Saclay, 91128, Palaiseau, France

    Éric Goubault

Authors
  1. Adel Djoudi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sébastien Bardin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Éric Goubault
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Adel Djoudi .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, United Kingdom

    John Fitzgerald

  2. US Naval Research Laboratory, Washington, District of Columbia, USA

    Constance Heitmeyer

  3. ISTI-CNR, Pisa, Italy

    Stefania Gnesi

  4. University of Cyprus, Nicosia, Cyprus

    Anna Philippou

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Djoudi, A., Bardin, S., Goubault, É. (2016). Recovering High-Level Conditions from Binary Programs. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-48989-6_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-48988-9

  • Online ISBN: 978-3-319-48989-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation