ISSN 1000-9825,CODEN RUXUEW E-mail:jos@iscas.ac.cn Journal of Sofnare,Vol.21,No.3,March 2010,pp.415-426 http://www.jos.org.cn do:10.3724/SP.J.1001.2010.03620 Tel/Fax:+86-10-62562563 by Institute of Sofnare,the Chinese Academy of Sciences.All rights reserved. 一种用于指针程序验证的指针逻辑 陈意云2，李光鹏，王志芳只，华保健中 (中国科学技术大学计算机科学与技术学院，安徽合肥230026) (中因科学技术大学苏州研究院软件安全实验室，江苏苏州215123) Pointer Logic for Verification of Pointer Programs CHEN Yi-Yun'2,LI Zhao-Peng 2+,WANG Zhi-Fang 2,HUA Bao-Jian2 (School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China) (Software Security Laboratory,Suzhou Institute for Advanced Study,University of Science and Technology of China,Suzhou 215123, China) Corresponding author:E-mail:zpli@mail.ustc.edu.cn Chen YY,Li ZP,Wang ZF,Hua BJ.Pointer logic for verification of pointer programs.Journal of Software, 2010,21(3):415-426.htp:/www.jos.org.cn/1000-9825/3620.htm Abstract:This paper improves and extends the pointer logic that has been designed for verifying pointer programs.Its main contribution is that a concept of legal sets of access paths is presented,which simplifies elementary operations on access paths and makes inference rules of the logic easier to understand.Furthermore,the logic with inference rules is extended for local reasoning and for function construction,making the logic used conveniently in the context of function calls. Key words:software safety;Hoare logic;pointer logic;proof-carrying code;certifying compiler 摘要：本文玫进并扩展先前为验证指针程序捉出的指针逻辑，主要页献是提出了合法访问路径集合的概念，极 大地简化了访问路径上的基本运算，并使得指针逻辑推理规则变得易理解.另外，增加了局部推理规则和函数构造的 推理规则，使得指针逻辑可以方便地用于有函数调用的场合. 关键词：软件安全；Hoare逻辑，指针逻辑；携带证明的代码，出具证明的编译器 中图法分类号：TP301文献标识码：A 携带证明的代码(proof-carrying code,简称PCC)I作为一种新的代码范型(paradigm),给编程语言的研究领 域带来了巨大挑战：其一是寻找表达力更强的逻辑或类型系统来规范或推理高级语言或低级语言程序的性质： 其二是研究出具证明的编译技术， 对于第1个挑战，类型化汇编语言四和类型细化的理论)是两种基于类型方式的典型研究，而PCC、携带基 础逻辑证明的FPCC(foundational proof-carrying code)、经过验证的汇编编程CAP(certifying assembly programming)和基于栈的经过验证的汇编编程SCAP(stack-based certifying assembly programming)是基于 逻辑方式的典型研究基于类型的技术和基于逻辑的技术是互补的，近年来，一些研究人员倾向于组合这两种技 ·Supported by the National Natural Science Foundation of China under Grant Nos.90718026,60928O04(国家自然科学基金) Received 2008-01-16;Accepted 2009-03-31 ©中国科学院软件研究所htp:wwv.c-s-a.org.cnISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn Journal of Software, Vol.21, No.3, March 2010, pp.415−426 http://www.jos.org.cn doi: 10.3724/SP.J.1001.2010.03620 Tel/Fax: +86-10-62562563 © by Institute of Software, the Chinese Academy of Sciences. All rights reserved. 一种用于指针程序验证的指针逻辑∗ 陈意云 1,2, 李兆鹏 1,2+, 王志芳 1,2, 华保健 1,2 1 (中国科学技术大学 计算机科学与技术学院,安徽 合肥 230026) 2 (中国科学技术大学 苏州研究院 软件安全实验室,江苏 苏州 215123) Pointer Logic for Verification of Pointer Programs CHEN Yi-Yun1,2, LI Zhao-Peng1,2+, WANG Zhi-Fang1,2, HUA Bao-Jian1,2 1 (School of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China) 2 (Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123, China) + Corresponding author: E-mail: zpli@mail.ustc.edu.cn Chen YY, Li ZP, Wang ZF, Hua BJ. Pointer logic for verification of pointer programs. Journal of Software, 2010,21(3):415−426. http://www.jos.org.cn/1000-9825/3620.htm Abstract: This paper improves and extends the pointer logic that has been designed for verifying pointer programs. Its main contribution is that a concept of legal sets of access paths is presented, which simplifies elementary operations on access paths and makes inference rules of the logic easier to understand. Furthermore, the logic with inference rules is extended for local reasoning and for function construction, making the logic used conveniently in the context of function calls. Key words: software safety; Hoare logic; pointer logic; proof-carrying code; certifying compiler 摘 要: 本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极 大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的 推理规则,使得指针逻辑可以方便地用于有函数调用的场合. 关键词: 软件安全;Hoare 逻辑;指针逻辑;携带证明的代码;出具证明的编译器 中图法分类号: TP301 文献标识码: A 携带证明的代码(proof-carrying code,简称 PCC)[1]作为一种新的代码范型(paradigm),给编程语言的研究领 域带来了巨大挑战:其一是寻找表达力更强的逻辑或类型系统来规范或推理高级语言或低级语言程序的性质; 其二是研究出具证明的编译技术. 对于第 1 个挑战,类型化汇编语言[2]和类型细化的理论[3]是两种基于类型方式的典型研究,而 PCC、携带基 础逻辑证明的 FPCC(foundational proof-carrying code)[4]、经过验证的汇编编程 CAP(certifying assembly programming)[5]和基于栈的经过验证的汇编编程 SCAP(stack-based certifying assembly programming)[6]是基于 逻辑方式的典型研究.基于类型的技术和基于逻辑的技术是互补的,近年来,一些研究人员倾向于组合这两种技 ∗ Supported by the National Natural Science Foundation of China under Grant Nos.90718026, 60928004 (国家自然科学基金) Received 2008-01-16; Accepted 2009-03-31