Binary Analysis based on Symbolic Execution and Reversible x86 Instructions

• Autorzy: Stoenescu T. , Stefanescu A. , Predut S. , Ipate F.

Identyfikatory

DOI

10.3233/FI-2017-1533

• Języki publikacji: EN

Abstrakty

EN

We present a binary analysis framework based on symbolic execution with the distinguishing capability to execute stepwise forward and also backward through the execution tree. It was developed internally at Bitdefender and code-named RIVER. The framework provides components such as a taint engine, a dynamic symbolic execution engine, and integration with Z3 for constraint solving. In this paper we will provide details on the framework and give an example of analysis on binary code.

Słowa kluczowe

EN

binary operations; elimination; mathematical models; information theory; binary codes

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 153, nr 1/2
• Strony: 105--124
• Opis fizyczny: Bibliogr.30 poz., rys., tab., wykr.

Twórcy

autor

Stoenescu T.

• Department of Computer Science, Bitdefender, Romania

autor

Stefanescu A.

• University of Bucharest, Department of Computer Science, Bucharest, Romania

autor

Predut S.

• University of Bucharest, Department of Computer Science, Bucharest, Romania

autor

Ipate F.

• University of Bucharest, Department of Computer Science, Bucharest, Romania

Bibliografia

• [1] DARPA U. Cyber Grand Challenge, 2016. URL http://cgc.darpa.mil.
• [2] King JC. Symbolic Execution and Program Testing. Commun. ACM, 1976;19(7):385–394. doi:10.1145/360248.360252.
• [3] Cadar C, Sen K. Symbolic execution for software testing: three decades later. Commun. ACM, 2013; 56(2):82–90. doi:10.1145/2408776.2408795.
• [4] Pasareanu CS, Visser W. A survey of new trends in symbolic execution for software testing and analysis. STTT, 2009;11(4):339–353. doi:10.1007/s10009-009-0118-1.
• [5] Cadar C, Godefroid P, Khurshid S, Pasareanu CS, Sen K, Tillmann N, Visser W. Symbolic execution for software testing in practice: preliminary assessment. In: Proc. of ICSE’11. ACM, 2011 pp. 1066–1071. doi:10.1145/1985793.1985995.
• [6] Schwartz EJ, Avgerinos T, Brumley D. All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In: Proc. of SP’10. IEEE, 2010 pp. 317–331. doi:10.1109/SP.2010.26.
• [7] Sen K, Marinov D, Agha G. CUTE: a concolic unit testing engine for C. In: Proc. of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM, 2005 pp. 263–272. doi:10.1145/1095430.1081750.
• [8] Cadar C, Dunbar D, Engler DR. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proc. of OSDI’08. USENIX Association, 2008 pp. 209–224. URL http://dl.acm.org/citation.cfm?id=1855741.1855756.
• [9] Tillmann N, De Halleux J. Pex: White Box Test Generation for .NET. In: Proc. of TAP’08, volume 4966 of LNCS. Springer, 2008 pp. 134–153. ISBN:3-540-79123-X 978-3-540-79123-2.
• [10] Li G, Ghosh I, Rajan SP. KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. In: Proc. of CAV’11, volume 6806 of LNCS. Springer, 2011 pp. 609–615.
• [11] Luckow KS, Pasareanu CS. Symbolic PathFinder v7. ACM SIGSOFT Software Engineering Notes, 2014;39(1):1–5. doi:10.1145/2557833.2560571.
• [12] Song D, Brumley D, Yin H, Caballero J, Jager I, Kang MG, Liang Z, Newsome J, Poosankam P, Saxena P. BitBlaze: A New Approach to Computer Security via Binary Analysis. In: Proc. of ICCIS’08, volume 5253 of LNCS. Springer, 2008 pp. 1–25. doi:10.1007/978-3-540-89862-7_1.
• [13] Cha SK, Avgerinos T, Rebert A, Brumley D. Unleashing Mayhem on Binary Code. In: Proc. of SP’12. IEEE, 2012 pp. 380–394. doi:10.1109/SP.2012.31.
• [14] Salwan J, Saudel F. Triton: A Dynamic Symbolic Execution Framework. In: Symposium sur la sécurité des technologies de l’information et des communications. SSTIC, 2015 pp. 31–54. URL http://triton.quarkslab.com.
• [15] David R, Bardin S, Ta TD, Mounier L, Feist J, Potet M, Marion J. BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis. In: Proc. of SANER’16. IEEE, 2016 pp. 653–656. doi:10.1109/SANER.2016.43.
• [16] Bitdefender. Top awards received by Bitdefender from independent evaluators, 2016. URL http://www.bitdefender.com/business/awards.html.
• [17] Stephens N, Grosen J, Salls C, Dutcher A, Wang R, Corbetta J, Shoshitaishvili Y, Kruegel C, Vigna G. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In: Proc. of NDSS’16. The Internet Society, 2016 pp. 1–16.
• [18] Bennett CH. Time/space trade-offs for reversible computation. Siam Journal on Computing, 1989;18:766–776. doi:10.1137/0218053.
• [19] Akgul T, III VJM. Assembly instruction level reverse execution for debugging. ACM Transactions on Software Engineering and Methodology, 2004;13(2):149–198. doi:10.1145/1018210.1018211
• [20] Stoenescu T, Stefanescu A, Predut S, Ipate F. RIVER: A Binary Analysis Framework Using Symbolic Execution and Reversible x86 Instructions. In: Proc. of FM’16, volume 9995 of LNCS. Springer, 2016 pp. 779–785. doi:10.1007/978-3-319-48989-6_50.
• [21] de Moura L, Bjørner N. Z3: An Efficient SMT Solver. In: Proc. of TACAS’08, volume 4963 of LNCS. Springer, 2008 pp. 337–340. ISBN:3-540-78799-2, 978-3-540-78799-0.
• [22] Clause JA, Li W, Orso A. Dytan: a generic dynamic taint analysis framework. In: Proc. of ISSTA’07. ACM, 2007 pp. 196–206. doi:10.1145/1273463.1273490.
• [23] Ciortea L, Zamfir C, Bucur S, Chipounov V, Candea G. Cloud9: a software testing service. Operating Systems Review, 2009;43(4):5–10. doi:10.1145/1713254.1713257.
• [24] Chipounov V, Kuznetsov V, Candea G. The S2E Platform: Design, Implementation, and Applications. ACM Trans. Comput. Syst., 2012;30(1):2. doi:10.1145/2110356.2110358.
• [25] Rizzi EF, Elbaum S, Dwyer MB. On the techniques we create, the tools we build, and their misalignments: A study of KLEE. In: Proc. of ICSE’16. ACM, 2016 pp. 132–143.
• [26] 9th Reversible Computation Conf., 2017. URL http://www.reversible-computation.org.
• [27] Lee J. Dynamic Reverse Code Generation for Backward Execution. Electr. Notes Theor. Comput. Sci., 2007;174(4):37–54. URL https://doi.org/10.1016/j.entcs.2006.12.028.
• [28] Sauciuc R, Necula G. Reverse Execution With Constraint Solving. Technical Report Tech report no. UCB/EECS-2011-67, University of California at Berkeley, 2011. URL http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-67.html.
• [29] Holzmann GJ. Backward Symbolic Execution of Protocols. In: Proc. of the IFIP WG6.1 Fourth International Workshop on Protocol Specification, Testing and Verification. North-Holland, 1985 pp. 19–30.
• [30] Gulwani S, Juvekar S. Bound Analysis using Backward Symbolic Execution. Technical Report Techreport no. MSR-TR-2009-156, Microsoft Research, 2009. URL http://www.bibsonomy.org/bibtex/255861b4395823c588d215c974ee6b0b0/fibso.