The Design And Implementation Of Verification Conditions Prover Of Safe C Language

It can be said that the status and role of software systems will become more and more important in various professions, but the consequent problem is the vulnerability in reliability and security of software systems, which is particularly important and urgent in a number of safety and life critical software systems, including aerospace,medicine, nuclear power, and finance. To guarantee the safety of software system,formal verification by deductive reasoning has become a hot research topic recently.Now Software security experts have designed and implemented a variety of program reasoning system to ensure that the behavior of software programs conforms to the corresponding security specifications.Aiming at the security of C language program, we are designing and developing an automatic program verification CPV oriented to the safe C language, whose main function is to guarantee the program passed through the verification in CPV as a program satisfies the specification of safety properties, by means of deductive reasoning on source program carrying with safety specifications. It includes a front-end for syntactic analysis, a verification conditions generator that is responsible for deductive reasoning, a shape system that is specialized for heap memory ion and analysis, and a verification conditions prover for the safe C language helped design mainly and implemented totally by myself in this paper.In this paper, the starting point of the verification condition prover is to prove the authenticity of the verification conditions in the verification process, the verification conditions prover is based on the automatic theorem prover Z3 with limited capability.The main contributions of this thesis are as follows:First, I participate in the design of and implement completely the verification condition translation framework for converting the safe C specification language SCSL to Z3 SMT2, it makes the verification tool can prove each verification condition automatically. In particular, to the types supported in original safe C, which don't be supported correspondingly in Z3, such as: record type, union type, pointer type etc, it implements all these types translation into Z3 SMT2 by the abstract description based on the Z3 algebraic data type.Second, there is no string type in original SCSL, I participate in the design of the logical string type and expand it into SCSL. It makes the description of string type program properties simpler and clearer. Meanwhile, I implement the translation of string type into Z3 SMT2 by the abstract description based on the Z3 algebraic data type.Third, around automated verification of programs operating with mutable data structures, I design and implement the lemma prover in CPV verification tool. Against the validity of inductive lemmas provided by user to assist for Z3, it adopts structure induction to prove automatically to ensure the reliability of program verification results. Its significance lies in under the objective constraints of the Z3 proving insufficient capacity, without reducing the reliability of verification tools at the same time, improve the proving ability of the verification system.Combining other modules in system, at present, CPV verification tool can verify the correctness of programs of array, pointer, mutable data structure and string type.