Analyzing properties of path predicate slicing algorithm
https://doi.org/10.15514/ISPRAS-2022-34(3)-1
Abstract
Security development lifecycle (SDL) is applied to improve software reliability and security. It extends program lifecycle with additional testing of security properties. Among other things, fuzz testing is widely used, which allows one to detect crashes and hangs of the analyzed code. The hybrid approach that combines fuzzing and dynamic symbolic execution showed even greater efficiency than classical fuzzing. Moreover, symbolic execution empowers one to add additional runtime checks called security predicates that detect memory errors and undefined behavior. This article explores the properties of the path predicate slicing algorithm that eliminates redundant constraints from a path predicate without accuracy loss. The article proves that the algorithm is finite and does not lose solutions. Moreover, the algorithm asymptotic complexity is estimated.
Keywords
dynamic symbolic execution,
DSE,
path predicate,
slicing,
irrelevant constraints elimination,
binary analysis
Supporting agencies: This work was supported by RFBR grant 20-07-00921 A
About the Author
Alexey Vadimovich VISHNYAKOV
https://vishnya.xyz/
Ivannikov Institute for System Programming of the RAS
Russian Federation
Ivannikov Institute for System Programming of the RAS
Russian Federation
Works for the Compiler Technology Department at the ISP RAS, obtained BSc degree and M.D. in the Faculty of Computational Mathematics and Cybernetics at MSU
References
1. M. Howard and S. Lipner. The security development lifecycle. SDL: A Process for Developing Demonstrably More Secure Software. Microsoft Press, Redmond, 2006, 348 p.
2. ISO/IEC 15408-3:2008: Information Technology – Security Techniques –Evaluation Criteria for It Security – Part 3: Security Assurance Components. ISO Geneva, Switzerland, 2008.
3. ГОСТ Р 56939-2016: Защита информации. Разработка безопасного программного обеспечения. Общие требования. Национальный стандарт Российской Федерации, 2016 / GOST R 56939-2016: Information Protection. Secure Software Development. General Requirements, National Standard of Russian Federation, 2016 (in Russian).
4. K. Serebryany. Continuous Fuzzing with libFuzzer and AddressSanitizer. In Proc. of the the 2016 IEEE Cybersecurity Development (SecDev), 2016, p. 157.
5. 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.
6. 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.
7. S. Poeplau and A. Francillon. Symbolic execution with SymCC: don’t interpret, compile! In Proc. of the 9th USENIX Security Symposium (USENIX Security 20), 2020, pp. 181-198.
8. 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.
9. L. Borzacchiello, E. Coppa, and C. Demetrescu. FUZZOLIC: mixing fuzzing and concolic execution. Computers & Security, vol. 108, 2021, article no. 102368.
10. E. J. Schwartz, T. Avgerinos, and D. Brumley. All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In Proc. of the 2010 IEEE Symposium on Security and Privacy, 2010, pp. 317-331.
11. R. Baldoni, E. Coppa et al. A survey of symbolic execution techniques. ACM Computing Surveys, vol. 51, issue 3, 2018, article no. 50, pp. 1-39.
12. 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.
13. 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.
14. 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, pp. 209-224, 2008.
Review
For citations:
VISHNYAKOV A.V. Analyzing properties of path predicate slicing algorithm. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2022;34(3):7-12. (In Russ.) https://doi.org/10.15514/ISPRAS-2022-34(3)-1
Email this article 