Proof Generation For Certifying Compiler

With the rapid development of computer science and technology, computer soft-wareinalargescaleismoredifficulttodebugandmaintain. Ontheotherhand,itisgrimthat the situation of safety and security of computer software and it gradually emergesthattherunningsafetyofthecodesprovidedbytheuntrustedsource. Inthiscontext, thedemand for high-confidence software used in the key areas of state and society is grow-ing. In a variety of software technologies to construct the high-confidence software,formalized program verification ensures that the programs will not violate the safetyspecification when running, by formalizing the property of programs and producing theformalized proof to ensure the safety.As an important branch of the verifying compiler, certifying compiler combinesmodern compiler technology and the program verification method. It generates theproof about the program property according to the notation of the source codes writedby programmers, when producing the assembly codes. The code consumer only needto use a trusted proof checker to check the generated proof and then indirectly checkthe safety of the codes, which removes the compiler from the trusted computing base.In the framework of certifying compiler, automated theorem prover plays a key role.Without automated theorem prover, programmers have to generate all proofs by hand,which is a huge workload.Based on our former projects PLCC, we design and implement a certifying com-piler: CComp. Its main feature is that it uses the Hoare style program verification meth-ods, apply the serparation logic to express the verification conditions, particularly theverification conditions about pointers. It introduces modern automated theorem prov-ing technology to automatically prove the verification conditions, use the framework ofstack-based certified assembly programming for reference to define the back-end pro-gram verification framework. The automated theorem provers embedded in CComp,support the linear arithmetic and the serparation logic, and generates the proof that canbe checked by the proof assistant Coq.In this thesis, we first introduce the research background and current research sta-tus. Then briefly describe our design and implement of the certifying compiler CComp,including the source language, assertion language, source-level verification frameworkand back-end verification framework. In the source-level verification framework, this thesis highlights the linear arithmetic prover which we design and implement based onSimplex algorithm and Bound & Branch method, and the proof library system proposedto save and manage the information of proving and generate the proof. We describessome key algorithms, including the real satisfiability check procedure, the informationof proving save procedure and the main algorithm of proof generation. Finally, thethesis gives two simple tests. The results show that our linear arithmetic prover canautomatically prove the verification conditions about linear arithmetic generated by ourcertifying compiler, and the generated proof is better than that generated by the Coq-tactic Omega.The main contributions of this thesis are:1. BasedonSimplexalgorithmandBound&Branchmethod,Itdesignsandimple-ments a linear arithmetic prover which is used to prove the linear arithmetic verificationconditions.2. It presents a new method of proof generation, which is used to generate theCoq-checkable proof term automatically in the automated theorem prover. It can au-tomatically construct the proof term according to the needs of the proof to select theexisting fragmented proof information, and form a proof term that is basically non-redundant. Its proof term is more simple than that generated by Omega which is a Coqtactic.The significance of this work lies in that through the research on the machine-checkable proof generation of automated theorem proving technology, we proposed anew method about proof generation, accumulated the experience on the automated the-oremprovingtechnologyindomain-specificlogic, andlaidthetheoreticalandtechnicalbasis for automatic program verification and building high-confidence software in thefuture.