Design of a Certifying Compiler Supporting Proof of Program Safety Yiyun Chen Lin Ge Baojian Hua Zhaopeng Li Cheng Liu Department of Computer Science and Technology University of Science and Technology of China Hefei,Anhui 230026,China yiyun @ustc.edu.cn gelin,huabj,zpli,liuc5 @mail.ustc.edu.cn Abstract safety policies is one of the hot topics in this research field. In the past decade,great progress has been made in the Safety is an important property of high-assurance soft- area of program verification.Many projects adopt type- ware,and one of the hot research topics on it is the veri- based or logic-based approaches to reason about the prop- fication method for software to meet its safety policies.In erties of low-level or high-level programs.The TAL (Typed our previous work,we designed a pointer logic system and Assembly Language)[15]project and the theory of type re- proposed a framework for developing and verifying safety- finements [13]are two typical projects using type-based ap- critical programs.And in this paper,we present the design proaches,while Proof-Carrying Code(PCC)[16],Founda- and implementation of a certifying compiler based on that tional PCC(FPCC)[1].Certified Assembly Programming framework.Here we will mainly explain verification con- (CAP)[19]and Stack-based CAP (SCAP)[6]are typical dition generation,generation of code and assertions,and projects on logic-based techniques.Type-based and logic- proof generation for basic blocks.Our certifying compiler based techniques are complementary to each other,and has the following novelties:1)it supports a programming some projects have tried to combine them.Hamid et al. language equipped with both a type system and a logic sys- adopted a syntactic approach to FPCC[7],and gave a trans- tem:2)and it can produce safety proofs for programs with lation from a typed assembly language into FPCC in the pointers. Flint project.The ATS(Applied Type System)[18]project proposed by Hongwei Xi et al.extends a type system with a notion of program states,so that invariants on states can 1.Introduction be captured in stateful programming.By encoding Hoare logic in its type system,ATS can support Hoare-logic-like Nowadays,high-assurance software is more and more reasoning via the type system. valued,and among its properties,safety and security are Based on the above work,we have proposed a new most important.Safety is the ability to guarantee that soft- framework for developing and verifying safety-critical soft- ware execution does no harm to the system.And security ware: is the ability to preserve the confidentiality,integrity,avail- 1.Safety policies of a program are specified formally by ability and authentication of data.There is a close relation- programmers.These specifications as well as the cor- ship between safety and security.For example,hackers usu- responding program are submitted to a compiler. ally use low-grade safety errors,such as buffer overflows, out-of-bound array accesses and dangling pointer derefer- 2.The compiler produces verification conditions (VCs) for the submitted program.These VCs are required to ences,to destroy a system or achieve unauthorized control of a system.Apparently,it is helpful to ensure software se- verify whether the program satisfies its specifications. curity by strengthening its safety,and it makes us focus on If all of them are proved,the program is believed to software safety in this paper. satisfy the specifications.Most VCs can be proved To achieve software safety,all program errors should automatically by the embedded theorem prover in the be discovered before the execution of the program or be compiler,and the rest are proved interactively by pro- gently captured during the execution.The research goal grammers using proof-assistant tools.All the proofs of software safety is to build a wholesome scientific and should be produced and preserved. technological infrastructure for the management of software 3.The compiler compiles the source code and specifica- safety.And the verification method for software to meet its tions into assembly level counterparts while translatingDesign of a Certifying Compiler Supporting Proof of Program Safety Yiyun Chen Lin Ge Baojian Hua Zhaopeng Li Cheng Liu Department of Computer Science and Technology University of Science and Technology of China Hefei, Anhui 230026, China yiyun@ustc.edu.cn {gelin, huabj, zpli, liuc5}@mail.ustc.edu.cn Abstract Safety is an important property of high-assurance soft￾ware, and one of the hot research topics on it is the veri- fication method for software to meet its safety policies. In our previous work, we designed a pointer logic system and proposed a framework for developing and verifying safety￾critical programs. And in this paper, we present the design and implementation of a certifying compiler based on that framework. Here we will mainly explain verification con￾dition generation, generation of code and assertions, and proof generation for basic blocks. Our certifying compiler has the following novelties: 1) it supports a programming language equipped with both a type system and a logic sys￾tem; 2) and it can produce safety proofs for programs with pointers. 1. Introduction 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 soft￾ware execution does no harm to the system. And security is the ability to preserve the confidentiality, integrity, avail￾ability and authentication of data. There is a close relation￾ship between safety and security. For example, hackers usu￾ally use low-grade safety errors, such as buffer overflows, out-of-bound array accesses and dangling pointer derefer￾ences, to destroy a system or achieve unauthorized control of a system. Apparently, it is helpful to ensure software se￾curity by strengthening its safety, and it makes us focus on software safety in this paper. 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 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 the prop￾erties of low-level or high-level programs. The TAL (Typed Assembly Language) [15] project and the theory of type re- finements [13] are two typical projects using type-based ap￾proaches, while Proof-Carrying Code (PCC) [16], Founda￾tional PCC (FPCC) [1], Certified Assembly Programming (CAP) [19] and Stack-based CAP (SCAP) [6] are typical projects on logic-based techniques. Type-based and logic￾based techniques are complementary to each other, and some projects have tried to combine them. Hamid et al. adopted a syntactic approach to FPCC [7], and gave a trans￾lation from a typed assembly language into FPCC in the Flint project. The ATS (Applied Type System) [18] project proposed by Hongwei Xi et al. extends a type system with a notion of program states, so that invariants on states can be captured in stateful programming. By encoding Hoare logic in its type system, ATS can support Hoare-logic-like reasoning via the type system. Based on the above work, we have proposed a new framework for developing and verifying safety-critical soft￾ware: 1. Safety policies of a program are specified formally by programmers. These specifications as well as the cor￾responding program are submitted to a compiler. 2. The compiler produces verification conditions (VCs) for the submitted program. These VCs are required to verify whether the program satisfies its specifications. If all of them are proved, the program is believed to satisfy the specifications. Most VCs can be proved automatically by the embedded theorem prover in the compiler, and the rest are proved interactively by pro￾grammers using proof-assistant tools. All the proofs should be produced and preserved. 3. The compiler compiles the source code and specifica￾tions into assembly level counterparts while translating