Dissertation > Excellent graduate degree dissertation topics show

A Modular Approach on Building Certified Software System

Author: GuoYu
Tutor: ChenYiYun
School: University of Science and Technology of China
Course: Computer Software and Theory
Keywords: software safety program certification assembly language proof-carrying code modular certification
CLC: TP311.52
Type: PhD thesis
Year: 2007
Downloads: 227
Quote: 0
Read: Download Dissertation

Abstract


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.

Related Dissertations

  1. A Close Stduy of Cohesive Devices Used in C-Einterretation,H315.9
  2. Research and Implementation of Embedded Assembly and Pragma Based on IMPACT,TP368.1
  3. DICOM image processing technology efficient data,TP391.41
  4. Research and Development on Network Assisted Teaching System of Assembly Language Programming Course,TP311.52
  5. PE file encryption Design,TP309.7
  6. ARM-based large-screen LED display system design study,TN873
  7. Research of Inter-Frame Prediction Algorithm of H.264 Video Coding Standard and DSP Implementation,TN919.81
  8. Research on Optimal Design and Implement of DSP-based XVID Video Decoder,TN764
  9. Multi- link structure of city street lights energy-saving micro ultimate wireless controller,TU994
  10. The Realization of HCO Network Operating System with Cx51,TP316.8
  11. Software Development Platform of the Single Chip Microcomputer Based on VC,TP311.52
  12. The Modelling and Application of a New Model of Software Reliability and Safety,TP311.52
  13. Design and Implementation of an embedded assembler software testing platform,TP311.52
  14. Analysis and Designs of Tax Bank Treasury Electronic Payment Platform System,TP311.52
  15. Embedded System Supported Safety Critical Software Design for Railway Signal,U284.362
  16. Research and Development of a Portable Engine Air-fuel Ratio Meter,TK401
  17. MCU controlled electronic fuel injection pump test bench research,TK427
  18. Ultrasonic testing signal spectrum analysis and software design,TP311.1
  19. YC7150 grinding machine CNC transformation,TG616
  20. Analysis and Check of Type Conversion and Control Flow Safety Vulnerability,TP309
  21. Software Safety Assurance Framework and Safety Technology Application,TP311.52

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Program design,software engineering > Software Engineering > Software Development
© 2012 www.DissertationTopic.Net  Mobile