Design And Implementation Of Assertion Guided Multithreaded Symbolic Execution

In modern society,software has become one of the most important infrastructures and plays an indispensable role in many industries.At the same time,the security of software is getting more and more attention.As one of the important methods to guarantee the reliability of software,software testing has always been a hot topic for researchers at home and abroad.Dynamic symbol execution technology is a cutting-edge technology in the field of software testing and has been receiving widespread attention since its birth.Domestic and foreign researchers have developed many practical software testing tools based on dynamic symbolic execution technology,of which KLEE is one of the best.However,KLEE can only perform symbolic execution on single-threaded programs.In view of this,Stefan Bucur of the Federal Institute of Technology in Lausanne,Sweden,and its partners developed the parallel symbol execution tool Cloud9 on the basis of KLEE,implementing symbolic execution of multi-threaded programs.However,Cloud9 does not consider thread interleaving scheduling when performing symbolic execution on multi-threaded programs,so it cannot fully explore all paths of multi-threaded programs.Therefore,based on Cloud9,this paper designs and implements a general multithreaded symbolic execution framework that can cover all paths.Based on this,it proposes a multithreaded symbolic execution method based on assertion guidance.The main contributions of this article include the following three points: Based on the basic theory of symbolic execution and Cloud9's method of symbolic execution of multi-threaded programs,the general multithreaded program symbolic execution framework that can cover all path branches is given,which is described from three aspects: Firstly,The related concepts of multi-threaded symbolic execution are described to prepare for the subsequent algorithm.Secondly,the concept of a generalized interleaving graph(GIG)is introduced to implement the modeling of the multithreaded symbol execution process.Finally,the basic process of general multithreaded symbolic execution is given in the form of an algorithm.In order to alleviate the path explosion problem faced by multi-threaded symbolic execution,this paper proposes a multithreaded symbolic execution method based on assertion guidance based on the general multithreaded symbolic execution framework.And then it gives the design scheme of important modules in this method and Finally implements this method on Cloud9.The method proposed in this paper was tested using the multithreaded program test cases provided by The 2018 Software Verfication Competition.The test result shows that this method is feasible for cutting the redundant execution.To a certain extent,this method alleviates the path explosion problem of multithreaded symbol execution.