A Formal Model for Detecting Bugs by Symbolic Execution of Programs

作     者：Gerasimov, A. Yu. Kuts, D. O. Novikov, A. A. 

作者机构：Russian Acad Sci Ivannikov Inst Syst Programming Moscow 109004 Russia 

出 版 物：《PROGRAMMING AND COMPUTER SOFTWARE》 (程序设计与计算机软件)

年 卷 期：2020年第46卷第8期

页      面：731-736页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Russian Foundation for Basic Research [17-07-00702] 

主　　题：Static analysis 

摘      要：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.