Based On The Logic Of Program Verification Methods In The Development Of High Confidence Software

Today, most softwares are of large scale, so the programmers have paid much more attention to their safety. But until now, the safety guarantee provided by existing programming language and software engineering technology is weak and unreliable. For instance, in the production of software, standard engineering method and intensive testings are used to decrease bugs. However, it can't be guaranteed that there are no bugs after intensive testings, in fact, new bugs will be introduced when the old bugs are fixed. It can be asserted that existing software engineering techniques can't improve the software safety and security essentially. On the other hand, language based approach of program verification can provide guarantee for software safety.Language based approach of program verification makes the programs of this language safe through adding language components of types (logic predicates), which are called program specifications universally, and typing rules (reasoning rules), which should be definitely proved to be sound. Existing research on certified code and type system has contributed much on the guarantee of a variety of program (high-level or low-level) safety properties, such as the simple type system of modern programming language, which can be utilized to check some simple semantics errors and guarantee fundamental safety properties with little cost. Although research on type system of high-level and intermediate language have contribute to computation safety significantly, the ultimate codes executed in machine are binaries, which are originated from certified programs and not certified themselves. For this reason, many researchers begin explore the approaches of low-level program verification and certifying compiler which preserves the program specification from high-level to low-level. Compared with logic predicates, types are less expressive, so type system can't deal with complex safety requirements, such as program correctness, information flow security. Thus, although type system is widely used, until now, no certified version of boot loader, operation system kernel, and runtime library are released, whose safety are critical for the safety of whole computation system. In the other hand, Hoare logic has enough expressiveness since logic predicates can express more information than types. However, the support of stack-based function call is weak in Hoare logic. For these reasons, the goal of this research is substituting logic predicates for types as program specification so that type system...