A formal model for program defect detection using symbolic program execution

An automatic program defect detection is extremely important direction of current research and development in the field of program reliability and security assurance. There were performed research of different ways of application for combined analysis methods which mix static source code analysis and dynamic symbolic execution, fuzz testing and dynamic symbolic execution as part of previous period of two years for project 17-07-00702 of the Russian Foundation for Basic Research. This paper presents elaboration of previously presented methods in form of formal model of program symbolic execution applied for program defect detection and implementation of analyzer of memory buffer bounds violation based on this model. The common theorem for program defect detection based on model of symbolic program execution and violation of definitional domain for computation system operation is formulated and proved. A special case theorem for buffer bounds violation detection is formulated and proved basing on common theorem and shadow memory model. As a practical application for theoretical basis an implementation of the analysis tool prototype description provided. Experimental results are received on the set of command line utilities of Debian Linux distribution, which shows applicability of proposed theoretical basis for solving practical tasks in the field of program reliability and security assurance.