| With its rapid development, computer technology has been applied in various fields. Information services have become ubiquitous, from intelligent electronic devices to large-scale server clusters. With the enhancements of software functionalities, security issues become even more important. Formal program verification is an important way to enhance software security, and the verification based on deductive reasoning is the most rigorous and reliable among various verification methods. It first generates verification conditions through formal deductive reasoning based on the specific program logic. Then, a theorem prover proves the generated verification conditions. However, due to the difficulty of automatic loop invariants inference and the limited capability of automatic theorem prover, formal program verification currently only has a preliminary application in industry.Our research group developed a prototype verification system for the PointerC language, which is able to verify five basic shapes. However, PointerC is an experimental C-like language and has little practical value. Our research group has recently developed a verification system for the safe C language. The safe C language is almost the same as the complete C language. In addition, the verification system uses the safe C specification language to describe the behavior property of programs. The general process of verifying a program in the verification system is as follows:Starting from the assertions of the source program, the verification system first conducts joint calculation by utilizing symbolic assertions and shape graphs, then uses shape graph theory and automatic theorem prover to prove the verification conditions generated during calculation. Shape graph is used for describing the property of heap pointer in the program, and its calculation rules and logic relationship proofs are provided by shape graph logic. Shape graph logic is still incomplete in the calculation rules for binary trees, which has limited the range of programs the can be verified by our system. The main work of this thesis is to extend shape graph logic and implement the extended shape system in safe C language verification system.The extension of shape graph logic consists of three parts. The first part is to enhance the verification ability of the shape system on binary tree program by adding some transformation rules for binary tree shape, designing an algorithm to decide the type of loop body, and modifying inference process of loop invariant shape graphs. The second part is to make shape logic easier to implement and also more suitable for C language semantics by modifying some calculation rules of shape graphs and adding some transformation rules for linked list shape. The third part is to reduce the number of iterations during the process of inferring loop invariant shape graph by improving the inference process.The above extensions have been implemented in the Safe C Language Verification System. The shape system uses the relationship assertions among heap pointers in the shape graph to provide functionalities such as judging alias of heap pointer, verifying the property of heap pointer, automatically inference of loop invariant shape graphs and to reporting memory leaks. This thesis introduces the shape system implementation in five parts. The first is a simple introduction of verification process of verification system. The second is the description of folding and unfolding algorithms for shape graphs by a more unified and simple manner based on the transformation rule of shape graphs. The third is the implementation of algorithm that proves implication relationship among shape graphs by transforming shape graphs into pointer sequence. The fourth is the implementation of the improved process of automatic loop invariant shape graph inference. And the last is using the corresponding relationship among a pair of virtual variable and program variable to accomplish the abstraction process of shape graphs. |
PDF Full Text Request