Automated verification of pointer programs in pointer logic

Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic – Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool – plcc was implemented to automatically verify a number of non-trivial pointer programs.     

空指针解引用错误检测的静态方法研究

空指针解引用是C语言中的一类常见的动态内存错误。Manevich R等提出了一种适用于检测空指针解引用错误的后向分析方法。本文将后向分析的思想和流敏感、上下文敏感的指针分析结合在一起,给出了一种需求驱动的空指针解引用检测静态分析算法。该算法首先由指针分析获得别名信息,然后针对所关心的数据做后向数据流分析,追踪数据传递的源头,以确定程序中的表达式是否产生解引用错误。我们在SUIF2平台上实现了这一算法。实验结果表明,算法具有较高的检测精度。     

一个用于指针程序验证的自动定理证明器的设计与实现

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.     

Precise Call Graphs for C Programs with Function Pointers

The use of pointers presents serious problems for software productivity tools for software understanding, restructuring, and testing. Pointers enable indirect memory accesses through pointer dereferences, as well as indirect procedure calls (e.g., through function pointers in C). Such indirect accesses and calls can be disambiguated with pointer analysis. In this paper we evaluate the precision of one specific pointer analysis (the FA pointer analysis by Zhang et al.) for the purposes of call graph construction for C programs with function pointers. The analysis is incorporated in a production-strength code-browsing tool from Siemens Corporate Research in which the program call graph is used as a primary tool for code understanding.The FA pointer analysis uses an inexpensive, almost-linear, flow- and context-insensitive algorithm. To measure analysis precision, we compare the call graph constructed by this analysis with the most precise call graph obtainable by a large category of existing pointer analyses. Surprisingly, for all our data programs the FA analysis achieves the best possible precision. This result indicates that for the purposes of call graph construction, inexpensive pointer analyses may provide precision comparable to the precision of expensive pointer analyses.     

A bottom-up pointer analysis using the update history

Pointer analysis is an important part for the source code analysis of C programs. In this paper, we propose a bottom-up and flow- and context-sensitive pointer analysis algorithm, where bottom-up refers to the ability to perform the analysis from callee modules to caller modules. Our approach is based on a new modular pointer analysis domain named the update history that can abstract memory states of a procedure independently of the information on aliases between memory locations and keep the information on the order of side effects performed. Such a memory representation not only enables the analysis to be formalized as a bottom-up analysis, but also helps the analysis to effectively identify killed side effects and relevant alias contexts. The experiments performed on a pilot implementation of the method shows that our approach is effective for improving the precision of a client analysis.     

Efficient binary transfer of pointer structures

This paper presents a pair of algorithms for output and input of pointer structures in binary format. Both algorithms operate in linear space and time. They have been inspired by copying garbage collection algorithms, and make similar assumptions about the representations of pointer structures. In real programs, the transfer of entire pointer structures is often inappropriate. The algorithms are extended to transfer partitions of a pointer structure lazily: the receiver requests partitions when it needs them. A remote procedure call mechanism is presented that uses the binary transfer algorithms for communicating arguments and results. A use of this as an enabling mechanism in the implementation of a software engineering environment is discussed.     

A pointer logic and certifying compiler

Proof-Carrying Code brings two big challenges to the research field of programming languages. One is to seek more expressive logics or type systems to specify or reason about the properties of low-level or high-level programs. The other is to study the technology of certifying compilation in which the compiler generates proofs for programs with annotations. This paper presents our progress in the above two aspects. A pointer logic was designed for PointerC (a C-like programming language) in our research. As an extension of Hoare logic, our pointer logic expresses the change of pointer information for each statement in its inference rules to support program verification. Meanwhile, based on the ideas from CAP (Certified Assembly Programming) and SCAP (Stack-based Certified Assembly Programming), a reasoning framework was built to verify the properties of object code in a Hoare style. And a certifying compiler prototype for PointerC was implemented based on this framework. The main contribution of this paper is the design of the pointer logic and the implementation of the certifying compiler prototype. In our certifying compiler, the source language contains rich pointer types and operations and also supports dynamic storage allocation and deallocation.     

基于属性可靠分析的空指针引用缺陷检测

为实现基于静态分析技术充分地检测出C程序中的空指针引用缺陷,提出了一种基于属性可靠分析的缺陷检测方法。首先介绍了空指针引用缺陷模式及特征。然后针对空指针引用缺陷的检测特点提出了属性可靠分析理论,并将指针的指向属性描述为一个属性格。通过提出的抽象内存模型,基于给出的每种程序语句上的迁移实现指针指向属性的可靠分析,根据得到的每个被引用指针的指向属性进而实现空指针引用缺陷的检测。通过对五个实际工程的检测结果分析表明,方法可充分检测出C程序的空指针引用缺陷。     

A low-level memory model and an accompanying reachability predicate

Reasoning about program heap, especially if it involves handling unbounded, dynamically heap-allocated data structures such as linked lists and arrays, is challenging. Furthermore, sound analysis that precisely models heap becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software. The reachability predicate has already proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. In this paper, we present a memory model suitable for reasoning about low-level pointer operations that is accompanied by a formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present our experience with a prototype verifier on a set of illustrative C benchmarks.