第31卷第3期 计 算机学报 Vol.31 No.3 2008年3月 CHINESE JOURNAL OF COMPUTERS Mar.2008 一种用于指针程序安全性证明的指针逻辑 陈意云华保健葛 琳王志芳 (中国科学技术大学计算机科学与技术系合肥230026) (中国科学技术大学苏州研究院软件安全实验室江苏苏州215123) 摘要在高可信软件的各种性质中，安全性是被关注的重点，其中软件满足安全策略的证明方法是研究的热点 之一，文中根据作者所设想的安全程序的设计和证明框架，为类C语言的一个子集设计了一个指针逻辑系统.该逻 辑系统是Hoae逻辑系统的一种扩展，它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指 针程序进行精确的指针分析，所获得的信息用来证明指针程序是否满足定型规则的附加条件，以支持程序的安全 性验证.该逻辑系统也可用来证明指针程序的其它性质. 关键词软件安全；指针逻辑；Hoare逻辑；指针分析：类型系统 中图法分类号TP301 A Pointer Logic for Safety Verification of Pointer Programs CHEN Yi-Yun HUA Bao-Jian GE Lin WANG Zhi-Fang (Department of Computer Science.University of Science and Technology of China.Hefei 230026) (So ftware Security Laboratory.Suzhou Institute for Advanced Study. University of Science and Technology of China.Suzhou.Jiangsu 215123) Abstract Safety is an important issue among the properties of high-assurance software and de- veloping the verification methods for software to meet safety policies is one of the hot research.In terms of the authors'sketch of design and verification of safety programs,a pointer logic system is designed for a subset of C-like language.This logic system is an extension of Hoare logic sys- tem and inference rules are designed to express the modification of pointer information for every kind of statements.It can be used for accurate pointer analysis of pointer programs.The informa- tion from the analysis can be used to verify if pointer programs satisfy the side conditions of typ- ing rules and then support safety verification for programs.The logic system can also be used to verify other properties of pointer programs. Keywords software safety;pointer logic;Hoare logic;pointer analysis;type system 引起危险、灾难的能力，而security是指软件系统对 引 数据和信息提供保密性、完整性、可用性、真实性保 障的能力.本文所讲的安全性主要是指safety,但是 在高可信的各种要求中，安全性（包括safety和 软件的safety和security是有联系的，黑客通常就 security)是关注的重点.Safety是指软件运行时不 是利用缓冲区溢出、数组访问越界、悬空指针访问等 收稿日期：2006-06-13：最终修改稿收到日期：2007-12-03.本课题得到国家自然科学基金(60673126)资助.陈意云，男，1946年生，教授， 博士生导师，主要研究领域为程序设计语言的理论和实现技术，形式描述技术、软件安全.E-mail:yiyun(@ustc.edu.cm.华保健，男，l979 年生，博士研究生，主要研究方向为程序验证、程序逻辑和软件安全.葛琳，女，19？9年生，博士研究生，主要研究方向为程序验证，软件 安全，类型理论和系统.王志芳，男，1982年生，博士研究生，主要研究方向为软件安全、程序逻辑和程序验证.书 第３１卷 第３期 ２００８年３月 计 算 机 学 报 ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳ Ｖｏｌ．３１ Ｎｏ．３ Ｍａｒ．２００８ 收稿日期：２００６０６１３；最终修改稿收到日期：２００７１２０３．本课题得到国家自然科学基金（６０６７３１２６）资助．陈意云，男，１９４６年生，教授， 博士生导师，主要研究领域为程序设计语言的理论和实现技术、形式描述技术、软件安全．Ｅｍａｉｌ：ｙｉｙｕｎ＠ｕｓｔｃ．ｅｄｕ．ｃｎ．华保健，男，１９７９ 年生，博士研究生，主要研究方向为程序验证、程序逻辑和软件安全．葛 琳，女，１９７９年生，博士研究生，主要研究方向为程序验证、软件 安全、类型理论和系统．王志芳，男，１９８２年生，博士研究生，主要研究方向为软件安全、程序逻辑和程序验证． 一种用于指针程序安全性证明的指针逻辑 陈意云 华保健 葛 琳 王志芳 （中国科学技术大学计算机科学与技术系 合肥 ２３００２６） （中国科学技术大学苏州研究院软件安全实验室 江苏 苏州 ２１５１２３） 摘 要 在高可信软件的各种性质中，安全性是被关注的重点，其中软件满足安全策略的证明方法是研究的热点 之一．文中根据作者所设想的安全程序的设计和证明框架，为类 Ｃ语言的一个子集设计了一个指针逻辑系统．该逻 辑系统是 Ｈｏａｒｅ逻辑系统的一种扩展，它用推理规则来表达每一种语句引起指针信息的变化情况．它可用来对指 针程序进行精确的指针分析，所获得的信息用来证明指针程序是否满足定型规则的附加条件，以支持程序的安全 性验证．该逻辑系统也可用来证明指针程序的其它性质． 关键词 软件安全；指针逻辑；Ｈｏａｒｅ逻辑；指针分析；类型系统 中图法分类号 ＴＰ３０１ 犃犘狅犻狀狋犲狉犔狅犵犻犮犳狅狉犛犪犳犲狋狔犞犲狉犻犳犻犮犪狋犻狅狀狅犳犘狅犻狀狋犲狉犘狉狅犵狉犪犿狊 ＣＨＥＮ ＹｉＹｕｎ ＨＵＡＢａｏＪｉａｎ ＧＥＬｉｎ ＷＡＮＧＺｈｉＦａｎｇ （犇犲狆犪狉狋犿犲狀狋狅犳犆狅犿狆狌狋犲狉犛犮犻犲狀犮犲，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犎犲犳犲犻 ２３００２６） （犛狅犳狋狑犪狉犲犛犲犮狌狉犻狋狔犔犪犫狅狉犪狋狅狉狔，犛狌狕犺狅狌犐狀狊狋犻狋狌狋犲犳狅狉犃犱狏犪狀犮犲犱犛狋狌犱狔， 犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犛狌狕犺狅狌，犑犻犪狀犵狊狌 ２１５１２３） 犃犫狊狋狉犪犮狋 Ｓａｆｅｔｙｉｓａｎｉｍｐｏｒｔａｎｔｉｓｓｕｅａｍｏｎｇｔｈｅｐｒｏｐｅｒｔｉｅｓｏｆｈｉｇｈａｓｓｕｒａｎｃｅｓｏｆｔｗａｒｅａｎｄｄｅ ｖｅｌｏｐｉｎｇｔｈｅｖｅｒｉｆｉｃａｔｉｏｎｍｅｔｈｏｄｓｆｏｒｓｏｆｔｗａｒｅｔｏｍｅｅｔｓａｆｅｔｙｐｏｌｉｃｉｅｓｉｓｏｎｅｏｆｔｈｅｈｏｔｒｅｓｅａｒｃｈ．Ｉｎ ｔｅｒｍｓｏｆｔｈｅａｕｔｈｏｒｓ′ｓｋｅｔｃｈｏｆｄｅｓｉｇｎａｎｄｖｅｒｉｆｉｃａｔｉｏｎｏｆｓａｆｅｔｙｐｒｏｇｒａｍｓ，ａｐｏｉｎｔｅｒｌｏｇｉｃｓｙｓｔｅｍ ｉｓｄｅｓｉｇｎｅｄｆｏｒａｓｕｂｓｅｔｏｆＣｌｉｋｅｌａｎｇｕａｇｅ．ＴｈｉｓｌｏｇｉｃｓｙｓｔｅｍｉｓａｎｅｘｔｅｎｓｉｏｎｏｆＨｏａｒｅｌｏｇｉｃｓｙｓ ｔｅｍａｎｄｉｎｆｅｒｅｎｃｅｒｕｌｅｓａｒｅｄｅｓｉｇｎｅｄｔｏｅｘｐｒｅｓｓｔｈｅｍｏｄｉｆｉｃａｔｉｏｎｏｆｐｏｉｎｔｅｒｉｎｆｏｒｍａｔｉｏｎｆｏｒｅｖｅｒｙ ｋｉｎｄｏｆｓｔａｔｅｍｅｎｔｓ．Ｉｔｃａｎｂｅｕｓｅｄｆｏｒａｃｃｕｒａｔｅｐｏｉｎｔｅｒａｎａｌｙｓｉｓｏｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓ．Ｔｈｅｉｎｆｏｒｍａ ｔｉｏｎｆｒｏｍｔｈｅａｎａｌｙｓｉｓｃａｎｂｅｕｓｅｄｔｏｖｅｒｉｆｙｉｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓｓａｔｉｓｆｙｔｈｅｓｉｄｅｃｏｎｄｉｔｉｏｎｓｏｆｔｙｐ ｉｎｇｒｕｌｅｓａｎｄｔｈｅｎｓｕｐｐｏｒｔｓａｆｅｔｙｖｅｒｉｆｉｃａｔｉｏｎｆｏｒｐｒｏｇｒａｍｓ．Ｔｈｅｌｏｇｉｃｓｙｓｔｅｍｃａｎａｌｓｏｂｅｕｓｅｄｔｏ ｖｅｒｉｆｙｏｔｈｅｒｐｒｏｐｅｒｔｉｅｓｏｆｐｏｉｎｔｅｒｐｒｏｇｒａｍｓ． 犓犲狔狑狅狉犱狊 ｓｏｆｔｗａｒｅｓａｆｅｔｙ；ｐｏｉｎｔｅｒｌｏｇｉｃ；Ｈｏａｒｅｌｏｇｉｃ；ｐｏｉｎｔｅｒａｎａｌｙｓｉｓ；ｔｙｐｅｓｙｓｔｅｍ １ 引 言 在高可信的各种要求中，安全性（包括ｓａｆｅｔｙ和 ｓｅｃｕｒｉｔｙ）是关注的重点．Ｓａｆｅｔｙ是指软件运行时不 引起危险、灾难的能力，而ｓｅｃｕｒｉｔｙ是指软件系统对 数据和信息提供保密性、完整性、可用性、真实性保 障的能力．本文所讲的安全性主要是指ｓａｆｅｔｙ，但是 软件的ｓａｆｅｔｙ和ｓｅｃｕｒｉｔｙ是有联系的，黑客通常就 是利用缓冲区溢出、数组访问越界、悬空指针访问等