Research On Verification Method Of C Language Program Based On Predicate Abstraction

As the scale of software and hardware system expands continuously and the function becomes powerful increasingly,the software security problem is getting worse.Model checking provides a new verification mode from perspective of mathematical theorem,but it will lead to state space explosion.State space explosion has always been influencing the further development and application of software verification and has become the bottleneck for this research direction.Impact algorithm is the concrete realization of lazy abstraction.In the refinement part of impact algorithm,the predicate is not stored as global storage any more,but is mapped to the state node.In this way,in next iteration,restart is not required,but approaching the wrong node from loop head of last iteration,which is called lazy abstract behavior.However,this technology still has some shortcomings.First,in the process of verification,Impact algorithm does not distinguish assert expressions.When the logical relationship bound by assert variable affects subsequent Impact coverage behavior,the convergence rate of verification model will slow down.Second,Impact algorithm completely depends on Craig interpolant solver to solve predicates,but the solution details of interpolant solver are invisible,which means interpolant results cannot be predicted,so we always get inefficient interpolant,and the algorithm cannot be terminated and will continue running indefinitely.In order to make up the shortcomings of Impact algorithm,this paper started from the analysis of C program,analyzed the abstract syntax tree of C program,and built the program transfer model.In the transfer model,it classified the logical relationship of assert expression.As long as it determined that the logical relationship of assert expression was single variable logical relationship,it immediately sent signals to refinement part to remind the need of logical analysis for expression in refinement process with purpose of eliminating the influence of assert expression on interpolant.Based on the fact that the interpolant solver was sensitive to variable,this paper put forward an optimized verification algorithm based on auxiliary expression.This algorithm inserts tracking expression into codes with the method of tracking variable.From perspective of interpolant calculation,this method affects the interpolant result by replacing the input parameter,thus getting efficient interpolant.From perspective of program function,this method maintains the original program expression.Finally,this paper conducted experimental verification for the optimized verification algorithm based on auxiliary expression.The experimental results show that on the premise of ensuring accuracy,this algorithm can reduce the memory consumption in verification process and shorten the verification time.