ISSN 1000-9825,CODEN RUXUEW E-mail:jos@iscas.ac.cn Journal of Sofnware,Vol.21,No.2,February 2010,pp.334-343 http://www.jos.org.cn doi:10.3724/SP.J.1001.2010.03783 Tel/Fax:+86-10-62562563 by Institute of Softare,the Chinese Academy of Sciences.All rights reserved. 处理指针相等关系不确定的指针逻辑 梁红瑾，张星5，陈意云中，李光鹏，华保健5 '(中国科学技术大学计算机科学与技术学院，安徽合肥230026) (中因科学技术大学软件学院，安徽合肥230026) (中国科学技术大学苏州研究院软件安全实验室，江苏苏州215123) Pointer Logic Dealing with Uncertain Equality of Pointers LIANG Hong-Jin'3,ZHANG Yu'3,CHEN Yi-Yun'3,LI Zhao-Peng'3.HUA Bao-Jian23 (School of Computer Science and Technology,University of Science and Technology of China,Hefei230026,China) (School of Software Engineering,University of Science and Technology of China,Hefei 230026,China) (Software Security Lab.,Suzhou Institute for Advanced Study,University of Science and Technology of China,Suzhou 215123.China) +Corresponding author:E-mail:Ihj1018@mail.ustc.edu.cn,http://kyhcs.ustcszedu.cn Liang HJ,Zhang Y,Chen YY,Li ZP,Hua BJ.Pointer logic dealing with uncertain equality of pointers. Journal of Sofrware,2010,21(2):334-343.http://www.jos.org.cn/1000-9825/3783.htm Abstract:A pointer logic is designed for a C-like programming language PointerC.The pointer logic is an extension of Hoare logic,and it uses the idea of precise alias analysis in pointer program verification to support safety verification of programs in which equality of pointers is well-regulated.This paper presents an extension to the pointer logic by introducing a set of uncertain-equality pointer access path sets,so as to reason in the extended pointer logic about properties of programs which manipulate data structures like directed graph in which equality of pointers is uncertain. Key words:software safety;Hoare logic;pointer logic 摘要：为类C小语言PointerC设计的指针逻辑是Hoare逻辑的一种扩展，可用来对指针程序进行精确的指针分 析，以支持指针相等关系确定的程序的安全性验证通过增加相等关系不确定的指针类型访问路径集合，可扩展这种 指针逻辑，使得扩展后的指针逻辑可以应用于有向图等指针相等关系不确定的抽象数据结构上的指针程序性质 证明 关键词：软件安全；Hoare逻辑：指针逻辑 中图法分类号：TP311 文献标识码：A 随着软件日益广泛的使用，软件的安全性也日益重要形式程序验证技术为证明程序安全性提供了一种方 法.Hoare逻辑是目前使用广泛的证明命令式语言程序性质的方法，但是Hoare逻辑在处理赋值语句时的代换只 会影响断言中涉及的特定变元虽然可以很容易地扩展它，使它能够确定一些较简单的别名关系，但它很难处理 别名关系复杂的指针程序 Supported by the National Natural Science Foundation of China under Grant Nos.90718026,60928004(国家自然科学基金) Received 2009-06-14;Revised 2009-09-11;Accepted 2009-12-07 ©中国科学院软件研究所http:www.c-s-a.org.cnISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn Journal of Software, Vol.21, No.2, February 2010, pp.334−343 http://www.jos.org.cn doi: 10.3724/SP.J.1001.2010.03783 Tel/Fax: +86-10-62562563 © by Institute of Software, the Chinese Academy of Sciences. All rights reserved. 处理指针相等关系不确定的指针逻辑∗ 梁红瑾1,3+, 张 昱1,3, 陈意云1,3, 李兆鹏1,3, 华保健2,3 1 (中国科学技术大学 计算机科学与技术学院,安徽 合肥 230026) 2 (中国科学技术大学 软件学院,安徽 合肥 230026) 3 (中国科学技术大学 苏州研究院 软件安全实验室,江苏 苏州 215123) Pointer Logic Dealing with Uncertain Equality of Pointers LIANG Hong-Jin1,3+, ZHANG Yu1,3, CHEN Yi-Yun1,3, LI Zhao-Peng1,3, HUA Bao-Jian2,3 1 (School of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China) 2 (School of Software Engineering, University of Science and Technology of China, Hefei 230026, China) 3 (Software Security Lab., Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123, China) + Corresponding author: E-mail: lhj1018@mail.ustc.edu.cn, http://kyhcs.ustcsz.edu.cn Liang HJ, Zhang Y, Chen YY, Li ZP, Hua BJ. Pointer logic dealing with uncertain equality of pointers. Journal of Software, 2010,21(2):334−343. http://www.jos.org.cn/1000-9825/3783.htm Abstract: A pointer logic is designed for a C-like programming language PointerC. The pointer logic is an extension of Hoare logic, and it uses the idea of precise alias analysis in pointer program verification to support safety verification of programs in which equality of pointers is well-regulated. This paper presents an extension to the pointer logic by introducing a set of uncertain-equality pointer access path sets, so as to reason in the extended pointer logic about properties of programs which manipulate data structures like directed graph in which equality of pointers is uncertain. Key words: software safety; Hoare logic; pointer logic 摘 要: 为类 C 小语言 PointerC 设计的指针逻辑是 Hoare 逻辑的一种扩展,可用来对指针程序进行精确的指针分 析,以支持指针相等关系确定的程序的安全性验证.通过增加相等关系不确定的指针类型访问路径集合,可扩展这种 指针逻辑,使得扩展后的指针逻辑可以应用于有向图等指针相等关系不确定的抽象数据结构上的指针程序性质 证明. 关键词: 软件安全;Hoare 逻辑;指针逻辑 中图法分类号: TP311 文献标识码: A 随着软件日益广泛的使用,软件的安全性也日益重要.形式程序验证技术为证明程序安全性提供了一种方 法.Hoare 逻辑是目前使用广泛的证明命令式语言程序性质的方法,但是 Hoare 逻辑在处理赋值语句时的代换只 会影响断言中涉及的特定变元.虽然可以很容易地扩展它,使它能够确定一些较简单的别名关系,但它很难处理 别名关系复杂的指针程序. ∗ Supported by the National Natural Science Foundation of China under Grant Nos.90718026, 60928004 (国家自然科学基金) Received 2009-06-14; Revised 2009-09-11;Accepted 2009-12-07