基于CEGAR的C程序空指针解引用检测

段　钊　田　聪　段振华

(西安电子科技大学计算机理论与技术研究所　西安　710071)

(ctian@mail.xidian.edu.cn)



基于CEGAR的C程序空指针解引用检测

段钊田聪段振华

(西安电子科技大学计算机理论与技术研究所西安710071)

(ctian@mail.xidian.edu.cn)

CEGAR Based Null-Pointer Dereference Checking in C Programs

Duan Zhao, Tian Cong, and Duan Zhenhua

(InstituteofComputingTheoryandTechnology,XidianUniversity,Xi’an710071)

AbstractWith the rapid growth of computer software in both scale and complexity, more and more attention has been paid by software developers on the reliability and security issue. Null-pointer dereference is a kind of errors which often occur in programs.This paper proposes a CEGAR based null-pointer dereference verification approach for C programs. With this method, first, a linear temporal logic (LTL) formula is used to specify the null-pointer dereference problem. Then whether null-pointer dereference occuring in a program is checked by a CEGAR based model checking approach. In order to verify null-pointer dereference problem in a total automatic way, this paper also studies how to generate temporal logic formulas automatically with respective to null-pointer dereference problem. Experimental results show that the proposed approach is useful in practice for checking null-pointer dereference in C programs with large scale.

Key wordsmodel checking; abstraction refinement; null-pointer dereference; program verification; temporal logic

摘要随着计算机软件规模和复杂度的日益增长，软件系统的可靠性和安全性倍受关注.空指针解引用是程序中常见的一类错误.提出了一种基于反例制导抽象精化CEGAR的C程序空指针解引用检测方法.该方法首先使用线性时序逻辑描述空指针解引用问题，然后通过抽象精化的方法检测待测程序中是否含有空指针解引用错误.为了达到完全自动验证的目标，同时针对空指针解引用问题，研究了该类性质的时序逻辑表达方法，并自动从程序中针对所有的指针变量，形成相应的时序逻辑公式.实验结果表明，所提出的方法在大规模C程序的空指针解引用检测方面有着重要的实际应用价值.

关键词模型检测；抽象精化；空指针解引用；程序验证；时序逻辑

计算机软件已深入到国防建设和国计民生的各个领域，如航天航空、工业控制、交通、医疗、教育和社交等，成为当今社会不可或缺的一部分.面对多样化的需求，软件的规模和复杂性不断增大，因而软件的可靠性和安全性更加难以得到保障.目前，大部分软件系统都存在各种各样的错误和缺陷.有的软件虽然可以正常运行，但是其内部仍然存在许多错误隐患,在特定情况下会导致软件性能下降，甚至引……