Chinese Journal of Computers   Full Text
Title	A Pointer Logic for Safety Verification of Pointer Programs
Authors	CHEN Yi-Yun HUA Bao-Jian GE Lin WANG Zhi-Fang
Address	(Department of Computer Science, 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.3(372—380)
Abstract &   Background	Abstract Safety is an important issue among the properties of high-assurance software and developing the verification methods for software to meet safety policies is one of the hot research. In terms of the authors’ sketch of design and verification of safety programs, a pointer logic system is designed for a subset of C-like language. This logic system is an extension of Hoare logic system and inference rules are designed to express the modification of pointer information for every kind of statements. It can be used for accurate pointer analysis of pointer programs. The information from the analysis can be used to verify if pointer programs satisfy the side conditions of typing rules and then support safety verification for programs. The logic system can also be used to verify other properties of pointer programs. keywords software safety; pointer logic; Hoare logic; pointer analysis; type system background This research is supported by the National Natural Science Foundation of China(Verification and Compilation of Software Safety, grant No.60673126). Proof-Carrying Code (PCC) brings two grand challenges to the research field of programming languages. One is to seek more expressive logic or type systems to specify or reason about the properties of high-level or low-level programs. The other is to study the technology of certifying compilation in which the compiler generates proofs for programs with annotations. For the first challenge, Typed Assembly Language and the theory of type refinements are two typical research projects in type-based approaches, while PCC, Foundational Proof-Carrying Code and Certified Assembly Programming are typical research projects on logic-based techniques. Type-based and logic-based techniques are complementary to each other, some researchers have tried to combine those techniques. This paper presents the authors’ research progress in the first challenge. A pointer logic is designed for PointerC language, a subset with explicit memory allocation and deallocation of C-like programming languages, in the authors’ research. As an extension of Hoare logic, the pointer logic is used to prove properties of pointer programs. The main characteristic of the pointer logic is that its inference rules are used to catch the modification of pointer information caused by the execution of each statement. Based on these rules, we can reason out the null pointers, dangling pointers and equality of effective pointers at each point in a program, and then calculate alias set of each pointer. These are the base information to prove safety and other properties of pointer programs. The main contribution of this paper is the elementary design of the pointer logic. In the project, the authors’ have implemented a certifying compiler based on the pointer logic and proved safety of PointerC language and soundness of the pointer logic.