A Modular Approach On Building Certified Software System

As computer keeps the trend of exerting influence over various aspects of human society, safety issue of computer programs is becoming more and more threatening on both Internet and personal computers. Unfortunately, far from ensuring the safety of all programs, the endlessly emerging virus and network attack always put our computers in great danger. Such menaces are resulted from the lurking bugs in programs, and even a small buggy program may cause the crash of the whole software system. In many paramount systems like nuclear control system and aerospace-plane control system, such bugs would be unpardonable. Formal certification methodology during software development is an approach to improve quality of programs. Among all the formal certification methods, static program certification distinguishes itself as a reliable and feasible method.The technique adopted by this paper is called proof-carrying code. Proof-carrying code is a program with attached proof, which describes the well-formedness of the certified program. Before running the program, a host will check the validity of the proof to evaluate the safety of the program. The validation of the proof indicates that the safety policy of the host will not be violated by the program at runtime.This paper firstly presents the definition of the concepts of program, abstract machine, operational semantics, safety definition and a certifying system in a proof-carrying code framework. The certifying system is used to construct simple proof-carrying codes. Nonetheless, as in traditional research on proof-carrying code frameworks, modular certification is not supported by this framework either. As is well known, realistic programs are developed in a modular way. The whole complicated program may be divided into several modules, which are easier to develop separately, and all the modules can be linked to form the complete version. Therefore, modularity plays a very important role in the modern software engineering, which necessitates the modularization of program certifying. To complicate the problem, the semantics of different modules may be in different styles and imposes much difficulty to be certified in a same certifying system.In this dissertation, a proof-carrying code framework to support modular certification is proposed. In this framework, after the separate certification, different modules with attached proof can be linked together to form a complete proof-carrying code package. Additionally, different modules can be certified in different certifying systems. The basic idea behind the framework is the adoption of an abstract program reasoning system, which supports good modularity, and in which other certifying systems can be embedded. This dissertation delves into the embedment of a certifying system(SCAP), which supports control stack reasoning, and the transplant of typed certifying system (TALP) into the proof-carrying code framework. Two modules, main certified in TALP and newpair certified in SCAP^?, as well as their proof, can be linked together.This dissertation also addresses the problems of safety proof automatic generation. A verification condition generator for SCAP and a type-checker for TALP are proposed. Employing these tools, the construction of safety proof of each module are largely simplified, which predicates the possibility of larger scale modules certification.All the formal definitions, descriptions and proofs have been formalized in the proof assistant Coq. So all the theorems presented in this dissertation are machine-checkable.The work of this dissertation is the first step to modularity certification framework, which demonstrates good modularity, and brings a bright prospect to the research and application of high-assurance software development.This dissertation was supported by Chinese Natural Science Foundation under Grant No. 60673126.