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

Design and Proof of a Safe Programming Language PointerC

作　　者：华保健 陈意云 李兆鹏 王志芳 葛琳 江苏苏州215123 

机构地区：[1]中国科学技术大学苏州研究院软件安全实验室

出　　处：《计算机学报》2008年第4期556-564,共9页Chinese Journal of Computers

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

摘　　要：程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(side conditions),这些副条件本质上是约束程序语法表达式值的逻辑公式.该文证明了PointerC语言的安全性定理,即满足这些副条件的程序,在执行时不会违反语言的安全策略.为静态推理副条件中涉及指针的命题,作者已经提出了一种指针逻辑(pointer logic),文中证明了指针逻辑对操作语义是可靠的.The safety property of programming languages plays a fundamental role in the design and implementation of safety-critical software systems. And the authors have made investigation towards the design and proof of safe languages suitable for system programming. This paper presents the design of a C-like imperative programming language PointerC. One novelty of PointerC is that typing rules in its type system are accompanied by logic propositions which are called side conditions. And this paper proves PointerC is safe--The executions of programs will not vio- late the safety policy of the language, if these side conditions hold. A pointer logic, as an extension of Hoare logic, has been designed for the purpose of proving pointer-related side conditions statically. This paper presents the soundness proof for the pointer logic.

关 键 词：软件安全 语言设计 类型系统 HOARE逻辑 指针逻辑 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]