（计算机软件与理论专业论文）可信软件开发框架下的出具证明编译研究.pdf

中文摘要 摘要 随着国家和社会对软件的依赖程度日益增长，软件的安全性越来越受 到关注，软件的安全性主要包括s a f e t y 和s e c u r i t y 两个方面。s a f e t y 是指软 件运行时不引起危险、灾难的能力，而s e c u r i t y 是指软件系统对数据和信息 提供保密性、完整性、可用性、真实性保障的能力。本文的研究主要关注 软件的s a f e t y ，但是软件的s a f e t y 和s e c u r i t y 是有联系的，黑客通常就是利 用缓冲区溢出、数组访问越界、悬空指针访问等低级的s a f e t y 错误，来破坏 系统和获得未经授权的控制等。因此提高s a f e t y 有助于保证s e c u r i t y 。 提高s a f e t y 的目标是：所有的程序错误在程序运行前被发现或者在程序 运行时被温和地捕获，以保证程序不会导致不可预测的系统行为。软件安 全性研究主要是探索建立一个管理安全性的健全的科学和技术基础，其中 软件满足安全策略的证明方法( 即程序性质证明) 是研究的热点之一。程 序性质证明既可以采用基于类型的方法也可以采用基于逻辑的方法，近年 来还有人提出了逻辑和类型相结合的方法。然而在程序性质证明方面，现 有的研究不是集中于高级语言层次就是集中于低级语言层次，而很少同时 考虑高级语言和低级语言的。基于高级语言的研究易于程序员使用，且可 以更早发现程序的安全问题，但是被信任计算基础( t c b ) 比较大，而基 于低级语言的研究虽然t c b 比较小但是形式大多比较复杂，难以被程序员 使用从而也难以应用到实际当中。一些出具证明的编译器虽然能根据源程 序信息产生其汇编代码的证明，但可证明的程序性质大都是一些源级类型 系统可以表达的性质，一些复杂的性质例如值相关的性质并没有在考虑的 范围内。 基于上述考虑，本文设计了一种可信软件开发框架，该框架的特点 是同时包含了源级和目标级的程序性质证明，并且使用出具证明编译器 根据源级规范和证明自动生成目标级证明。该框架可以表达的程序性质 不仅局限于类型，还可以是更复杂的程序性质。比如值相关的部分正确 性。本文在该框架下主要探讨了出具证明编译的相关技术，即编译器在 翻译源代码到汇编代码的同时，根据源级安全规范和证明附带生成汇编 中文摘要 代码满足等效规范的证明，并同汇编代码一同输出。这些证明可以被底 层证明检查器所检查以证明生成的汇编代码满足安全规范。本文的 工作主要基于类型化汇编语言( t y p e da s s e m b l yl a n g u a g e ) 、验证汇编 编程( 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 ) 和携带证明代码( p r o o f - c a r r y i n g c o d e ) 等研究，采用的是类型和逻辑相结合的研究方法。 本文首先介绍了国内外基于程序性质证明的软件安全的相关研究和出 具证明编译的研究，然后提出了一个可信软件开发框架，随后本文着重介 绍了在这个框架下的出具证明编译技术，以及一个相应的出具证明编译器 的设计和实现。这些技术包括验证条件生成技术，底层代码规范( 断言) 的翻译和生成技术，以及底层证明的生成技术。本文还讨论了出具证明的 编译特性对传统编译技术的影响。 本文的主要特色和贡献为： 提出了一个可信软件开发框架。它向程序员提供源级程序性质证明接 口，允许程序员提供源级规范和源程序满足规范的证明，并通过出具 证明编译器产生目标程序满足等效规范的证明。对目标级证明的检查 可以将代码编译器排除出系统t c b ，从而提高程序可信性；而目标 级证明的自动生成则减轻了程序员的负担。 改进设计了源级验证条件生成算法。该算法将证明源程序满足安全规 范的问题转化为证明验证条件正确性的问题。该算法还合并了源语言 定型规则中的附加条件收集，同时也考虑了生成的验证条件的化简问 题。源级验证条件的证明可以使程序的安全问题尽早暴露。 设计并实现了一个出具证明编译器的原型系统，该编译器首次尝试根 据源级规范和证明生成目标级规范和证明，且产生的证明包含了验证 条件生成过程的证明，从而将验证条件产生器排除出系统t c b ，避 免了现有出具证明编译器的t c b 中存在复杂的验证条件产生器的尴 尬局面。而且，相比已有的出具证明编译器，该编译器可以处理更加 复杂的程序性质，例如值相关的部分正确性。 本文由中国国家自然科学基金资助( 编号6 0 6 7 3 1 2 6 ) 关键宇： 软件安全，程序性质证明，h o a r e 逻辑。被信任计算基础，类型 安全，验证框架，出具证明编译器 英文摘要 a b s t r a c t n o w a d a y s ，h i g h - a s m t r a n c es o f t w a r ei 8m o r ea n dm o r ev a l u e d ，a n da m o n g i t sp r o p e r t i e s s a f e t ya n ds e c m 4 t ya r em o s ti m p o r t a n t s a f e t yi 8t h ea b i 】i t yt o g u a r a n t e et h a ts o f t w a r ee x e c u t i o nd o e sn oh a r mt ot h es y s t e m a n ds e c u r i t y i st h ea b i l i t yt op r e s e r v et h ec o a t i d e n t i a l i t y , i n t e g r i t y , a v a i l a b i l i t ya n da n t h e n - t i c a t i o no fd a t a t h e r ei 8ac l o s er e l a t i o n s h i pb e t w e e ns a f e t ya n ds e c u r i t y f o r e x a m p l e ，h a c k e r su s u a l l y 瑚el o w - g r a d es a f e t ye r r o r s ，s u c ha sb u f f e ro v e r f l o w s ， o u t - o f - b o u n da r r a ya c c e 8 嘲a n dd a n g l i n gp o i n t e rd e r e f e r e n c e s t od e s t r o ya s y s t e mo ra c h i e v eu n a u t h o r i z e dc o n t r o lo fas y s t e m 。a p p a r e n t l y , i ti sh e l p f u l t oe n s i k es o f t w a r es e c u r i t yb ys t r e n g t h e n i n gi t ss a f e t y t oa c h i e v es o f t w a i - es a f e t y , a l lp r o g r a me r r o r ss h o u l db ed i s c o v e r e db e - f o r et h ee x e c u t i b no ft h ep r o g r a mo rb eg e n t l yc a p t u r e dd u r i n gt h ee x e c u t i o n t h er e s e a r c hg o a lo fs o f t w a r es a f e t yi st ob u i l daw h o l e s o m es c i e n t i f i ca n d t e c h n o l o g i c a li n f r a s t r u c t u r ef o rt h em a n a g e m e n to fs o f t w a r es a f e t y a n dt h e v e r i f i c a t i o nm e t h o df o rs o f t w a r et om e e ti t ss a f e t yp o l l c i e sf i e ，p r o g r a mv e t - i f i c a t i o n ) i so n eo ft h eh o tt o p i c si nt h i sr e s e a r c hf i e l d i nt h ep a s td e c a d e ， g r e a tp r o g r e s sh a sb e e nm a d ei nt h ea r e ao fp r o g r a mv e r i f i c a t i o n m a n y p r o j e c t sa d o p tt y p e - b a s e do rl o g i c - b a s e da p p r o a c h e st or e a s o na b o u tp r o g r a m p r o p e r t i e s a n di nr e c e n ty e a r s ，s o m ep r o j e c t sh a v et r i e dt oc o m b i n et h e m h o w e v e r ，p r e v i o u sp r o g r a mv e r i f i c a t i o np r o j e c t sh a v ef o c u s e do ne i t h e rh i g h - l e v e lp r o g r a m m i n gl a n g u a g e so rl o w - l e v e la s s e m b l yl a n g u a g e s ，b u tn o to nb o t h s i m u l t a n e o u s l y r e s e a r c h0 1 3 h i g h - l e v e ll a n g u a g e sh a sm a n ya d v a n t a g e ss u c h a sn s e r f r i e n d l i n e s s ，e a r l ys a f e t yb u gd e t e c t i o ne r e ，b u tt h et c b ( t r u s t e d c o m p u t i n gb a s e ) i sr e l a t i v e l yl a r g e ；o nt h eo t h e rh a n d ，t h et c b o fl o w - l e v e l p r o g r a mv e r i f i c a t i o ni sm u c hs m a l l e rb u tt h el o w - l e v e ls a f e t yp r o o f sa r em o r e c o m p l e xa n dh a r d e rt oc o n s t r u c tt h a nt h eh i g h - l e v e lo n e s e v e nt h o u g hs o m e c e r t i f y i n gc o m p i l e r 8a r ea b l et op r o d u c es a f e t yp r o o f sf o ra s s e m b l yp r o g r a m s b a s e do nt h ek n o w l e d g eo ft h ec o m p i l e ds o u r c ep r o g r a m s ，o n l ys o m es i m p l e 英文摘要 p r o g r a mp r o p e r t i e 8 勺r p i c a l l yt h o s eo ft y p es y s t e m - - c o u l db ep r o v e da u t o - m a t i c a l l y m u c hm o r ec o m p l e xp r o p e r t i e s ，s u c ha sp a r t i a lc o l t e c t n e s sa b o u t v a l u e s ，a r eh a r dt op r o v ea u t o m a t i c a l l yi nt h e s e m p i l e r s u n d e rt h ea b o v ec o n s i d e r a t i o n s ，i nt h i sd i s s e r t a t i o n ，ip r e s e n tt h ed e s i g n a n di m p l e m e n t a t i o no fah i g h - a s s u r a n c es o f t w a r ed e v e l o p m e n ti n f r a s t r u c t u r e i nt h i si n f r a s t r u c t u r e ，s o u r c e - l e v e la n da e s e m b l y - l e v e lp r o g r a mv e r i f i c a t i o n c o u l db ed o n es i m u l t a n e o u s l y , a n da c e r t i f y i n gc o m p i l e rp r o d u c e sa s s e m b l y - l e v e ls a f e t yp r o o f sa u t o m a t i c a l l yf r o mt h es o u r c e - l e v e l s p e c i f i c a t i o n sa n ds a f e t y p r o o f s t h em a i na d v a n t a g eo ft h i si n f r a s t r u c t u r ei st h a tt h ep r o v e ds a f e t y p r o p e r t i e si n c l u d en o to n l yt y p ep r o p e r t i e s ，b u ta l s oa d v a n c e dp r o p e r t i e s ，s u c h a sp a r t i a lc o l t e c t n e 8 8a b o u tv a l u e s t h i sd i e s e r t a t i o np r e s e n t st h ei m p o r t a n t t e c h n i q u eia d o p t e di nc e r t i f y i n gc o m p i l a t i o n t h a ti s ，a l o n gw i t hc o d eg e n - e r a t i o n ，t h ec o m p i l e rp r o d u c e st h es a f e t yp r o o f so ft h ea s s e m b l yp r o g r a m s s a r i s f y i n ga s s e m b l ys p e c i f i c a t i o n sf r o ms o u r e e - l o v e lp r o g r a m s ，s p e c i f i c a t i o n s a n ds a f e t yp r o o f s b o t ht h es p e c i f i c a t i o n sa n dt h es a f e t yp r o o f sa r ec a r r i e d b yt h ec o d e ，a n dc o u l db ec h e c k e db ya na e s e m b i - l e v e lp r o o fc h e c k e rt oe n - s u r et h a tt h ec o d es a t i s f i e si t ss p e c i f i c a t i o n s t h 6w o r ki nt h i sd i s s e r t a t i o n i si n s p i r e db yt a l ( t y p e da s s e m b l yl a n g u a g e ) ，c a p ( c e r t i f i e da s s e m b l y p r o g r a m m i n g ) a n dp c c ( p r o o f - c a r r y i n gc o d e ) e t c ，a n da d o p t sa na p p r o a c h o fc o m b i n i n gb o t ht y p e sa n dl o g i c s i nt h i sd i s s e r t a t i o n ，i ，f i r s t l y , i n t r o d u c es o m e p r e v i o u sw o r ko np r o g r a m v e r i f i c a t i o na n dc e r t i f y i n gc o m p i l a t i o n ；t h e nip r e s e n tah i g h - a s s u r a n c es o f t - w a r ed e v e l o p m e n t i n f r a s t r u c t u r e ；n e x tim a i n l yp r e s e n tt h ec e r t i 研n gc o m p i - l a t i o nt e c h n i q u e sb a s e do i lt h i si n f r a s t r u c t u r ea n dt h e d e s i g na n di m p l e m e n t s - t i o no fa c e r t i f y i n gc o m p i l e rp r o t o t y p e t h e s et e c h n i q u e si n c l u d e ：v e r i f i c a t i o n c o n d i t i o ng e n e r a t i o n ( v cg e n ) ，a s s e m b l y - l e v e lc o d es p e c i f i c a t i o nt r a n s l a t i o n a n d g e n e r a t i o n ，a s s e m b l y - l e v e ls a f e t yp r o o fg e n e r a t i o n ，e t c ia l s od i s c u s st h e i n f l u e n c eo fc e r t i f y i n gc o m p i l a t i o nt e c h n i q u e so nt r a d i t i o n a lc o m p i l a t i o n t h em a i nc o n t r i b u t i o n sa n dc h a r a c t e r i s t i c so ft h i sd i s s e r t a t i o na r e ： i tp r e s e n t sa ni n f r a s t r u c t u r ef o rh i g h - a s s u r a n c es o f t w a r ed e v e l o p m e n t t h i si n f r a s t r u c t u r eg i v e sa ni n t e r f a c ef o rp r o g r a m m e r st op r o v i d es o u r c e s p e c i f i c a t i o n sa n dt h ep r o o f so fp r o g r a m ss a t i s f y i n gt h e s es p e c i f i c a t i o n s l v 英文摘要 a l o n gw i t hs o u r c ep r o g r a m s ac e r t i f y i n gc o m p i l e ri nt h i si n f r a s t r u c t u r e c o u l dp r o d u c et h ea s s e m b l ys p e c i f i c a t i o n sa n ds a f e t yp r o o f sf r o mt h e s o u r c e - l e v e lo n e 8 a s s e m b l y - l e v e lp r o o fc h e c k i n gr e m o v e st h ec o m p i l e r f r o mt h et c b ，a n ds oe n h a n c e st h er e l i a b i l i t yo ft h es y s t e m t h ea u t o - m a t i ca e s e m b l y - l e v e lp r o o fg e n e r a t i o na l l e v i a t e st h ed i m c u l 够o fw 矗t m g p r o o f s i ti m p r o v e st h ed e s i g no fs o u r c e - l e v e lv cg e n e r a t i o na l g o r i t h m t h e n e w - a l g o r i t h mt u r n st h ep r o b l e mo fp r o v i n gp r o g r a m ss a t i s f y i n gs p e c i - f i c a t i o n si n t oa ne q u i v a l e n tp r o b l e mo fj u d g i n gt h ev a l i d i t yo ft h ev e r i f i - c a t i o nc o n d i t i o n s ( v c s ) t h i sa l g o r i t h ma l s oc o m b i n e st h ec o l l e c t i o no f s i d ec o n d i t i o n si ns o u r c et y p i n gr u l e sa n dc o n s i d e r st h es i m p l i f i c a t i o no f v c s t h ep r o v i n go f8 0 n r c ev c sm a k e st h ee a r l yb u gd e t e c t i o np o s s i b l e a n de a s y 。 i ts h o w st h ed e s i g na n di m p l e m e n t a t i o no fac e r t i f y i n gc o m p i l e rp r o t m 锣p e ，a n dt h i sc e r t i f y i n gc o m p i l e rp r o d u c e sa s s e m b l y - l e v e ls p e c i f i c a t i o n s a n ds a f e t yp r o o f sa u t o m a t i c a l l yf r o mt h es o u r c e - l e v e lc o u n t e r p a r t s t h e g e n e r a t e dp r o o f sc o n t a i nt h es o u n d n e s sp r o o f so fv cg e n e r a t i o n s ot h a t t h ev cg e n e r a t o ri sr e m o v e df r o mt h et c b a n dt h i sa v o i d st h ee x i s - t e n c eo fab i gt c b - v cg e n e r a t o r c o m p a r e dw i t hp r e v i o u sc e r t i f y i n g c o m p i l e r s ，t h i sc o m p i l e rc o u l dd e a lw i t hm u c hm o r ec o m p l e xp r o g r a m p r o p e r t i e s ，s u c ha gp a r t i a lc o r r e c t n e s sa b o u tv a l u e s t h i sd i s s e r t a t i o nw a ss u p p o r t e db yc h i n e s en a t u r a ls c i e n c ef o u n d a t i o n u n d e rg r a n tn o 6 0 6 7 3 1 2 6 k e yw o r d s ： s o f t w a r es a f e t y ，p r o g r a mv e r 进c 8 t i o n ，h o a r el o g i c ，t r u s t e d c o m p u t i n gb a s e ，t y p es a f e t y , v e r i f i c a t i o nf r a m e w o r k ，c e r t i f y i n gc o m p i l e r v 插图目录 插图目录 1 一le s c 检查器结构图， 1 2 p c c 整体框架图。 1 - 3t o u c h s t o n es a f e c 的整体框架 1 4 验证器的结构 1 - 5t o u c h s t o n es a f e c 低级语言上安全谓词的语法， 2 - 1 传统程序设计框架 2 - 2 加入了源级验证系统的程序开发框架 2 - 3 加入了目标级验证系统的程序开发框架 2 4 可信程序开发框架 2 - 5p o i n t e r c 语法 2 - 6p o i n t e r c 运算符的优先级( 从高到低) 和结合性 2 - 7p a l 的抽象语法 2 - 8 耳标机器( t m ) 模型，。 2 - 9f c a p 证明系统规范的抽象语法 2 - 1 0 传统编译器框架：。 2 - 1 1 出具证明编译器p l c c 框架 3 1 出具证明编译器p l c c 的前端框架 3 - 2 数据结构：a s t 3 - 3 数据结构：t a b l e 孓4 验证条件生成算法及其使用的最弱前条件演算规则 v 0 0 埔 玷 丝弱；! 号 盯勰 驼；5；盯钓眈 盯 乩 孔 插图目录 垂1 出具证明编译器p l c c 的后端框架 4 - 2 数据结构：c o d e g e n - t a b l e 垂3 代码生成流程 垂4 栈帧的组织 4 - 5 一个例子：m u l t ( m ，n )( 源代码) 垂6 一个例子：- m u l t ( m ，n ) ( 汇编代码) 垂7 翻译后的汇编级规范 4 - 8 调整后的汇编级规范 4 - 9 前条件计算的部分规则 5 - 1 函数满足规范的证明示意图 v i 丝8记住竹鸺眈 酃 中国科学技术大学学位论文相关声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工 作所取得的成果。除已特另j j 2 n 以标注和致谢的地方外，论文中不 包含任何他人已经发表或撰写过的研究成果。与我一同工作的同 志对本研究所做的贡献均已在论文中作了明确的说明。 本人授权中国科学技术大学拥有学位论文的部分使用权， 即：学校有权按有关规定向国家有关部门或机构送交论文的复印 一 件和电子版，允许论文被查阅和借阅，可以将学位论文编入有关 数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、 汇编学位论文。 保密的学位论文在解密后也遵守此规定。 5 作者签名： 葛杵 2 0 0 7 年5 月3 1 日 绪论 1 1背景研究 第一章绪论 随着国家和社会对软件依赖程度的日益加深，计算机软俘在人们的日 常和社会生活中正在扮演着越来越重要的角色，小到常见的手机、电脑的 操作系统，大到火箭、航天飞机的控制系统，无不渗透着软件的作用。而 社会对软件的依赖直接导致了关键软件的高可信要求越来越重要 在软件高可信的各种要素中，安全性是关注的重点，软件的安全性包 括s a f e t y 和s e c u r i t y 两个方面，s a f e t y 是指软件运行时不引起危险、灾难的 能力，而s e c u r i t y 是指软件系统对数据和信息提供保密性、完整性、可用 性、真实性保障的能力。本文的研究主要是针对软件s a f e t y 所做的一些尝 试，但是实际上，软件的s a f e t y 和s e c u r i t y 是有联系的，黑客通常就是利 用缓冲区溢出、数组访问越界、悬空指针( d a n g l i n gp o i n t e r ) 访问等低级 的s a f e t y 错误，来破坏系统和获得未经授权的控制等。显然提高s a f e t y 有助 于保证s e c u r i t y 。本文后面所提到的软件安全性都是指软件的s a f e t y 。 提高安全性的目标是：所有的程序错误在程序运行前被发现或者在程 序运行时被温和地捕获，以保证程序不会导致不可预测的系统行为。目前 工业界大多使用测试的方法来保证软件的安全性，但是测试有其固有的局 限性，由于测试不可能穷举所有可能的输入，因此尽管测试花费了很多人 力物力，却依然无法保证软件在实际运行中遇到其他数据不出现问题。人 们更希望有一种开发安全软件的方法，可以让软件在开发过程中就能保证 不出现某一类错误，程序性质证明( 或者称为程序验证) 就是这样一种方 法。关于程序性质证明的研究曾在上世纪7 0 年代得到很多成果【1 】1 ，8 0 年代 趋于沉寂，丽在9 7 年以后随着携带证明的代码 2 1 ( p r o o f - c a r r y i n gc o d e ， 简称p c c ) 的出现和兴起又重新受到重视。本文所探讨的就是在程序性质 证明基础上设计一种可信软件开发框架，并在该框架下阐述我对出具证明 编译的相关研究。本节将介绍一下该领域的基本概念。 1 1 背景研究 1 1 1程序性质证明 程序性质是对程序或程序元素( 例如程序变量等) 的某种行为的描 述。程序性质的描述方式多种多样，最常见的方式是类型的方式。例如， 在c 3 l 语言中，“程序变量v 的类型是i n t 型”描述了该变量在其作用域 和生存期内都是按照“整型”的行为方式来存在的。程序的性质也可以用 程序规范( s p e c i f i c a t i o n s ) 来描述，所谓程序规范是描述程序行为的断言， 例如“变量v 的值在o 到l o 之间”。这个例子里的程序规范是用自然语言 描述的，但是实际上程序规范般会用严格的形式语言加以描述。前面所 述类型的方式实际上是程序规范的一种特例，例如前面关于整型的例子实 际上就表达了“v 是整型”这一程序规范，使用c 中的形式语言描述就是 “i n tv ；”。程序规范有时会包含程序不变式( i n v a r i a n t s ) 【4 1 这种概念， 不变式在程序运行的始末保持不变。 程序的安全性也属于程序性质范畴，不过这是一个比较宽泛的概念。 例如它可以包括数组访问不越界，没有空指针引用，内存不泄漏等等。 程序性质证明实际上就是证明程序( 或程序元素) 的行为满足程序性 质f 5 1 作为名词使甩肘，程序性质证明指的是这种证明的过程。本文后面 所说的程序安全性证明指的就是证明程序行为满足“安全性”这种程序性 质。程序性质证明是提高软件安全性的一类重要研究方法。 1 1 2软件的可信- i 生 由于本文使用程序性质证明这种方式来保证软件的安全性，因此本文 引入软件可信性这一概念本文中所说的软件是可信的就是指在使用程序 性质证明方法时，程序( 软件) 满足其对应的规范，即程序遵守它所声称 的行为要求，因此是可信的。 本文之所以使用软件“可信性”而不使用软件“安全性”这种提法， 是因为程序规范所描述的不一定是程序的安全性质，还可能是其他的性 质，但是只要程序满足规范中描述的性质，本文都称该程序是可信的。 1 1 3 被信任计算基础 被信任计算基础 6 】( t r u s t e dc o m p u t i n gb a s e ，简称t c b ) ，是指实 现系统的代码中不能证明为安全或者尚未被证明为安全，而不得不给予 2 绪论 信任的那些部分例如，所有的计算机硬件是包含在t c b 之内的，因为 如果你不信任计算机硬件的正确性，什么也做不了，也无法证明任何软 件的安全性。在常见的计算机系统中，除了硬件之外，操作系统内核也属 于t c b 。 t c b 这个概念通常被用来评价一个系统的易被攻击性，因为t c b 内可 能含有系统的安全漏洞。因此，研究软件安全的一个重要的方向就是研究 如何减小系统的t c b ，t c b 越小，相对来说系统安全的可能性就越高。 而且，小的t c b 可以使锝人们有能力将有限的精力投入到t c b 部件的检 查和测试中去，以尽可能保证这部分的安全性，从而提高系统的安全性。 越大的t c b 包含安全漏洞的可能性就越大，t c b 中的安全漏洞很可能使 你保障系统安全性的其他努力化为泡影 计算机系统中是不可能没有t c b 的，因为无论你使用什么样的保证系 统安全性的方法，你都必须在系统中找到一个部件去推行这个方法，这个 部件一定会包含在t c b 之内。因此，我们的研究只能立足于尽量减小系统 的t c b ，使之接近于一个极限最小值。 1 1 4出具证明的编译器 在现代程序设计中，人们一般使用c c + + m 等高级程序设计语言 来完成开发，以提高开发效率。高级语言编写的源程序需要经过编译器 等编译成低级语言进而成为目标程序来运行。如果在源语言级进行程 序性质证明，则编译器等势必包含在系统t c b 之内，从而使得t c b 庞 大。为了减小t c b ，很多学者试图在低级语言层次进行程序性质证明， 如t a lf 8 ，9 1 等，为了使得用高级语言编写的程序能在低级语言层次完成程 序性质证明编译器需要在编译源程序的同时生成低级语言层次的证明， 以便代码消费方可以在低级语言层次检查程序性质的证明。具有这样功能 的编译器通常叫做出具证明的编译器 出具证明编译器的概念最初是由n e c u l a 提出的，他设计的t o u c h s t o n e s a f e c 编译器f 1 0 1 除了包括传统编译器的功能外，还包含一个验证器 ( c e r t i f i e r ) ，能够为编译出来的汇编程序产生安全性证明，这些证明 可以被低层检查器所检查。他把这样的编译器叫做出具证明的编译器 ( c e r t i f y i n gc o m p i l e r ) 【1 0 1 。 3 1 2 程序性质证明和出具证明编译的相关研究现状及比较 1 2程序性质证明和出具证明编译的相关研究现 状及比较 本节介绍国际上与程序性质证明及出具证明编译相关的研究工作的新 动向与成果，并对它们进行比较。首先介绍的是关于程序性质证明的研 究，这些研究被分为基于h o a r e 逻辑 5 ，1 1 】的方法和基于类型的方法两种， 然后介绍结合这两种方法的程序性质证明的研究，最后讨论目前国际上对 验证编译的研究。 1 2 1基于h o a r e 逻辑推理的程序性质证明研究 基于逻辑的程序性质证明方法早在二十世纪六十年代就开始兴 起，f l o y d 1 l 和h o a r e 5 】的论文的发表被认为是基于逻辑的程序验证的基 石，h o a r e 在他的论文中提出了这样一个形式系统，后来被称为是h o a r e 逻 辑f 5 ，1 1 l - 要证明的定理由h o a r e 三元组 p s q 表示，其中p ，q 表 示命题，而s 表示程序语句。该三元组的含义是：如果当控制位于程序 语句s 的起始位置时命题p 为真，那么当控制位于s 的结尾时，q 将为 真。h o a r e 逻辑里还包含一组推理规则，例如赋值公理和w h i l e 规则： 规则1 1t p 陋z 1 ) 。：= e p 其中z 是变量标识符，e 是表达式，p 是 命题断言，p 【e 叫表示将p 中所有自由出现的z 替换成e 以后得到的断 言 规则1 2 如果有 p e s 【p ， 中e 是w h i l e 循环的条件表达式， 的循环不变式 那么有( p w h i l ee d o s p a ，e 其 s 是循环体语句，p 是断言，它是该循环 利用h o a r e 逻辑进行程序性质证明的特点是：逻辑系统给出基于程序状态的 断言语言( 规范) ，这些断言语言将用于描述关键程序点需要满足的条件 以及某些证明提示，例如循环不交式；然后根据推导规则由程序员手工或 是借助于某些证明工具半自动地给出断言成立的证明。 h o a r e 逻辑可以用来进行程序正确性的证明，这给了程序员一个希望， 这就是所有计算机程序的正确性都可以用形式证明严格保证。因此，在后 续的十几年里，大量工作基于此展开，以便验证更复杂的语言结构，寻求 4 绪论 更好的方式来表示、构造和检查程序性质。例如，谓词转移语义【1 2 】和最弱 前条件f 1 3 】的观点，以及用验证条件产生器和自动定理证明器【1 4 1 进行程序 的验证等。h o a r e 逻辑用于j a v a 【1 5 】语言程序上的验证如 1 6 】。 然而h o m e 逻辑规则并非都是语法制导的，例如规则1 2 ，这导致了许 多证明无法自动生成从八十年代起，关于h o m e 逻辑的研究进入了停滞阶 段。一方面是因为形式描述程序的正确性是一件很困难的事，另外一方面 是因为程序正确性证明中出现的定理往往浅显但证明过程冗长，而自动定 理证明问题迟迟无法解决。正如d e m i l l o ( 1 7 1 所说的那样：程序正确性证明 “绝不会成功”。 进入九十年代，g e o r g en e c u l a 提出了携带证明代码( p r o o f - c a r r y i n g c 0 d e ，简称p c c ) 【2 1 技术。自此，人们的研究焦点从程序正确性证明转 变为对程序安全性质的证明。这些安全性质通常是关于程序部分正确性的 规范，例如“数组下标在数组边界之内”、“锁使用后被释放”等等。证 明程序满足这样的规范要比证明程序正确性简单得多。h o e 逻辑推理又获 得了新生。 一、扩展静态检查 n e c u l a 的思想起源于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 ) 研究1 8 ，1 9 l 。该研究将h o m e 逻 辑方法应用于m o d u l a r - 3 以及j a v a 程序的错误检查。 e s c 的研究工作开发了一种编译时静态程宁检查器，用于检查一般 的编程错误。它能解决的问题包括空指针引用( n u l ld e r e f e r e n c e s ) 、数 组边界错误( a r r a yb o u n d se r r o r s ) 、类型投射错误( w p ec a s te r r o r s ) 等。也可以报告并发程序中的同步错误：竞争( r a c ec o n d i