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

• 作者: 华保健 李兆鹏 王志芳 葛琳 陈意云
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 软件安全 语言设计 类型系统 Hoare逻辑 指针逻辑
• 年，卷（期）: 2008,（4）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 556-564
• 页数: 9页
• 分类号: TP301
• 字数: 9659字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2008.04.002

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学苏州研究院软件安全实验室	83	854	16.0	26.0
2	华保健	中国科学技术大学计算机科学技术系	17	116	6.0	10.0
3	王志芳	中国科学技术大学苏州研究院软件安全实验室	5	75	5.0	5.0
4	李兆鹏	中国科学技术大学计算机科学技术系	17	99	7.0	9.0
5	葛琳	中国科学技术大学计算机科学技术系	10	83	6.0	9.0