Researches On Two Important Topics Of Certifying Compiler

As software becomes a part of the infrastructure of production and living of human beings, software security is becoming more and more import. In the research field, program verification which is an import approach to achieve security, use logic rules to prove the program setifies its specification. Certifing compiler which is combined by a compiler and a certifier uses this approach. The pioneer project TouchStone[1] developed by Necula can translate the source program to the target assembly code annoted with type annotations. The verifier then verify the target code setifyies the speicifications which describe the type safty and memory safty, and then finnaly produces Prof-Carring Code(PCC).Some sorce level verifier such as Smallfoot [2] and Boogie[3],let the programmer to provide the specification to describe the expected properties of the program. The verifier then verifies the source program setifies the specification like a type cheker. However, these systems do not provide PCC.The certifying compiler we proposed let the user to provide the specification use separation logic to express more properties than type safty. The compier verifies program both in source level and target level. Verify in source level can report errors in time, while target level verification can produce PCC.A practical compiler often has many optimization passes to produce more efficient code. Code optimization which we believe is significant for certifying compiler to become practical is less concerned by the community. Code optimization is composed by many code transformation sequences. The original specification of the the code may not correctly or adequately describe the property of the optimized code. So the specification should be transformed along with the code during optimization.In this paper, we research two important topics of certifying compiler.1. Verification condition generation and reduction in soruce level language. We focus on the design of the assetion language and the reasoning rules to find the pointer of balance and to simplify the VCs generate by the VC generator.2. How code optimization affect the specification. We research how to transform specification to pass the constraint of it to the optimized code in a certifying compiler with multiple optimization passes.These two topics are both significant to certifying compiler. In this paper we propose sultions for both the problems. We have also implement prototype systems to valid our solutions. The contribution and innovation of this paper are list below.1. Design the assertion language of our certifying compiler and implement verification condition generator for the source level verification. We also develop a rewrite system to reduce the redundant of the generated verification condition.2. We propose a dataflow analysis based method to transform specifications to sustain the constraint of original specifications to the optimized code.We also develop a prototype compiler with many important optimizations to demonstrate the feasibility of our approach.The following of this paper are divied into several parts. In part one, we introduce the background of certifying compiler. We will introduce program certification, certifying compiler and source level verifier. In part two we will introduce the assertion language, the inference rules, the design and implementation of VCGen, we will also introduce rewriting system of VC reducer. Part four will introduce compiler optimization and specification transformation.