| With the development of the Internet,the security of software has attracted people’s attention,so the program verification technology has been developed rapidly.Program verification is a technology to study program security,which depends on the design of verification algorithms,among which predicate abstract algorithm,Impact algorithm,k-induction algorithm and lazy abstract algorithm are widely used.In recent years,in the software security verification competition,the experimental results show that the k-induction algorithm has the potential to outperform the lazy abstract algorithm when verifying cyclic programs.Therefore,this dissertation designs and develops a verification tool to verify the security of C language programs,and implements an improved k-induction algorithm in this tool.The main innovation achievements are as follows:1.In view of the existing verification tools that construct too many times of model refinement and iterate redundant program paths during program verification,a verification tool K-CValidator based on model detection is designed and developed,which can delete information irrelevant to security attributes to be verified.Then,a system with security attributes to be verified and a small scale is obtained,which realizes the reduction of program state space and saves resources for the verification process of subsequent algorithms.2.Aiming at the problems of low induction efficiency and time-out in k-induction algorithm verification for programs that are asserted to be in the loop,value analysis method is introduced to generate cyclic invariants to strengthen the constraints of k-induction cycle conditions and induction iteration.In this dissertation,the proposed improved K-induction algorithm is tested on the validation tool K-CValidator.Through comparison experiments,it is proved that the improved algorithm can effectively reduce the validation time and improve the validation accuracy when verifying the cyclic program. |
