Font Size: a A A

Research On Security Verification Method Of C Language Program Based On Static Analysis

Posted on:2024-05-17Degree:MasterType:Thesis
Country:ChinaCandidate:S ZhangFull Text:PDF
GTID:2568307127960769Subject:Computer technology
Abstract/Summary:PDF Full Text Request
Nowadays,all kinds of software are widely used and have penetrated into all aspects of our lives,so the quality of software is particularly important.The most important thing of all kinds of software is the program.To ensure the quality of software,the correctness of the program must be considered.The static analysis method developed in recent years provides a theoretical framework for program verification.Within this framework,variable value increment method was applied to detect programs,which can not only detect bugs in programs,but also verify the correctness of programs.Based on the theory of static analysis,this paper designed and developed a static detection tool for incremental analysis on variable values of C language program,and this tool was applied to improve the traditional k-induction algorithm.The innovation of this work are as follows:1.In order to solve the problem of computational waste in process of verifying of bounded loop programs with assertions outside the loop,a value increment analysis method based on static analysis was proposed.Based on this method,a tool for incremental operation on program variable values was developed.This tool improves the efficiency of finding bugs for such programs and solves the problem of computational waste.2.In order to solve the problem of computational waste and verification timeout in process of applying k-induction algorithm to bounded loop programs with assertions within the loop,an improved k-induction algorithm for such programs was proposed by combining static analysis with dynamic analysis and combining the tool of value increment analysis with k-induction algorithm.The algorithm improves the efficiency of searching counterexample path and the accuracy of verification.
Keywords/Search Tags:Program verification, Static analysis, Value incremental analysis, K-induction algorithm, Bounded loop program
PDF Full Text Request
Related items