Certifying The Safety Of Assembly Pointer Programs

With the rapid development of computer science and technology,computer software is more and more widely used in various industries.The dependence of computer software using in the key areas of the state and society is growing.So high-assurance software is more and more valued,and among its properties,safety and security are most important.The objective to improve software safety is:all program errors in the programs were discovered before the program is executed,or were captured moderately.Thus it ensures that programs would not result in unpredictable system behaviors.The research goal of software safety is to build a wholesome scientific and technological infrastructure for the management of software safety.And the verification method for software to meet its safety policies is one of the hot researches.In the past decade,great progress has been made in the area of program verification.Proof-Carrying Code brings two grand challenges to the research field of programming languages.By analysis of the current research situation,combining both type-based and logic-based approaches is a better way.We have designed a high-assurance software development infrastructure.In this infrastructure programs are certified to meet their safety policies using a simple type system and a logic system.In this infrastructure,source-level and assembly-level program verification could be done simultaneously,and a certifying compiler produces assembly-level safety proofs automatically from the source-level specifications and safety proofs.In terms of our infrastructure to design and verification of safety programs,and the pointer logic proof system,this dissertation presents the research work in assembly-level program verification.Among various computer programs,the programs containing pointers are more complex to reason about.So the research on verification of assembly pointer programs is an emphasis.The work in this dissertation is inspired by Hoare Logic,PCC(Proof-Carrying Code)and CAP (Certified Assembly Programming)etc.,and adopts an approach of combining both types and logics.This dissertation firstly introduces our research background on software safety and verification of pointer programs.Then a high-assurance software development infrastructure is presented.Under this infrastructure,the design and implementation of the assembly verification framework will be introduced.The main characteristics and contributions of this dissertation are:●A design of formal verification framework(Function-based Certifying Assembly Programming,FCAP)based on a x86 target machine.It is based on Intel x86 target machine.●A design of the assembly pointer logic(APL)for reasoning the safety of the assembly pointer programs.It has resolved difficulties to deal with the aliases using Hoare logic.It assures that there will be no null-pointer dereferences and no memory leak after the program is passed the verification.●Proof of the soundness of the assembly pointer logic is finished in the proof assistant Coq.●Implementation of a prototype system of the assembly-level verification framework.And using this prototype system,some non-trivial pointer programs of operations on the lists and binary trees have been verified.This dissertation was supported by Chinese Natural Science Foundation under Grant No.60673126 and Intel China Research Center(Beijing).