Chinese Journal of Computers   Full Text
Title	Design and Proof of a Safe Programming Language PointerC
Authors	HUA Bao-Jian CHEN Yi-Yun LI Zhao-Peng WANG Zhi-Fang GE Lin
Address	(Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230026) (Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou, Jiangsu 215123)
Year	2008
Issue	No.4(556—564)
Abstract &   Background	Abstract The safety property of programming languages plays a fundamental role in the design and implementation of safety-critical software systems. And the authors have made investigation towards the design and proof of safe languages suitable for system programming. This paper presents the design of a C-like imperative programming language PointerC. One novelty of PointerC is that typing rules in its type system are accompanied by logic propositions which are called side conditions. And this paper proves PointerC is safe—The executions of programs will not violate the safety policy of the language, if these side conditions hold. A pointer logic, as an extension of Hoare logic, has been designed for the purpose of proving pointer-related side conditions statically. This paper presents the soundness proof for the pointer logic. keywords software safety; language design; type systems; Hoare logic; pointer logic background This research is supported by the National Natural Science Foundation of China(Verification and Compilation of Software Safety, grant No.60673126), and the Intel China Research Center. These projects study the theory and method of program verification and compilation of software safety. Program verification is an important method to improve software reliability. And axiomatic semantics and certifying compilation are also well-populated research fields with decades of history. In the past decade, the success of Proof-Carrying Code (PCC) renews researchers’ interests in program verification. One important reason for PCC’s success is that by concentrating on safety properties, instead of partial correctness, the safety proofs could be generated automatically by a certifying compiler. Their research group has focused on research of scaling the technology of PCC to the verification and compilation of more realistic programming languages and more practical safety policies. This paper presents their research progress on the design and safety proof of the PointerC programming language. More specifically, they have designed a C-like imperative language PointerC which retains explicit memory allocation and deallocation features. By introducing side conditions, PointerC’s type system is kept expressive yet simple. The safety proof for PointerC is presented, which is based on the technique of invariants. To reason PointerC programs statically, a pointer logic, as an extension of Hoare logic, has been proposed in their previous work, and this paper presents the soundness proof of the pointer logic.