（计算机软件与理论专业论文）一种用于指针程序安全性证明的指针逻辑.pdf

摘要 摘要 在社会逐渐走入信息时代的今天，社会的各个层面，包括工业界、政府机 关、学校、商业部门等，都和计算机软件等信息系统结合越来越紧密。信息系 统中的任何一个环节工作失败或是遭受攻击都会带来难以预料的灾难性后果， 因而软件安全的重要性与日俱增。用形式化的方法对软件进行严格推理是提高 软件质量的根本途径。在众多的形式化方法中，近十年来基于程序设计语言理 论和实现技术的软件安全研究引起了广泛的关注。基于语言理论的研究从程 序基础出发考虑软件安全，有利于减小运算系统的受信任计算基础( n u s t e d c o m p u t i n gb a s e ，简称t c b ) 。 未来高安全软件设计和开发的一种行之有效的方式将是基于程序性质证明 的开发框架。在这个框架中，程序设计者将软件的安全策略等描述成程序应满 足的规范，连同程序一起提交给编译器；编译器生成为证明程序满足规范所需 的验证条件，并且利用内嵌的定理证明器自动地或交互地证明这些验证条件； 编译器在把源程序翻译成目标代码的同时，将源程序满足规范的证明翻译成目 标代码满足等效规范的证明，这样的编译器称为出具证明的编译器( c e r t i f y i n g c o m p i l e r ) ；在目标代码一级由证明检验器利用代码所携带的证明自动进行代 码满足规范的检验。该框架的主要优点是，它向程序设计者提供源级而不是目 标级的程序性质证明方法，以提高安全程序的开发效率，同时它将编译器、证 明器等排除出受信任的计算基础，以尽量缩小系统的t c b 。 作为上述基于程序性质证明的软件安全长期研究工作的一个环节和组成部 分，本文在指针逻辑以及基于指针逻辑的源代码性质描述和性质证明方面做了 有益探索。 本文首先研究了一个强调指针类型的类c 的命令式语言源语言p o i n t e r c 的 设计并给出了它的安全性证明。p o i n t e r c 语言设计的主要出发点是：已有软件 安全和出具证明编译的研究大多集中在类型安全等简单安全策略上；而本文研 究的高安全程序设计框架关注更实际、更丰富的安全策略，如内存安全等，因 此，p o i n t e r c 保留了c 语言指针特性。本文给出了一种易于程序员理解的安全语 言描述方式，并尝试以类型系统和逻辑系统相结合的静态机制来推理程序的 安全性。本文利用辅助定理证明工具c o q ，机械证明了p o i n t e r c 语言的安全性定 理。 本文研究了一种指针逻辑系统。指针逻辑扩展了传统h o 盯e 逻辑，并加入了 新的推理规则以支持对指针操作的推理，因此指针逻辑为证明指针程序的安全 性提供了可行的途径。本文给出了针逻辑系统在一个出具证明编译器原型系统 中的实现，该原型证明系统包括一个验证条件生成器和定理证明器，能够根据 摘要 指针逻辑的公理和推理规则，自动完成断言的生成和证明；并且，这些代码、 断言和证明可以被出具证明的编译器继续翻译到目标语言级。本文利用辅助定 理证明工具c o q ，机械证明了指针逻辑对于操作语义的可靠性定理。 本文研究了指针逻辑在面向对象语言上的应用。本文设计了一个小的面 向对象语言c o o i 并定义了它的形式语义；c o o i 保留了j a v a 语言核心的的语法元 素，如类、对象、继承等。本文扩展了指针逻辑以增加对这些新语言特性的支 持。除了作为通用的程序逻辑外，本文还研究了指针逻辑在静态垃圾判断方面 的应用。具体的，本文研究了指针逻辑判断静态垃圾的两种典型应用：栈分配 和静态垃圾判断。栈分配可以通过把对象分配到栈而不是堆上，有效的减少垃 圾的产生；而静态垃圾判断可以静态判断堆上的垃圾。 本文的研究工作是对基于程序性质证明的安全软件开发框架的初步探索， 但本文所研究的以指针逻辑为基础的程序性质证明方法为更大规模和更实际的 软件系统安全性证明提供了一条可行的途径。 关键词：软件安全程序性质证明h o a r e 逻辑指针逻辑验证框架 a b s t r a c t a b s t r a c t n o w a d a y s ，i n f o r m a t i o nt e c h n o l o g i e sp l a ym o r ea n dm o r ei m p o r t a n tr o l e si n a l la u s p e c t so fo u rw o r l d ： i n d u s t r i e s ，g o v e r n m e n t s ，b u s s i n e s s ，a n ds c h o o l s o n c e an o d ei nt h i sn e t w o r kc o l l a p s e s ，a ne x p e n s i c ec a t a s t r o p h ew d u l dh a p p e n a sa r e s u l t ，t h er e q u i r e m e n tf o rs o f t w a r es a f 宅t ya n ds e c u r i t yb e c o m e sm o r ea n dm o r e u r g e n t t bm o d e r a t et h i sd i s p a r i t y ，d e v e l o p i n gh i g h a s s u r a n c es o f t w a r eb a s e d o nf o r m a lm e t h o d si sa ne s s e n t i a la p p r o a c h a m o n gv a r i o u sf o r m a lm e t h o d s ， l a n g u a g e b a s e da p p r o a c ht os 0 f t w a r es e c u r i t yh a sa t t r a c t e dw i d e s p r e a da t t e n t i o n i nt h ep a s td e c a d e t h e s ea p p r o a c h e sh e l pr e d u c et h e7 r r u s t e dc o m p u t i n gb a s e o fs o f t w a r es y s t e m sb ys t a r t i n gf r o mt h eb a s eo fs o f t w a r e ，t h a ti s ，p r o g r a m m i n g l a n g u a g e sa n dc o m p i l e r s o n ep r o m i s i n ga p p r o a c hf o rh i g hs e c u r es o f t w a r ed e v e l o p m e n ti nt h ef u t u r ei s t h es o f t w a r ep r o p e r t yp r o v i n 分b a s e df r a m e 、o r k i nt h i sf r a m e w o r k ，p r o 伊a m m e r s d e s i g ns a f e t yp o l i c i e sa n dd e c r i b et h e ma ss o f t w a r es p e c i f i c a t i o n s ，w h i c ha r ef e d t ot h ec o m p i l e r sa l o n gw i t hn o r m a lp r o g r a mc o d e i no r d e rt op r o 、，et h e s ep r o - g r 锄ss a t i s f yt h e s es p e c i f i c a t i o n s ，t h ec o m p i l e rg e n e r a t e sv e r i f i c a t i o nc o n d i t i o n s ， w h i c ha r ep r o v e da u t o m a t i c a l l yo ri n t e r a t i v e l yb yt h ep r o g r a m m e r s ac o m p i l e r t r a n s i a t e st h e s ep r o g r a mc o d e ，a l o n gw i t ht h o s ev e r i f i c a t i o nc o n d i t i o n sa n dp r o o f s ， a n ds u c hk i n do fc o m p i l e r sa r ec a l l e dc e r t i f y i n gc o m p i l e r a tt h ea s s e m b l yl e v e l ， a ni n d 印e n d e n tp r o o fc h e c k e rc h e c l ( st h eo b j e c tc o d et oe n s u r ei t s a t i s f yi t ss p e c i f i c a t i o n s t h ek e yb e n i f i to ft h i sf r a m e w o r ki st h a ti to 艉r ss o u r c e l e v e lp r o o f m e t h o d s ，i i l s t e a do fa ta s s e m b l y l e v d ，w h j c hm a k e st h ep r o c e s so fp r o g r 锄d 争 v e l o p m e n tm o r ee 艉c i e n t m e a i l w h i l e ，m a k i n gu s eo fac e r t i f i n gc o m p i l e rg r e a t l y r e d u c e st h et r u s t e dc o m p u t i n gb a s eb yr e m o v i n gt h ec o m p i e ra n dp r o v e rf r o mt h e t c b a sa ni n t e g r a lp a r to ft h ea b o v ef a m e 、o r k ，t h 诘t h e s i si n v e s t i g a t e sp o i n t e r l o g i ca n di t sa p p l i c a t i o nt os o u r c ec o d ep r o v i n g t h i st h e s i sd e s i g i l sp o i n t e r c ，ac h k ei m p e r a t i v el a n g u a g ew h i c hr e t a i n sc se x p l i c i tm e m o r ym a n a g e m e n tf a c i l i t i e s t h ep r i m a r yd e s i g nm o t i v 玑i o nf o rp o i n t e r ci so u rg o a lt os t u d ym o r ee x p r e s s i v e s a f b t y ep o l i e sb e y o n dt y p e8 a f e t ys u c ha sm e m o r ys a f e t y a n dt h i st h e s i sm a k e s u s eo fas t a t i cd i s c i p l i n ec o m b i n i n gt y p es y s t e ma n dp o i n t e rl o g i cs y s t e m t h i st h e s i sp r o p o s e san o v e lp r o g r a ml o g i c ，i e ，t h ep o i n t e rl o g i c t h ep r i m a r y9 0 8 lf o rt h ed e s i g no fp o i n t e rl o g i ci s ：o no nh a n d ，t r 8 d i i o n a lt y p es y s t e m a r e ，e a ka n dc o u l dn o tc h e c kt h ev 甜u e - r e l a t e ds a f 爸t yo b l i g a 上i o n s ；o nt h eo t h e r l i l a 1 ) s t r a c t h a n d ，h o a r el o g i cc a nn o th a n d l ep o i n t e ro p e r a t i o n sd i r e c t l y t h ep o i n t e rl o g i c e x t e n d st r a d i t i o n a lh o a r el o g i cw i t hn e wp r e d i c a t e sa n do p e r a t i o n s la n dp r e s e n t s n e wd e d u c t i o nr u i e s t h ep o i n t e rl o g i ch a sb e e ni m p l e m e n t e di no u rp r o t o t y p e c e r t i f y i n gc o m p i l e ra n dh a sb e e ne m p l o y e dt op r o v es o m en o n t r i v i a lp o i n t e rp r 伊 g r a m s t h i st h e s i sp r o v e sp o i n 七e ri o g j cs o u n d n e s sw i t hr e s p e c tt o0 p e r a t i o n a l s e m a n t j c s t h i st h e s i si n v e s t i g a t e st h ea p p l i c a t i o no ft h ep o i n t e rl o g i ct oas m a l lo b j e c t o r i e n t e dl a n g u a g e i bb es p e c i f i c ，t h i st h e s i sd e s i g n sas m a l lo b j e c t o r i e n t e dl a n g u a g ec o o l ，p r e s e n t si t ss y n t a x ，s t a t i ca ，n dd y n a m i cs e m a n t i c s c o m p a r i n gw i t h t h ep o i n 扛e rl o g i cf o rp o j n t e r c ，t h ep o i n t e rl o g i cf b rc o o ic a na i s os e r v ea sas t a t i c g a r b a g ed e t e c t i o nt o o l ，w h i c hi sc a p l b l et od e t e c tg a r b a g e si nt w ow a y s ：s t a c k - a l i o c a t i o na n ds t a t i cd e t e c t i o n s t a c k a u o c a t i o nr e d u c e st h ee x i s t e n c eo fg a r b a g e b ya l l o c a t i n go b j e c t so ns t a c k s ，i n s t e a do fi nh e a p s a n ds t a t i cg a r b a g ec o u l d d e t e c ts o m es t a t i cg a r b a g e sa tc o m p i l et i m e t h ew o r kp r e s e n t e di nt h i st h e s i si st h ef i r s ts t e pt ot h ei n v e s t i g a t i o no f p r o p e r t yp r o v i n 哥b a s e ds o f t w a r es a f e t yr e s e a r c h a n dt h i s 、v o r kp r o v i d e sam e t h o d t ot h es a f 色t yv e r i 6 c a t i o n so fl a r g e ra n dm o r ep r a c t i c a ls a f t w a r es y s t e m s k e y b r d s ：s o f t w 甜es a f b t y ，p r o g r 锄v e r 馒c a t i o n ， h o a r el o g i e ，p o i n t e rl o g i c i v 中国科学技术大学学位论文原创性和授权使用声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工作 所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含 任何他人已经发表或撰写过的研究成果。与我一同工作的同志对本 研究所做的贡献均已在论文中作了明确的说明。 本人授权中国科学技术大学拥有学位论文的部分使用权，即： 学校有权按有关规定向国家有关部门或机构送交论文的复印件和电 子版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进 行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论 文。 保密的学位论文在解密后也遵守此规定。 作者签名：姒 仞髫年衫月7 日 绪论 第1 章绪论 本文研究一种基于程序性质证明的高安全软件设计和性质证明框架。在这 个框架中，程序设计者将软件的安全策略等描述成程序应满足的规范，连同程 序一起提交给编译器；编译器生成为证明程序满足规范所需的验证条件，并且 利用内嵌的定理证明器自动地或交瓦地证明这些验证条件：编译器在把源程序 翻译成目标代码的同时，将源程序满足规范的证明翻译成目标代码满足等效 规范的证明，这样的编译器称为出具证明的编译器( c e r t i f y i n gc o m p i l e r ) ；在 目标代码一级由证明检验器利用代码所携带的证明自动进行代码满足规范的 检验。该框架的优点是，它向程序设计者提供源级而不是目标级的程序性质 证明方法，以提高安全程序的开发效率，同时它将编译器、证明器等排除出 受信任的计算基础( t r u s t e dc o m p u t i n gb a s e ，简称t c b ) ，以尽量缩小系统 的t c b 。 1 1研究背景 在社会逐渐走入信息时代的今天，社会的各个层面，包括工业界、政府 机关、学校、商业部门等，都和计算机软件等信息系统结合越来越紧密。信 息系统中的任何一个环节工作失败或是遭受攻击都会带来难以预料的灾难性 后果。数据的完整性、机密性等等性质不再仅是军用计算系统的安全要求， 而是i n t e r n e t 上日益增长的企业及个人用户的需求。因而人们对计算机习题尤 其是软件系统安全的要求日益增加。但与这种需求相对立的是目前软件系统 不尽人意的安全状况。大多数软件产品在发布时依然含有已经查出但尚未排 除的错误，更不用说还没有查出的缺陷。根据国家计算机病毒应急处理中心 ( c n c e r t c c ) 公布的一份统计报告( c n c e f 江c c ，2 0 0 7 ) ，仅在2 0 0 6 年，我 国就有超过7 4 的计算机受到计算机病毒的感染和破坏，直接经济损失数亿 元；并且，近四年国内报告的安全事件数量( 不包括扫描攻击) ，年平均增长 超过2 0 0 ，去年已超过2 6 0 0 0 件。 安全问题的形势如此严峻，最基本的原因是计算机系统存在可被渗透 ( e x p l o i t ) 的脆弱性( v u l n e r a b i l i t y ) 或者称为安全漏洞( s e c u r i t yh o l e ) 。由 绪论 法等。本节主要对这些方法和技术做简要介绍。 1 2 1类型系统 类型系统在现代程序设计语言中有着广泛的应用，并且在新语言的设计与 实现中扮演着重要的角色。近数十年来，在类型论和类型系统上的研究工作也 对软件安全的研究起了十分重要的作用。 类型系统是一种对程序短语进行分类，来保证特定程序属性的一种语法 方法。类型系统在程序开发的早期阶段就能排除许多程序错误，并且它提 供确定的类型检查算法来判定程序是否是良类型的。类型系统可靠性证明保 证了良类型的程序必然不可能出现特定的类型错误。下面以简单类型化a 演 算( b a r e n d r e 昏，1 9 8 8 ) 为例，说明类型系统的典型使用。之所以选择简单类型 化a 演算，有三个方面的重要原因：首先这个系统比较简单，但是它展示了设 计类型系统的典型方法和步骤；其次，在这个系统上可以方便的扩展新的语言 结构和类型结构，进一步形成表达力更强的系统，从而该系统形成了新语言研 究的重要基础；最后，本文在后面的章节将讨论如何给这种类型系统的定型规 则加入作为副条件的逻辑命题，从而进一步扩展类型系统的表达能力，所以， 该系统构成了本文工作的基础并形成了对比。该演算的定义在图l 一1 给出：该 表达式e 类型7 - 值u 定型环境r zla z ：7 - ee e 7 _ 7 _ a z ：7 e ir ，z ：7 - 图1 1 ：简单类型化a 演算 演算的表达式e 只包含三种形式：变量z 、函数抽象妇：7 e 和函数作用e e ；其中 值口仅包括函数抽象蛔：f e 。类型丁包括函数类型7 i 一7 一；定型环境r 是一个变量 和类型的二元组列表。该演算系统的归约规则包括三条： 纛日高易 e 1e 2 _ e je 2u le 2 + t ，le j ( a z ：7 e ) + 【口z 】e 前两条规则说明对一个函数作用的表达式进行归约时，首先必须把函数和参数 两部分都归约到值；第三条是替代规则，符号p 。】e 表示把表达式e 中所有自由 出现的z 都替换成值移。注意到，这些归约规则仅当表达式满足特定语法形式时 才有意义，例如，当且仅当函数作用的第一元能归约到函数抽象时，整个归约 3 绪论 才能继续进行。这些约束由类型系统的定型规则给出： z ：7 - f1 1 r ，z ：7 - 卜e ：7 - 7 亓磊l 亓i 函i j 习 甲 r 卜_ e 1 ：r 7 7 r 卜e 2 ：7 71 1 2 丌乏i f 一3 第三条规则保证了函数作用只能出现在良类型的表达式上。类型系统的主要特 点是关于定型规则的性质可以被表达成类型安全性定理并被严格证明，以该系 统为例，不难证明如下的前进性和保持性两条定理： 定理1 1 ( p r o g r e s s ) ： 若卜e ：7 - ，则要么e 是一个值，要么存在e 7 ，使得e e ， 定理1 2 ( p r e s e r v a t i o n ) ： 若卜e ：7 - ，且存在e 7 ，使得e _ e 7 ，则卜e ：7 。 这些定理的证明都不难根据结构化归纳完成( p i e r c e ，2 0 0 2 ) 。从这两条定理可以 得到结论，即良类型的程序肯定不会陷住( s t u c k ) 。 尽管传统的类型系统提供了如上的较强的安全保证，但是它的表达能力相 对较弱，例如它难以表达对程序中变量值有要求的安全策略。因此，近年来基 于类型方法的热点研究主要沿着着两个方向来展开：第一个方向是研究如何设 计表达力更强或者更细化的类型系统来表达更丰富程序安全性质；第二个方向 是研究如何把高层的类型系统推广到中间语言甚至汇编语言层次上。 研究者已经在第一个方面进行了许多研究工作，例如，r 0 w a n d a v i e s 和p f e n n i n g 研究了交类型( i n t e r s e c t i o nt y p e ) 和专门领域的谓词，并 用以拓展m l ( d a v i e sa n dp f e n n i n g ，2 0 0 0 ) 。x i 和p f e n n i n g 进一步提出了单元素类 型( s i n g l e t o nt y p e ) ( x ia n dp f e n n i n g ，1 9 9 9 ) 。一般来说，类型细化把同一类 型的值根据不同的性质再划分成多个子集。根据r o b e r lh a r p e r 和f r a n kp f e n - n i n g 等提出的类型细化理论( m a n d e l b a u me ta 1 ，2 0 0 3 ) ，现有的类型细化研究可 以划分为两类：一种称为索引细化( i n d e xr e f i n e m e n t ) ，另一种类型细化是数 据分类细化( d a t a s o r tr e f i n e m e n t ) 。 索引细化也是由依赖类型( d e p e n d e n tt y p e ) 引起的类型细化。依赖类型 以某个表达式的值确定一组类型表达式，从而从现有的类型符号上定义一 种新的抽象。从细化类型的角度看，依赖类型可以认为是将一种基础类型 ( b a s et y p e ) 以某个变量或表达式的值为索引划分出若干个不同的子类型。 依赖类型最早出现在自动定理证明器n u p r l 的研究中( p i e r c e ，2 0 0 2 ) 。h o n g w e i x i ( x i ，1 9 9 8 ；x ia n dp f e n n i n g ，1 9 9 8 ，1 9 9 9 ) 将和依赖类型有关的值提升到类型 层次，使程序和类型分开，从而可用于实际程序设计中。进一步，x i 等把依 赖类型用于命令式语言x a n a d u 。x a n a d u 能够捕捉诸如数组长度、链表长度 4 绪论 赋值公理；还有部分规则不是语法制导的，例如弱化规则等。另外，循环语 句的推导规则需要循环不变式。这些非语法制导的推导规则给自动生成验证条 件提出了挑战，另外，循环不变式的自动合成也是非常困难的问题，对于多数 情况，需要程序员手工标注。 h o a l r e 逻辑三元组卜 p ) s 【q 所表达的含义是：如果断言p 在代码s 执 行前成立，且s 的执行能够终止的话，则断言q 在执行后成立。为了严格陈 述h o a r e 逻辑的可靠性，要给出它的可靠性定理，及其证明。可靠性定理的证 明分成如下几个步骤：首先是形式化该语言l 的操作语义，这包括定义抽象机 器模型m 和给出作为抽象机器状态转换规则的操作语义规则；第二步是给出 逻辑命题尸在机器模型朋上的语义解释：m p ，即命题p 在机器状态m 下为 真；第三个步骤也是最后一个是证明可靠性定理：若对于机器状态朋和朋7 ， 有朋 p 和朋归约到朋7 ，且有h o a r e 三元组卜 【p 】s q _ 成立，则有朋 q 。 尽管h o a r e 逻辑在验证p a s c a l 等语言程序上取得了一些成功，但从上世纪八 十年代起，关于h o a r e 逻辑的研究陷入沉寂，许多研究者对程序验证的前景持悲 观的态度( d e m i l l oe ta 1 ，1 9 7 7 ) 。导致这种局面的主要原因有两点：首先是在验 证的过程中需要程序员手工对代码进行程序断言标注( 如循环不变式和程序规 范等) ，而由于大部分关于部分正确性的断言相对复杂，这给程序员增加了较 大的负担，而且对于较大规模的程序而言，标注的工作量繁重；第二是当时的 自动定理证明技术还不成熟，手工的证明难以保证证明过程的严格可靠。 然而，从上世纪九十年代起，以携带证明的代码( p r 0 0 f c a r r y i n gc o d e ， 简称p c c ) f n e c u l a ，1 9 9 7 ；n e c u l aa n dl e e ，2 0 0 0 ；n e c u i aa n ds c h n e c k ，2 0 0 3 ) 为代 表的一系列研究工作所取得的成功又莺新让程序验证的技术受到研究者的重 视。携带证明的代码核心的观点是：通过给可执行代码附加一个容易被严格检 查的形式安全性证明，代码的消费者可以在执行该代码以前，很容易的通过 x 绪论 样，出具证明的编译器能够自动为目标代码生成基于类型的循环不变式。除了 通常的目标代码之外，代码产生方还需要产生移动代码满足安全策略的证明。 证明产生的基本过程足：首先由验证条件生成器扫描标注了类型断言的目标代 码并产生验证条件，然后这些验证条件由自动定理证明器产生证明。 代码消费方在同时接收到带注释的目标码和证明之后，使用同样的安全策 略和同样的验证条件产生器产生验证条件。但是代码消费方并不产生证明，而 是检查代码所附带的证明是否正确。证明检查过程可以看作一个类型检查过 程，即证明是一个项，而作为逻辑命题的验证条件是该项的类型。检查证明中 的每一步推断是逻辑中的公理或是推断规则的一个实例。因为验证条件是通过 对目标码进行符号计算产生的，所以所检查的确实是实际代码满足安全策略的 证明，这可以防止恶意的代码通过携带一个合法的证明来破坏主机。 携带证明的代码是一个通用的代码验证框架，除了类型安全外，原则上还 能保证其它的可以形式化的安全策略，如内存安全、死锁性质以及资源限制在 内的各种安全性质。携带证明的代码还是一种有效的移动代码传递协议：代码 产生方承担了对代码安全性质的繁复的证明工作，而代码消费方只需承担少量 且能够自动完成的验证条件生成即证明检查工作。 携带证明的代码将h o a r e 逻辑应用到汇编语言的安全性质验证中。和源级 的h o a r e 逻辑验证相比，在汇编语言甚至在机器语言级别上验证安全性质的优点 在于将编译器排除出t c b 。因此，携带证明的代码不仅给出了在汇编语言上的 推理系统，而且提出了一个传递安全移动代码的协议( n e c u l a ，1 9 9 8 ) 。 携带证明的代码存在的主要问题有两个方面：一是对于比较复杂和实际的 安全策略，安全证明难以自动产生，因此整个的验证过程很难自动化完成；第 二是验证条件生成器的规模仍然比较庞大( 例如，在为j a v a 语言实现的携带证 明代码框架中，验证条件生成器由数万行的c 代码构成) ，因此大大增大了系 统的t c b 。针对第一个问题，为了追求验证过程的自动性，许多研究者放弃了 对可靠性的要求，而把整个框架用作代码的静态检查框架。这其中典型的工作 包括c o m p a q 系统研究中心进行的扩展静态检查( e x t e n d e ds t a t i cc h e c k i n g ， 简称e s c ) 研究( d e t l e 盆e ta 1 ，1 9 9 8 ；f l a n a g a ne ta 1 ，2 0 0 2 ) 和微软研究院进行 的s p e c 券( b a r n e t te ta 1 ，2 0 0 4 ，2 0 0 5 ；l e a v e n se ta 1 ，2 0 0 7 ) 项目等。针对第二个问 题，许多研究者放弃了自动完成证明的要求，而尝试手工使用辅助定理证明工 具来完成相应相应程序的证明，这其中典型的研究包括基础携带证明的代码 ( f o u n d a t i o n a lp r o o f - c a r r i n gc o d e ，简称f p c c ) 和验证汇编编程等。 扩展静态检查研究将h o a r e 逻辑方法用于m o d u l a 卜3 以及j a v a 程序的错误检 查。扩展静态检查研究工作开发了一种用于捕捉源程序中错误的静态检查器。 它能够检查包括数组下标越界、空指针引用、以及多线程程序中同步错误等在 9 绪论 内的许多常见的程序错误。下面以在j a v a 语言上的扩展静态检查器e s c j a v a 为 例，简要地描述检杳器的工作过程。e s c j a v a 检奄器的输入是经断言标注 的j a v a 源语言。检查器的前端将提取标注程序中的断言信息用于检查。在编译 器的内部，这些断言信息都被转化为源程序抽象语法树上的相关断言节点。背 景谓词是描述要检查的j a v a 类的类型相关的一阶谓词。接下来，翻译器把加有 注释的例程翻译成一些警戒命令( g u a r d e dc o m m a n d ) ( d i j k s t r a ，1 9 7 5 ) 。警戒命 令描述了在源程序的某些程序点执行状态需要满足的断言。检查器将根据警戒 命令计算验证条件( v e r i f i c a t i o nc o n d i t i o n s ，简称v c ) 。这些验证条件将被输 入一个自动定理证明器s i m p l i f y ( d e t l e f se ta 1 ，2 0 0 5 ) ，证明器尝试从背景淆词和 描述j a v a 程序固有性质的谓词证明验证条件，如果证明的过程成功，则可以保 证程序不会出现特定的程序错误；若证明的过程失败，则可以较为精确地给出 可能出错的程序点及错误信息。扩展的静态检查的成功之处在于它摈弃程序验 证中一些比较困难的目标，例如部分正确性等；但是由于扩展的静态检查自动 合成近似的循环不变式，放弃了可靠性要求，因此，它并不能保证程序完全不 会出现某种错误，而只能达到某种程度的语义精确性。 通过前面的分析已经知道，在传统的p c c 系统中，验证条件生成器构成了 系统最大的t c b 。为了减小p c c 的t c b ，a p p e l 提出基础携带证明代码的的概 念( a p p e l ，2 0 0 1 ) ，基础携带证明的代码使用最基础的逻辑，不添加和类型系统 相关的任何公理和原语。基础携带证明的代码没有了验证条件生成器，且不依 赖任何特定的类型系统，所以它有比传统携带证明的代码更小的t c b 。在基础 携带证明的代码里，机器代码的操作语义和安全策略都统一使用一种合适的有 足够表现力的逻辑来描述。基础携带证明的代码中的证明更难构造出来，因为 它需要建立复杂的语义模型来进行类型的推理。例如，f p c c 的逻辑类型即源 代码类型的语义解释，它是抽象存储和值上的命题。基础携带证明的代码的语 义模型存在很多问题，最大的一个问题是语义模型的复杂性使得证明的构造很 复杂，一个浅显的命题都要通过基本的公理集合和逻辑推理规则来进行证明， 所以基础携带证明的代码构造是困难的。 基于基础携带证明代码中存在的这些问题，s h a o 和n a d e e mh a m i d 等人 在携带证明的汇编编程项目( c e r t i f i e da s s e m b l yp r o g r a m m i n g ，简称c a p ) 中( f e n ga n ds h a o ，2 0 0 5 ；f e n ge ta 1 ，2 0 0 6 ；h a m i de ta 1 ，2 0 0 3 ；n ia n ds h a o ，2 0 0 6 ； y ua n ds h a o ，2 0 0 4 ；y ue ta 1 ，2 0 0 3 ) ，提出了一种基于语法的基础携带证明的代 码，在这个框架中，机器级的逻辑证明与源级类型系统的语法编码合并使用来 推导安全性，形成h o a r e 逻辑和类型系统的接口连接。早期的基础携带证明的代 码通过为类型构造一个复杂的语义模型来建立证明，以推导机器级的安全性。 而在验证汇编编程中，关于一个类型化程序的基础逻辑上的证明仅由类型推断 1 0 绪论 和语言类型系统的可靠性证明组成。每一种符合安全策略的机器状态都与一个 类型正确的程序相联系，而机器状态的转换则与程序的计值联系。这样类型系 统的前进性和保持性证明可以用来构造相应的程序安全性证明。类型系统的前 进行和保持性证明要比语义的可靠性证明容易得到。而类型推断也可以从以语 法制导的类型检查规则为基础的类型检查器得到。由此，这种语法的方法可以 较简单地得到关于程序安全性的基础逻辑证明。研究者通过两种方法来构造携 带证明的二进制代码：一是程序员利用c o q 证明辅助工具手工地为机器代码产 生安全性证明；二是通过上述语法方法对t a l 代码的构造产生安全性证明。此 外统一的基础逻辑框架使经过分离编译和检查产生的类型化汇编语言代码能接 受外部函数。这些函数是由验证汇编编程的语言写成的携带证明的二进制代 码。 1 2 3类型系统和逻辑系统相结合的方法 应用类型系统( a p p l i e dt y p es y s t e m ，简称a t s ) ( c h e na n dx i ，2 0 0 5 ；x i ， 2 0 0 4 ；x ie ta 1 ，2 0 0 3 ，2 0 0 5 ) 是h o n g w e ix i 等人在依赖类型和h o a r e 逻辑基础上做 的进一步工作。这种方法尝试将类型理论和h o a r e 逻辑结合起来。通过这种方 法可以在实用的编程语言上支持h o a r e 逻辑，但同时又能够保持实际定理证明 的可行性。和传统的类型系统相比，应用类型系统能够静态地捕捉更多的运行 时信息和状态变化，因而可以在编译期间确保更多的安全性质；但是和传统 的h o a u r e 逻辑相比，应用系统所面对的安全策略比较简单，可以被有效的整合到 类型系统当中，从而进行有效的检查，并且保证了可靠性。 最初的依赖类型只包括整数依赖变量( 单元素整型) ，应用类型系统对依 赖类型系统进行了扩展，其中的依赖类型可以依赖于：整数类型、布尔类型以 及引用类型，这些类型的变量都被赋以单元素类型。这三类不同的单元素类 型被提升到种类层次( k i n d ) ，形成b 0 0 1 e 强、i n t 、a d d r 三个类别。在同一种 类上的单元素类型之间具有相应类型层上的运算，例如整数种类上的单元素 类型之间可以进行四则运算；布尔种类上可以进行非、析取、合取等逻辑运 算。这些单元素类型能够用来构成断言类型( a s s e r t i n gt y p e ) 。这些类型用于 描述细致的计算状态。应用类型系统中引入了警卫类型和计算类型，它们都是 断言类型，分别对应h o a r e 逻辑推理中的前条件和后条件。例如参数为整型变 量m 和n 的求积函数的类型为： 眦1 t ：vm ，n ：i n t m 0 n 0 ) ( m 木n i n t ) 这个类型中符号“) ”之前为警卫类型，在类型检查时需要检查当前程序状态 中相关断言类型是否得到满足，即断言仇0 礼0 是否成立。函数箭头符 1 1 绪论 号“_ ”之后为计算类型，描述了满足警卫类型函数体必须达到的程序状态。 计算类型不仅可以像这个例子那样表现为函数返回值的类型，还可以表现为 谓词形式的断言类型。依靠与h o a r e 逻辑的相似性，应用类型系统能够编码部 分h o a r e 逻辑，从而可以在这一类型系统上模拟h o a r e 逻辑的部分推理。 1 3 存在的问题和发展方向 上面的小节对近几年来基于程序语言理论和实现技术的软件安全性研究中 有代表性和比较重要的研究工作进行了介绍。这一领域中的研究基本上可以分 为两类：基于h o a r e 逻辑推理的研究和基于类型系统的研究，并且在这两个方向 上都已经取得了有价值的研究成果。基于类型系统的研究是一种比较简单的语 法方法，其主要优点是相对简单，可扩展性好且容易应用到现有的程序设计语 言中去，因此，现在的主流程序设计语言都使用了类型系统的技术，且都试图 保证语言是类型安全的；但是类型系统因此要保证类型检查理论上的可判断性 和实际上实现的可行性，因此只能保证比较简单的安全策略，无法处理复杂的 安全策略。而基于h o a r e 逻辑和程序验证的研究应用范同更加广泛，原则上可以 处理任何可以被形式化的安全策略，但是这种方法对程序设计者提出了更高的 要求，并且在证明部分或者完全正确性时，要么证明过程繁杂，超出了实际程 序设计代价的承受能力，要么证明不能自动完成。 基于现有的研究现状，基于h o a r e 逻辑方法和类型方法相结合的方法是基于 程序设计语言理论和实现技术的安全软件的可行研究方向。现有的研究离现实 的编程应用还存在着较大的差距。在综合已有的基于语言理沦和实现技术的软 件安全研究的基础上，我们认为，今后高安全软件设计的一种新的模式将是基 于程序性质证明的开发。具体讲，这个开发模式具有以下特点：1 ) 程序设计者 将软件的安全策略等描述成程序应满足的规范，连同程序一起提交给编译器。 在这个步骤中，程序设计者所描述的安全策略应该比类型安全更强，但弱于完 全或者部分正确性，以便这些安全策略能够被后续的阶段处理；即试图保证的 程序形式是安全性质，而不是任意的正确性性质，从这个角度来说，这个工作 介于简单的类型检查和复杂的程序验证中间；2 ) 编译器生成为证明程序满足规 范所需的验证条件，并且利用内嵌的定理证明器自动地或交互地证明这些验证 条件并生成显式的证明；为了证明这些验证条件，要设计并实现独立的定理证 明器，之所以要重新设计而不是利用已有的证明器，是因为已有的证明工具一 般是为证明普遍的数学或者逻辑命题而设计，当处理具体语言相关的命题是， 存在较大局限；3 ) 编译器在把源程序翻译成目标