Certifying Compilation In An Infrastructure For Developing Trustable Software

Nowadays, high-assurance software is more and more valued, and among its properties, safety and security are most important. Safety is the ability to guarantee that software execution does no harm to the system. And security is the ability to preserve the confidentiality, integrity, availability and authentication of data. There is a close relationship between safety and security. For example, hackers usually use low-grade safety errors, such as buffer overflows, out-of-bound array accesses and dangling pointer dereferences, to destroy a system or achieve unauthorized control of a system. Apparently, it is helpful to ensure software security by strengthening its safety.To achieve software safety, all program errors should be discovered before the execution of the program or be gently captured during the execution. 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 (i.e. program verification) is one of the hot topics in this research field. In the past decade, great progress has been made in the area of program verification. Many projects adopt type-based or logic-based approaches to reason about program properties. And in recent years, some projects have tried to combine them. However, previous program verification projects have focused on either high-level programming languages or low-level assembly languages, but not on both simultaneously. Research on high-level languages has many advantages such as user-friendliness, early safety bug detection etc., but the TCB (Trusted Computing Base) is relatively large; on the other hand, the TCB of low-level program verification is much smaller but the low-level safety proofs are more complex and harder to construct than the high-level ones. Even though some certifying compilers are able to produce safety proofs for assembly programs based on the knowledge of the compiled source programs, only some simple program properties—typically those of type system—could be proved automatically. Much more complex properties, such as partial correctness about values, are hard to prove automatically in these compilers.Under the above considerations, in this dissertation, I present the design and implementation of a high-assurance software development infrastructure. 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. The main advantage of this infrastructure is that the proved safety properties include not only type properties, but also advanced properties, such as partial correctness about values. This dissertation presents the important technique I adopted in certifying compilation. That is, along with code generation, the compiler produces the safety proofs of the assembly programs satisfying assembly specifications from source-level programs, specifications and safety proofs. Both the specifications and the safety proofs are carried by the code, and could be checked by an assembly-level proof checker to ensure that the code satisfies its specifications. The work in this dissertation is inspired by TAL (Typed Assembly Language), CAP (Certified Assembly Programming) and PCC (Proof-Carrying Code) etc., and adopts an approach of combining both types and logics.In this dissertation, I, firstly, introduce some previous work on program verification and certifying compilation; then I present a high-assurance software development infrastructure; next I mainly present the certifying compilation techniques based on this infrastructure and the design and implementation of a certifying compiler prototype. These techniques include: verification condition generation (VC Gen), assembly-level code specification translation and generation, assembly-level safety proof generation, etc. I also discuss the influence of certifying compilation techniques on traditional compilation.The main contributions and characteristics of this dissertation are:It presents an infrastructure for high-assurance software development. This infrastructure gives an interface for programmers to provide source specifications and the proofs of programs satisfying these specifications along with source programs. A certifying compiler in this infrastructure could produce the assembly specifications and safety proofs from the source-level ones. Assembly-level proof checking removes the compiler from the TCB, and so enhances the reliability of the system. The automatic assembly-level proof generation alleviates the difficulty of writing proofs.It improves the design of source-level VC Generation algorithm. The new algorithm turns the problem of proving programs satisfying specifications into an equivalent problem of judging the validity of the verification conditions (VCs). This algorithm also combines the collection of side conditions in source typing rules and considers the simplification of VCs. The proving of source VCs makes the early bug detection possible and easy.It shows the design and implementation of a certifying compiler prototype, and this certifying compiler produces assembly-level specifications and safety proofs automatically from the source-level counterparts. The generated proofs contain the soundness proofs of VC generation, so that the VC generator is removed from the TCB. And this avoids the existence of a big TCB—VC generator. Compared with previous certifying compilers, this compiler could deal with much more complex program properties, such as partial correctness about values.