安全语言PointerC的设计及形式证明

作     者：华保健 陈意云 李兆鹏 王志芳 葛琳 江苏苏州215123 HUA Bao-Jian;CHEN Yi-Yun;LI Zhao-Peng;WANG Zhi-Fang;GE Lin

作者机构：中国科学技术大学苏州研究院软件安全实验室 

出 版 物：《计算机学报》 (Chinese Journal of Computers)

年 卷 期：2008年第31卷第4期

页      面：556-564页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金(60673126) Intel中国研究中心资助 

主　　题：软件安全 语言设计 类型系统 Hoare逻辑 指针逻辑 

摘      要：程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(side conditions),这些副条件本质上是约束程序语法表达式值的逻辑公式.该文证明了PointerC语言的安全性定理,即满足这些副条件的程序,在执行时不会违反语言的安全策略.为静态推理副条件中涉及指针的命题,作者已经提出了一种指针逻辑(pointer logic),文中证明了指针逻辑对操作语义是可靠的.