The Design And Implementation Of Verification Conditions Generator Of Safe C Language Verification Tool

With the wide application of compute technology, we have higher requirements for safety and security of software. These demands are reflected in safety-critical systems and infrastructure, including nuclear power, aviation, aerospace, military, finance etc. They are also reflected in people’s daily life areas such as automobile, medicine, electronic payments etc. As one of the major programming languages, C language has been widely used in operating systems, embedded software, compilers, and other areas. Due to features such as pointers and dynamic memory allocation, C programs are prone to security vulnerabilities, e.g. illegal pointer dereference, memory leaks. Discovering these security vulnerabilities in C programs by static analysis, dynamic analysis and program verification are hot research directions in both academic and industrial research. We are developing a program verification tool:Safe C Language Verification Tool, which is based on deductive reasoning. It is an automatic verification tool for C programs. It can discover memory errors and prove that a C program is able to meet its specification.This dissertation describes the design and implementation of verification conditions generator of the tool. Its main functionality is:1) the calculation of post assertions based on the calculation rules and function protocols; 2) the generation of verification conditions at each program point based on post assertions.Contributions of this dissertation are listed as follows:Firstly, this dissertation has designed and implemented assertion calculation processes, including assertion calculation rules based on Hoare logic for all kinds of statements in the Safe C Specification Language and procedures that need to be done before and after applying calculation rules. In addition, at each program point the verification conditions generator also needs to do some checking, including type variants and type invariants, out-of-range pointer access, illegal pointer dereference, etc.Secondly, this dissertation has designed and implemented a method for formal verification of programs involving stack pointers and static area pointers. The method defines the triple-attribute of a pointer, including the name and the size of the data block that the pointer points to, as well as the offset of the pointer within the data block. By extending Hoare logic, we have designed assertion calculus rules for generating verification conditions based on the triple-attribute. The method is capable of detecting path aliases, wild pointers and illegal pointer de-references.For calculating assertions of heap pointers, this dissertation has provided necessary interfaces to call the shape analysis module. By using the verification condition generator, our Safe C Language Verification Tool has successfully verified some classic algorithms from textbooks.