Error detection in binary code with dynamic symbolic execution
https://doi.org/10.15514/ISPRAS-2022-34(2)-3
Abstract
Modern software is rapidly developing, revealing new program errors. More and more companies follow security development lifecycle (SDL). Fuzzing and symbolic execution are among the most popular options for supporting SDL. They allow to automatically test programs and find errors. Hybrid fuzzing is one of the most effective ways to test programs, which combines these two techniques. Checking security predicates during symbolic execution is an advanced technique, which focuses on solving extra constraints for input data to find an error and generate an input file to reproduce it. In this paper we propose a method for automatically detecting errors with the help of dynamic symbolic execution, combining hybrid fuzzing and checking security predicates. Firstly, we run hybrid fuzzing, which is required to increase number of corpora seeds. Then we minimize corpora. Thus, it would give the same coverage as the original corpora. After that we check security predicates on minimized corpora. Thus, security predicates allow to find errors like division by zero, out of bounds access, integer overflow, and more. Security predicates results are later verified with sanitizers to filter false positive results. As a result of applying the proposed method to different open source programs, we found 11 new different errors in 5 projects.
Keywords
About the Authors
Alexey Vadimovich VISHNYAKOVIvannikov Institute for System Programming of the RAS
Russian Federation
Works for the Compiler Technology Department, obtained BSc degree and M.D. in the Faculty of Computational Mathematics and Cybernetics at Lomonosov Moscow State University
Eli Aleksandrovich KOBRIN
Russian Federation
Works for the Compiler Technology Department at ISP RAS. He is a BSc student in the Faculty of Computational Mathematics and Cybernetics at Lomonosov Moscow State University
Andrey Nikolaevich FEDOTOV
Russian Federation
Works for the Compiler Technology Department, graduated from National Research Nuclear University MEPHI (Moscow Engineering Physics Institute) in 2013. Obtained PhD degree in 2017
References
1. CWE – common weakness enumeration. URL: https://cwe.mitre.org/.
2. M. Howard and S. Lipner. The Trustworthy Computing Security Development Lifecycle. Microsof, 2006. URL:http://msdn.microsoft.com/en-us/library/ms995349.aspx.
3. ISO/IEC 15408-3:2008. Information technology – Security techniques – Evaluation criteria for IT security – Part 3: Security assurance components.
4. ГОСТ Р 56939-2016: Защита информации. Разработка безопасного программного обеспечения. Общие требования. Национальный стандарт РФ, 2016. / GOST R 56939-2016: Information Protection. Secure Software Development. General Requirementsю National Standard of Russian Federation, 2016 (in Russian).
5. K. Serebryany. Continuous fuzzing with libFuzzer and AddressSanitizer. In Proc. of the 2016 IEEE Cybersecurity Development (SecDev), 2016, p. 157.
6. A. Fioraldi, D. Maier et al. AFL++: combining incremental steps of fuzzing research. In Proc. of the 14th USENIX Workshop on Offensive Technologies (WOOT 20), 2020, 12 p.
7. J.C. King. Symbolic execution and program testing. Communications of the ACM, vol. 19, issue 7, 1976, pp. 385-394.
8. J. Salwan. Triton Under the Hood. 2015, URL: https://shell-storm.org/blog/Triton-under-the-hood/#8.
9. N. Stephens, J. Grosen et al. Driller: augmenting fuzzing through selective symbolic execution. In Proc. of the Network and Distributed System Security Symposium, volume 16 of number 2016, 16 p.
10. I. Yun, S. Lee et al. QSYM: a practical concolic execution engine tailored for hybrid fuzzing. In Proc. of the 27th USENIX Security Symposium, 2018, pp. 745–761.
11. R. Baldoni, E. Coppa et al. A survey of symbolic execution techniques. ACM Computing Surveys, vol. 51, issue 3, 2018, Article no. 50, 39 p.
12. A. Vishnyakov, A. Fedotov et al. SYDR: cutting edge dynamic symbolic execution. In Proc. of the 2020 Ivannikov ISPRAS Open Conference (ISPRAS), 2020, pp. 46-54.
13. S. Poeplau and A. Francillon. Symbolic execution with SymCC: don’t interpret, compile! In Proc. of the 29th USENIX Security Symposium, 2020, pp. 181-198.
14. S. Poeplau and A. Francillon. SymQEMU: compilation-based symbolic execution for binaries. In Proc. of the 2021 Network and Distributed System Security Symposium, 2021, 18 p.
15. L. Borzacchiello, E. Coppa, and C. Demetrescu. FUZZOLIC: mixing fuzzing and concolic execution. Computers & Security, vol. 108, 2021, article no. 102368.
16. D. Kuts. Towards symbolic pointers reasoning in dynamic symbolic execution. In Proc. of the 2021 Ivannikov Memorial Workshop (IVMEM), 2021, pp. 42-49.
17. J. Chen, J. Wang et al. JIGSAW: Efficient and Scalable Path Constraints Fuzzing. In Proc. of the 2022 IEEE Symposium on Security and Privacy (SP), 2022, pp. 1531-1531.
18. C. Cadar, D. Dunbar, and D. R. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proc. of the 8th USENIX Conference on Operating Systems Design and Implementation, 2008, pp. 209-224.
19. S.K. Cha, T. Avgerinos et al. Unleashing Mayhem on binary code. In Proc. of the 2012 IEEE Symposium on Security and Privacy, 2012, pp. 380-394.
20. Google sanitizers. URL: https://github.com/google/sanitizers.
21. Y. Chen, P. Li et al. SAVIOR: towards bug-driven hybrid testing. In Proc. of the 2020 IEEE Symposium on Security and Privacy, 2020, pp. 1580-596.
22. S. Österlund, K. Razavi et al. ParmeSan: sanitizer-guided greybox fuzzing. In Proc. of the 29th USENIX Security Symposium, 2020, pp. 2289-2306.
23. T. Wang, T. Wei et al. IntScope: automatically detecting integer overflow vulnerability in x86 binary using symbolic execution. In Proc. of the Network and Distributed System Security Symposium, 2009, 14 p.
24. R. Demidov, A. Pechenkin, and P. Zegzhda. Integer overflow vulnerabilities detection in software binary code. In Proc. of the 10th International Conference on Security of Information and Networks, 2017, pp. 101-106.
25. A. Niemetz and M. Preiner. arXiv: 2006.01621, 2020, 2 p.
26. A. Vishnyakov, V. Logunova et al. Symbolic security predicates: hunt program weaknesses. In Proc. of the 2021 Ivannikov ISPRAS Open Conference (ISPRAS), 2021, pp. 76-85.
27. CWE top 25 most dangerous software weaknesses. URL: https://cwe.mitre.org/top25/archive/2021/2021_cwe_top25.html.
28. G. Savidov and A. Fedotov. Casr-Cluster: crash clustering for Linux applications. In Proc. of the 2021 Ivannikov ISPRAS Open Conference (ISPRAS), 2021, pp. 47-51.
29. FreeImage project. URL: https://freeimage.sourceforge.io/.
30. FreeImage: Integer overflow errors in differnet places. URL: https://sourceforge.net/p/freeimage/bugs/347/.
31. xlnt project. URL: https://github.com/tfussell/xlnt.
32. xlnt: Integer overflow in compound_document::read_sector. URL: https://github.com/tfussell/xlnt/issues/616.
33. xlnt: Integer Overflow in compound_document::read_sector leads to Heap Buffer Overflow. URL: https://github.com/tfussell/xlnt/issues/626.
34. xlnt: Segmentation fault in xlnt::detail::compound_document::follow_chain(). URL: https://github.com/tfussell/xlnt/issues/595.
35. Unbound project. URL: https://github.com/NLnetLabs/unbound.
36. Unbound: Integer Overflow in sldns_str2period function. URL: https://github.com/NLnetLabs/unbound/issues/637.
37. HDF4 library. URL: https://support.hdfgroup.org/products/hdf4/whatishdf.html.
38. Hdp from hdf4-tools division by zero. URL: https://bugs.launchpad.net/ubuntu/+source/libhdf4/+bug/1915417.
39. Miniz library. URL: https://github.com/richgel999/miniz.
40. PyTorch project. URL: https://github.com/pytorch/pytorch.
41. Miniz: Fix integer overflow in header corruption check. URL: https://github.com/richgel999/miniz/pull/238.
Review
For citations:
VISHNYAKOV A.V., KOBRIN E.A., FEDOTOV A.N. Error detection in binary code with dynamic symbolic execution. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2022;34(2):25-42. https://doi.org/10.15514/ISPRAS-2022-34(2)-3