Font Size: a A A

The Design And Implementation Of Safe C Language

Posted on:2017-03-05Degree:MasterType:Thesis
Country:ChinaCandidate:W S LiFull Text:PDF
GTID:2308330485451671Subject:Computer application technology
Abstract/Summary:PDF Full Text Request
In today’s highly information-oriented society, social life and production are highly dependent on software systems, so security and reliability of software systems become more important. Formal verification is an important way to ensure the safety of programs.There are two ways of formal verification. One is model checking, which traverses all the state space of the system to automatically verify the finite-state system and construct counterexample that does not meet the properties and theorems. Another one is deductive inference, which makes deductions for programs mathmetically by formal methods. Although automatic verification tools based on deductive inference have already been developed in some laboratories, they have not been applied in industry. The ultimate reason is the difficulty in automatic theorem proving, which limits the capability of such procedures as the descriptive ability of assertion language, inference of loop invariants, alias analysis, and proving verification conditions. For this reason, at the same time of improving the ability of automatic theorem proving, we should give appropriate consideration to reduce our expectation on it. We can design a safe language to raise the threshold of valid programs, and design a specification language that describes the behavior of programs to reduce the burden of theorem provers.The main contributions of this thesis are listed below:First, safe C, a subset of the C language oriented for verification, has been designed. In the procedure of program verification based on Hoare logic inference rules, whenever the assignment axiom{Q[E/x]}x=E{Q}(Q is the post-condition of assignment statement, Q[E/x] means substitute x in Q by E) is applied, we must ensure that the assignment statement and assertion Q[E/x] have no potential aliases. Otherwise, the conclusion that Q[E/x] is the weakest pre-assertion becomes unreliable. The widespread existence of aliases in the C language raises problems for Hoare logic based inference. In this thesis, based on the C99 standard, we discuss the safty problems of the C language from the perspective of aliases and analyze how these problems affect program verification. Inspired by this, we design the safe C language, which imposes some restrictions on various data types so that the operations on the variables of certain types can be more regular. In addition, it requires that some annotations be used to describe program behavior to reduce the burden of automatic theorem provers.Second, a specification language has been designed. The specification language defines the syntax, semantics and usage of the annotations that safe C language requires. The specification language describes the behavioral interface of C language in a formal way, and these formal descriptions will eventually be passed to the automatic theorem prover to help the prover to better capture the behaviors of program and finally to help the prover prove if the program meets these specifications. In the specification language, we introduce shape descriptions to represent pointer related properties. The shape descriptions are used to address the verification problems caused by these pointer aliases.Third, we have implemented the program restrictions that safe C language requires and the analysis of the specification language in Clang.
Keywords/Search Tags:Hoare Logic, Formal Verification, Safe Language, Specification Language, Shape Description
PDF Full Text Request
Related items