栈指针程序的形式验证

Formal Verification of Stack Pointer Programs

提出一种验证含栈指针、静态区指针操作的C语言程序的方法.该方法定义指针的三元属性表示一个指针的状态.指针的三元属性包括指针指向数据块的名称、数据块的长度以及指针在所指向数据块上的偏移.通过对Hoare逻辑的扩展,基于指针的三元属性设计了相应的断言演算规则和演算过程中生成验证条件的方法.该方法可以解决访问路径别名判断、指针越界访问检查、非法指针解引用检查等问题.该方法已经在一个基于演绎推理的安全C语言验证系统中实现,并且成功验证了教材上常用的一些经典算法.

This paper proposes a method for verifying C programs involving operations of stack pointers and static area pointers. To represent the state of a pointer,the method defines the triple-attribute for it,which includes the name and size of the data block that the pointer points to, as well as the offset of the pointer on the data block. By extending Hoare logic, we have designed assertion calculus rules for generating verification conditions based on the triple-attribute. The method is capable of detecting path alias, wild pointer and illegal pointer de-reference. A verification system for C programs based on deductive reasoning has implemented the method and successfully implemented some classic algorithms in textbooks.