A Pointer Logic For Safety Verification Of Pointer Programs

Nowadays, information technologies play more and more important roles in all aspects of our world: industries, governments, bussiness, and schools. Once a node in this network collapses, an expensice catastrophe would happen. As a result, the requirement for software safety and security becomes more and more urgent. To moderate this disparity, developing high-assurance software based on formal methods is an essential approach. Among various formal methods, language-based approach to software security has attracted widespread attention in the past decade. These approaches help reduce the Trusted Computing Base of software systems by starting from the base of software, that is, programming languages and compilers.One promising approach for high secure software development in the future is the software property proving-based framework. In this framework, programmers design safety policies and decribe them as software specifications, which are fed to the compilers along with normal program code. In order to prove these programs satisfy these specifications, the compiler generates verification conditions, which are proved automatically or interatively by the programmers. A compiler translates these program code, along with those verification conditions and proofs, and such kind of compilers are called certifying compiler. At the assembly level, an independent proof checker checks the object code to ensure it satisfy its specifications. The key benifit of this framework is that it offers source-level proof methods, instead of at assembly-level, which makes the process of program development more effecient. Meanwhile, making use of a certifing compiler greatly reduces the trusted computing base by removing the compier and prover from the TCB.As an integral part of the above framework, this thesis investigates pointer logic and its application to source code proving. This thesis designs PointerC, a C-like imperative language which retains C's explicit memory management facilities. The primary design motivation for PointerC is our goal to study more expressive safetye polies beyond type safety such as memory safety. And this thesis makes use of a static discipline combining type system and pointer logic system.This thesis proposes a novel program logic, i.e., the pointer logic. The primary goal for the design of pointer logic is: on on hand, traditional type system are weak and could not check the value-related safety obligations; on the other hand, Hoare logic can not handle pointer operations directly. The pointer logic extends traditional Hoare logic with new predicates and operations, and presents new deduction rules. The pointer logic has been implemented in our prototype certifying compiler and has been employed to prove some nontrivial pointer programs. This thesis proves pointer logic soundness with respect to operational semantics.This thesis investigates the application of the pointer logic to a small object-oriented language. To be specific, this thesis designs a small object-oriented language Cool, presents its syntax, static and dynamic semantics. Comparing with the pointer logic for PointerC, the pointer logic for Cool can also serve as a static garbage detection tool, which is capable to detect garbages in two ways: stack-allocation and static detection. Stack-allocation reduces the existence of garbage by allocating objects on stacks, instead of in heaps. And static garbage could detect some static garbages at compile time.The work presented in this thesis is the first step to the investigation of property proving-based software safety research. And this work provides a method to the safety verifications of larger and more practical saftware systems.