Skip to main content
SpringerLink
Log in

Expression Reduction from Programs in a Symbolic Binary Executor

  • Conference paper
Model Checking Software (SPIN 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7976))

Included in the following conference series:

Abstract

Symbolic binary execution is a dynamic analysis method which explores program paths to generate test cases for compiled code. Throughout execution, a program is evaluated with a bit-vector theorem prover and a runtime interpreter as a mix of symbolic expressions and concrete values. Left untended, these symbolic expressions grow to negatively impact interpretation performance.

We describe an expression reduction system which recovers sound, context-insensitive expression reduction rules at run time from programs during symbolic evaluation. These rules are further refined offline into general rules which match larger classes of expressions. We demonstrate that our optimizer significantly reduces the number of theorem solver queries and solver time on hundreds of commodity programs compared to a default ad-hoc optimizer from a popular symbolic interpreter.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Appleby, A.: murmurhash3 (November 2012), http://sites.google.com/site/murmurhash

  2. Bansal, S., Aiken, A.: Binary translation using peephole superoptimizers. In: OSDI 2008, pp. 177–192 (2008)

    Google Scholar 

  3. Barrett, C., de Moura, L., Stump, A.: Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). Journal of Automated Reasoning 35(4), 373–390 (2005)

    Article  MATH  Google Scholar 

  4. Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI 2008, pp. 209–224 (2008)

    Google Scholar 

  5. Chipounov, V., Kuznetsov, V., Candea, G.: S2E: A Platform for In-vivo Multi-Path Analysis of Software Systems. In: ASPLOS 2011, pp. 265–278 (2011)

    Google Scholar 

  6. Church, A., Rosser, J.B.: Some Properties of Conversion. Transactions of the American Mathematical Society 39(3), 472–482 (1936)

    Article  MathSciNet  Google Scholar 

  7. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 System. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 76–87. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Davidson, J.W., Fraser, C.W.: Automatic generation of peephole optimizations. In: SIGPLAN Symposium on Compiler Construction, pp. 111–116 (1984)

    Google Scholar 

  9. Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Godefroid, P., Levin, M.Y., Molnar, D.: Automated whitebox fuzz testing. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 2008. The Internet Society (2008)

    Google Scholar 

  11. Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  12. Khurshid, S., Păsăreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation, pp. 342–376. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  14. Martignoni, L., McCamant, S., Poosankam, P., Song, D., Maniatis, P.: Path-exploration lifting: hi-fi tests for lo-fi emulators. In: ASPLOS 2012, pp. 337–348 (2012)

    Google Scholar 

  15. Massalin, H.: Superoptimizer: A look at the smallest program. In: ASPLOS-II, pp. 122–126 (1987)

    Google Scholar 

  16. Molnar, D., Li, X.C., Wagner, D.A.: Dynamic test generation to find integer bugs in x86 binary linux programs. In: Proceedings of the 18th Conference on USENIX Security Symposium, SSYM 2009, pp. 67–82 (2009)

    Google Scholar 

  17. Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: PLDI 2007, pp. 89–100 (2007)

    Google Scholar 

  18. Păsăreanu, C., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. STTT, 339–353 (2009)

    Google Scholar 

  19. Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: ESEC/FSE-13, pp. 263–272 (September 2005)

    Google Scholar 

  20. Sinha, N.: Symbolic program analysis using term rewriting and generalization. In: FMCAD 2008, pp. 19:1–19:9. IEEE Press, Piscataway (2008)

    Google Scholar 

  21. Song, D., Brumley, D., Yin, H., Caballero, J., Jager, I., Kang, M.G., Liang, Z., Newsome, J., Poosankam, P., Saxena, P.: BitBlaze: A New Approach to Computer Security via Binary Analysis. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 1–25. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Stanford University, USA

    Anthony Romano & Dawson Engler

Authors
  1. Anthony Romano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dawson Engler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Engineering, Vienna, University of Technology, Austria

    Ezio Bartocci

  2. Department of Computer Science, Stony Brook University, 11794-4400, Stony Brook, NY, USA

    C. R. Ramakrishnan

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Romano, A., Engler, D. (2013). Expression Reduction from Programs in a Symbolic Binary Executor. In: Bartocci, E., Ramakrishnan, C.R. (eds) Model Checking Software. SPIN 2013. Lecture Notes in Computer Science, vol 7976. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39176-7_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-39176-7_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-39175-0

  • Online ISBN: 978-3-642-39176-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation