A Formal Model for Detecting Bugs by Symbolic Execution of Programs
- PDF / 349,901 Bytes
- 6 Pages / 612 x 792 pts (letter) Page_size
- 6 Downloads / 205 Views
Formal Model for Detecting Bugs by Symbolic Execution of Programs A. Yu. Gerasimova,*, D. O. Kutsa,**, and A. A. Novikova,*** a
Ivannikov Institute for System Programming, Russian Academy of Sciences, Moscow, 109004 Russia *e-mail: [email protected] **e-mail: [email protected] ***e-mail: [email protected] Received February 12, 2020; revised March 15, 2020; accepted March 30, 2020
Abstract—Automatic detection of bugs in programs is an extremely important direction of current research and development in the field of program reliability and security assurance. Earlier studies covered, methods for program analysis that combine the dynamic symbolic execution, randomized testing, and static analysis. In this paper, a formal model for detecting bugs using the symbolic execution of programs and its implementation for detecting the buffer bounds violation is presented. A formal model of the program symbolic execution is described, and a theorem on detecting a bug on the basis of the violation of the operation domain is formulated and proved. An implementation of the buffer bounds violation analyzer in the process of symbolic program execution is described, and the application of the implemented prototype for analyzing a set of programs in Debian Linux is presented. The experiments confirm the actionability of the proposed method. DOI: 10.1134/S0361768820080046
1. INTRODUCTION A most important task for demonstrating bugs in a program found by an analyst or by automatic code inspection tools is the generation of a set of data on which the erroneous behavior of the program can be reproduced. The most popular method for detecting bugs during the program execution is the randomized testing method [1], which tests the program on pseudorandom external data and checks the program stability under unexpected external data [2]. The randomized testing method has high performance because the sets of external data can be rapidly generated and the program should undergo lightweight instrumentation (in the case of randomized testing with reinforcement), which does not significantly decelerate the program execution. However, the detection of bugs in the case of randomized testing is of random nature, and it cannot be used to reliably confirm the detected bug. An alternative way for generating test sets of external data is dynamic symbolic execution [3]. This method is based on the heavy instrumentation of the program code aimed at gathering the trace of executed instructions for the subsequent construction of a formula describing a model of the program execution. Based on this formula, new sets of external data are calculated that guide the program execution on an alternative path or reproduce the already detected bug. Due to the heavy instrumentation of the program code
and the high computational complexity of the formula evaluation, this method cannot be practically used for exhaustive testing of real-life programs. The most promising way of applying the method of dynamic symbolic execution is the directed analysis of the program [4]
Data Loading...
