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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Appleby, A.: murmurhash3 (November 2012), http://sites.google.com/site/murmurhash
Bansal, S., Aiken, A.: Binary translation using peephole superoptimizers. In: OSDI 2008, pp. 177–192 (2008)
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)
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)
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)
Church, A., Rosser, J.B.: Some Properties of Conversion. Transactions of the American Mathematical Society 39(3), 472–482 (1936)
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)
Davidson, J.W., Fraser, C.W.: Automatic generation of peephole optimizations. In: SIGPLAN Symposium on Compiler Construction, pp. 111–116 (1984)
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)
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)
Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)
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)
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)
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)
Massalin, H.: Superoptimizer: A look at the smallest program. In: ASPLOS-II, pp. 122–126 (1987)
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)
Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: PLDI 2007, pp. 89–100 (2007)
Păsăreanu, C., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. STTT, 339–353 (2009)
Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: ESEC/FSE-13, pp. 263–272 (September 2005)
Sinha, N.: Symbolic program analysis using term rewriting and generalization. In: FMCAD 2008, pp. 19:1–19:9. IEEE Press, Piscataway (2008)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)