（计算机软件与理论专业论文）基于携带证明的代码的垃圾收集过程验证.pdf

摘要 摘要 使用j a v a 和c 样等安全的程序设计语言编写的程序能够完全避免一些在传统 程序设计语言编写的程序中经常出现的安全漏洞，从而提高软件的可靠性。然 而，这类安全语言的众多安全特性都依赖于其运行环境，特别是垃圾收集机制的 正确性和安全性。不幸的是，垃圾收集算法通常难于设计和正确地实现。同时， 垃圾收集器和用户程序的交互过程也往往相当复杂而易出错。因此，为了提高 使用垃圾收集机制的程序设计语言的安全性和可靠性，势必需要对垃圾收集过 程的安全性和正确性进行严格的研究。 本文工作使用基于h o a r e 逻辑的汇编语言级形式程序验证框架，对垃圾收集 器的安全性和正确性，以及垃圾收集器与多种用户程序，特别是类型化汇编语言 的交互过程的安全性进行了严格的形式验证。本文工作基于携带证明的代码技 术，所有的验证都在计算机辅助定理证明工具c o q 中实现为计算机可检查的证 明。这样，垃圾收集器和用户程序就能够被构造为一个完整的携带安全性证明 的软件包，方便地通过互联网和其他渠道进行发布。 本文的第一部分工作验证了两种典型垃圾收集器的汇编语言实现。该工作 使用分离逻辑风格的代码规范语言给出了停止式标记一清扫垃圾收集器和基于 初始快照的y u a s a 渐进式垃圾收集器的安全规范，并使用h o a r e 风格的程序逻辑 和推理方法证明了垃圾收集器满足其安全规范。 第二部分工作从单独验证垃圾收集器工作存在的不足出发，提出并实现了 一种通用的验证垃圾收集器和用户程序交互过程的方法。其核心思想是使用类 似抽象数据类型的技术将垃圾收集器对用户程序的接口及其验证抽象起来，使 得用户程序的验证无需再关心垃圾收集器的具体实现，并方便用户程序验证和 垃圾收集器验证的链接。 最后一部分工作研究了类型安全的垃圾收集过程。给出了一种为基础的类 型化汇编语言提供验证的垃圾收集过程的方法，它基于一个开放式的汇编语言 级程序逻辑，并使用了第二部分工作的主要思想，将垃圾收集器的细节从类型化 汇编语言的类型系统中抽象出去，简化了类型化汇编语言的设计。 同时，本文还讨论了这些工作在计算机辅助定理证明工具c o q 中的实现，以 摘要 及在这些实现中设计和发展的一些提高证明效率的方法和技术。 本文工作的主要贡献和创新包括：1 ) 基于汇编语言层次的一个携带证明程 序的验证框架，首次成功地验证了多种垃圾收集算法的汇编级实现代码，以及 它们和用户程序的交互过程；2 ) 提出了一种基于抽象数据类型技术的通用方法， 能够对垃圾收集器、用户程序以及它们的交互过程进行简洁且严格的验证；3 ) 首次成功地解决了在最小被信任计算基础的前提下为类型化汇编语言提供类型 安全的垃圾收集过程这一热点研究问题；4 ) 基于分离逻辑技术，首次成功地从 单个内存单元开始构造了标记一清扫式垃圾收集器的具体内存规范。 这些研究工作对减小安全程序设计语言的被信任计算基础进行了有益的尝 试一一使用形式程序验证技术，携带基础证明的垃圾收集过程就可以被排除出 安全程序设计语言的被信任计算基础。同时，它们也为汇编语言级程序的形式验 证，特别是为携带证明的代码的技术的应用积累了重要的理论和实践经验。而 随着这类技术的进步，更多被信任的软件就可以经过验证而被排除出系统的被 信任计算基础。 关键词：形式程序验证，携带证明的代码，垃圾收集，类型化汇编语言 i i a b s t r a c t s a f ep r o g m 删n i n gl a n g u a g e ss u c ha sj a v aa n dc 蛳i sc a p a b l e0 fp r o d u c i n gs o r - w a r es y s t e m st 1 1 a ta r ef r e ef r o ms o m ep i 也l l so 缸ns e e ni ns 0 1 f t w a r ed e v e l o p e dw i m t r a d i t i o n a lp r o g r a n m l i n gl a n g u a g e s h o w e v e r ，a l l 山ee x i s t i n gs a f el a n g u a g e sr e l yo n g a r b a g ec o i l e c t i o nm e c h a 血s m f 0 rd y n a m i cm e m o 巧m a n a g e m e n t a n ds o m eo tt l l e i r s a f e t y r e l a t e df e a t u r e s ，i n c l u d i n gt l l ep r e v e n t i o no fd a n g l i n gp o i n t e rd e r e f e r e n c e 龃d m e m o 拶l e 如a r ep r o v i d e db yg 莉a g ec o l l e c t i o n n u s ，t h ec o 眦c t n e s so ft 1 1 e u n d e r l y i n gg a r b a g ec o l l e c t i o ni st l l ek e yt 0t 1 1 es a f e t yo ft l l e s el a n g u a g e s u 耐0 r t u n a t e l y ， g 砷a g ec o l l e c t o r sa r ee x ：1 1 e l yh 砌t 0i m p l e m e n tc 0 仃e c t l y ，锄dm e i ri n t e r a c t i o n s w i 也m u t a t o r sa r eo f t e nc o m p l e xa i l d r o r - p r o n e f o ri n c r e a s i n gt t i es a f e t yo fl a i l 。 g u a g e ss u c h 硒j a v aa n dc 群，i ti sn e c e s s a r yt 0d 9 0 m u s l yr e 笛o nd b o u tt t l es a f e t ya i l d c o r r c c m e s s0 fg a r b a g ec o l l e c t i o n n i sp 印盯p r c s e n t st i l e f - c 哪，i n gc o d cs t y l ef o n n 甜v c f i f i c a t i o no f1 w 0 g a r b a g ec o l l e c t o r sa g a i n s tt h e i rs a f b t ya n d c o r r e c t n e s ss p e c i f i c a t i o n s ，雏w e n 雏t h e s a f ei n t e r a c t i o nb e t w c e ng a r b a g ec o l l e c t o r sa n dv 撕o u s 舢t a t o r s ，i n c l u d i n gc o d e s c o n - s t m c t c dw i 山耐p e da s s e m b l yl a n g u a g e i h ev e r i f i c a t i o nw o r kp r e s e n t e di si m p l e 。 m e n t e da sc o qp r o o f s ，a n di st l l u sm a c h i n e c h e c k a b l ea n dr e a d y t 0b ed i s 耐b u t e di n t l l ef 0 咖o fp r o o f ca r 】呵i n gc o d e n ew o r kp r e s e n t e di nt h i sp a p e ri n c l u d e st h 嗽m a j o rp 躺。 t h ef i r s tp 甜o f w o f kv e r i 6 e st w og a r b a g ec o l l e c t o r s ，n 锄e l ys t o p - t h e w o r l dm a r k 。s w e e p 锄dy u a s a i n c r e m e n t a l ，a g 撕n s tm e i rs a f c t y 卸dc o r i 优t n e s ss p e c i f i c a t i o n s t 1 1 es p c c i 仃c a t i o n s ， i n c l u d i n gs o m ei m r i c a t ei n v 撕锄t sl i k et h ew e a l 【t n c o l o ri n v 撕a j l t ，a r ec o n s t r 佻t e d u s i n gs e p a r a t i o n - l o g i cs t y l es p e c i f i c a t i o nl a n g u a g e a n dt h ep r o o f i sc o n s t m c t e dl na h o a r e - s t y l ep r 0 伊a ml o g i c n es e c o n dp a r to fw o r ki n 仃d d u c e san e wu n i f o r n la p p r o a c ht 0v e r i f yt l l es a f e t y o ft t l ei r l t c r a c t i o nb e t w e e nm u t a t o r a i i dg a r b a g ec o i l e c t o ri nh o a r e s t y l ep r o g r a ml o 目c b a s e do nt e c h n i q u e sj i k ea b s 昀c td a ab p e ，m i sa p p r o a c hs p e c m e sg 曲a g ec o l l e c t o r i n t e r f a c e sj na na b s t r a c tw a y 7 i h u st h ev 嘶6 c a t i o n0 fm u t ：a t o ri sf r e e df 两mr e 硒o n - m a b s t r a c t i n ga b o u tt h ed e t a i l so fg a r b a g ec 0 1 l e c t o r a n dt h el i n l ( i n go ft h em u t a t o rv e r i f i c a t i o n a g a i n s tt h ev e r if i c a t i o no fg a r b a g ec o l l e c t o ri se a s i e ra n dm o r ef l e x i b l e t h ef i n a lp a r to fw o r ks t u d i e st h ej s s u eo ft y p e - s 疵g a r b a g ec o l l e c t i o n i to f f e r s a na p p r o a c ho fc o m b i n i n gt y p e da s s e m b l yl a n g u a g ew i t hv e r i f i e dg a r b a g ec o l l e c t i o n u s i n ga no p e np r o o f 二c a n 了i n gc o d e 仃a m e w o r l ( a n dt h ei d e a si nt h es e c o n dp a r t o fw o r k ，t l l i sa p p r o a c hs u c c e s s f u l l yl i n k st l l ec o d ec o n s 1 j c t e di nat y p e da s s e m b l y l a n g u 鸩ew i t l lap r o v e dc o n s e n ，a t i v eg a r b a g ec o l l e c t o r w h i c hi n c l u d e ss h o w i n gt h a t t h ec o l l e c t o r si n t e r f 砬es p e c i f i c a t i o n sa r ec o m p a t i b l ew i t ht h et y p i n gr u l e so ft h et y p e d a s s e m b l yl a n g u a g e b e s i d e s ，m i sp a p e ra l s 0d i s c u s s e sm ec o qi m p l e m e n t a t i o ni s s u e so fm ew o r k a b o v e ，a n di n 仃o d u c e ss o m ei d e a sa n dt e c h n i q u e sf o ri m p r o v i n gp r o d u c t i v i t yi np r o o f c o n s t m c t i o n t h ew o r kp r e s e n t e di nt h i sp a p e rm a ye f f 色c t i v e l yr e d u c e dm e 1 1 r u s t e dc o m p u t i n g b a s e0 fl a n g u a g e s1 i k ej a v aa n dc 静，a sw e l la so t h e rs a f ep r o g r a m m i n gs y s t e m su s - i n gg a r b a g ec 0 1 l e c t i o n a n dt h es u c c e s s f h lv e r j f i c a t i o no fc o m p l e xg a r b a g ec o l l e c t o r a l g o r i t h m si sa l s oav a l u a b l ee x p e r i e n c ef o rp r o o f - c a r 哕i n gc o d es t y l ev e r 狮c a t i o n k e yw b r d s ：f 6 n n a lp r o g r 狮v e r i f i c a t i o n ；p r o o f - - c a r r y i n gc o d e ：g a r b a g ec o l l e c t i o n ； t y p e da s s e m b l yi a n g u a g e 中国科学技术大学学位论文原创性和授权使用声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工作 所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含任 何他人已经发表或撰写过的研究成果。与我一同工作的同志对本研究 所做的贡献均己在论文中作了明确的说明。 本人授权中国科学技术大学拥有学位论文的部分使用权，即：学 校有权按有关规定向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进行检 索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 保密的学位论文在解密后也遵守此规定。 作者签名：土隧 瑚年6 月弓日 第1 章绪论 第1 章绪论 随着信息科学技术的进步，计算机已经被广泛地应用到国民经济和人民生 活的各个方面，这其中也包括了在航空航天、医疗、金融、能源、国防等核心的 应用领域中的关键应用。因此计算机系统的安全性和可靠性，特别是计算机软件 的安全性和可靠性，越来越为人所关注。传统的软件安全保障技术主要依赖于 软件测试。而由于软件测试与生俱来的不完备性，即便是通过了详尽测试的软 件也仍然可能存在着安全隐患。基于程序设计语言的软件安全研究试图通过使 用安全的程序设计语言来完全地消除软件中可能存在的特定安全隐患。使用这 类安全的程序设计语言，程序员通常能够避免在使用传统程序设计语言时经常 出现的一些安全漏洞，如数组越界、悬空指针访问、内存泄漏等等。对比于不完 备的软件测试技术，这类安全语言能够对特定的安全性要求给出完备的保证。 近几十年来，研究人员提出了多种安全的程序设计语言包括s m l ( m i l n e re t a 1 ，1 9 9 7 ) 、c a m i ( l e r o ye ta 1 ，2 0 0 7 ) 、j a v a ( g o s l i n ge ta 1 ，2 0 0 0 ) 、c # ( h e j l s b e 略e ta 1 ， 2 0 0 6 ) 、( m i c r o s o f tc o 甲o r a t i o n ，2 0 0 7 ) 等等。它们有的提供完整的类型系统以及 静态类型检查机制，避免了类似c ，c + + 语言中随意的类型转换造成的安全问题。 有的则通过运行时的动态检测和异常处理机制保证程序的行为即便在错误操作 的情况下也能得到有效的控制。 然而这类安全语言的实现大都相当复杂。一个典型的实现通常包括编译器、 标准库和一个复杂的执行环境( 虚拟机) 。由此可见，语言的安全性只是一个相 对概念，它是建立在诸如语言实现的正确性等基本假定之上的。而这些假定就 构成了这类安全语言的被信任计算基础( t h s 刷c o m p u t i n gb a s e ，简称t c b ) 。 从上个世纪9 0 年代开始，大量研究开始关注于如何减小安全语言的t c b ，从 而获得更高的安全性。携带证明的代码( p r o o f c a n 了i n gc o d e ，简称p c c ) 是其中 最有代表性的工作。基于p c c 的研究通过使用保类型( 证明) 的编译( m o 而s e t te t a 1 ，1 9 9 9 a ，l e a g u ee ta 1 ，2 0 0 l 。c h e ne ta 1 ，2 0 0 7 ) 、编译器验证( l e r o y ，2 0 0 6 ) 等技术， 把语言的安全性建立在汇编语言层次上，从而将编译器排除在t c b 之外。尽管如 此，一个安全的执行环境始终是必须的。而迄今为止所有安全语言的执行环境都 使用垃圾收集机制( j o n e s ，1 9 9 6 ) 来提供自动的动态存储管理。因此为基于p c c 的 第l 章绪论 安全语言系统构建安全的垃圾收集过程也就成了当前国际软件安全研究领域的 热点。 本文工作使用基于p c c 的汇编语言级形式程序验证技术( h o a r e ，1 9 6 9 ) ，在最 小化t c b 的前提下给出了对垃圾收集过程进行严格安全性验证的通用方法，并 验证了典型垃圾收集过程的安全性。在讨论具体研究工作之前，本章首先对垃 圾收集技术以及以p c c 为代表的形式程序验证技术做简要的非形式介绍，并回 顾相关的研究工作。 1 1 垃圾收集技术 垃圾收集技术( w i l s o n ，1 9 9 2 ，j o n e s ，1 9 9 6 ) 最早在2 0 世纪6 0 年代被使用 于l i s p 语言( m c c a n i l y ，1 9 7 8 ) 的实现中。相对于手动分配和释放动态内存 的m a l l o c f r e e 风格内存管理，垃圾收集是一种自动的内存管理模式。用户 程序并不需要显示的释放无用内存单元，而垃圾收集器会通过特定的方法发现 并回收这些无用内存。这种自动的内存管理模式不仅大大简轻了用户程序管理 内存的负担，也避免了悬空指针引用、重复释放内存等等传统系统中常见的问 题。因此，垃圾收集技术已经被广泛的应用于包括j a v a 和c 在内的众多程序设计 语言的实现当中。 1 1 1基本概念 通常，用户程序数据包括： 保存在寄存器中的数据、保存在活动记录中的局部变量以及保存在全局数 据区中的全局变量和静态变量等。用户程序可以通过寄存器号、局部或者 全局的名字直接访问它们。 保存在动态存储空间( 堆) 上的数据。用户程序需要通过指针引用进行间 接的访问，一旦引用或指针丢失，相应的数据将不再能被访问到。这些间 接数据通常以内存对象的单位分配，每个对象包含若干基本内存单元。 垃圾收集器在保证用户程序将会使用的数据( 即活跃数据) 不被破坏的情 况下将用户程序不可用的存储资源回收。由于用户程序行为的不可确定性，并 不存在一个算法能够精确地确定用户程序用户程序的活跃数据集合。因此，垃 2 第1 章绪论 根集根集根集 空闲链表 图1 1 标记一清扫式垃圾收集 圾收集器总是通过可达数据集合来保守地估计活跃数据集合。如果把用户程序 能直接访问的数据集合称为根集，那么可达数据就是那些从根集开始可以跟随 指针引用间接访问到的数据。 1 1 2 经典垃圾收集算法 依据垃圾收集器使用算法的不同，垃圾收集器可以被分为如下几类： 标记一清扫式( m 破s w e e p ) ，最早由m c c a n l l y ( 1 9 6 0 ) 提出。如图1 1 ，一个标记 一清扫垃圾收集周期包括两部分。首先，收集器从根集开始遍历内存对象 的引用关系图，同时标记所有可达的对象。然后扫描内存回收所有没有被 标记的对象。 节点复制式( c o p y i n g ) ，最早由m i n s k y ( 1 9 6 3 ) 提出，而以c h e n e y ( 1 9 7 0 ) 的算法最 为著名。如图1 2 ，节点复制式收集器最大的特点在于将整个堆分为两个半 区，用户程序只使用其中的一个半区，另一个半区作为保留半区。每当一 个半区充满后，垃圾收集器遍历并复制所有可达对象到保留半区，同时修 改相应的引用位。收集结束时系统将保留半区作为新的用户半区。 标记一清扫和节点复制被统称为跟踪式( t r a c i n g ) 垃圾收集，它们都需要对内存 对象的引用关系图进行跟踪遍历。相较而言，标记一清扫的特点在于不移动用户 3 第l 章绪论 根集 i 、用户半区! 保留半区 - - - ， 根集 i 、用户半区! 保留半区， 。一一， 根集 图1 2 节点复制式垃圾收集 数据，但容易产生内存碎片。而节点复制需要在两个半区间复制内存对象，但可 以很好的控制内存碎片。本文将主要讨论标记一清扫式垃圾收集，对于节点复 制式垃圾收集的类似讨论可以参考( b i r k e d a le ta 1 ，2 0 0 4 ，m c c r e i g h te ta 1 ，2 0 0 7 ) 。 其他的垃圾收集算法包括最早由c o l l i n s ( 1 9 6 0 ) 提出的引用计数算 法( r e f e r e n c ec o u n t i n g ) 。它记录到每个内存对象的引用的数目，在引用数 为0 的时候就回收相应的对象，但其最大的问题在于无法处理循环引用。另外还 有将标记一清扫和节点复制结合起来的标记一缩并( m a r k c o m p a c t ) 算法( h a n a n de v a n s ，1 9 6 4 ) 等。因为和本文后续内容无关，本节省略了对这些算法的介绍， 有兴趣的读者可以参考( j o n e s ，1 9 9 6 ) 。 1 1 3 用户程序和垃圾收集器的交互方式 垃圾收集过程是用户程序和垃圾收集器交互的过程。根据这个交互过程的 并发粒度，垃圾收集器可以被分为如下几类： 停止式( s t o p t l l e w o r i d ) ，如图1 3 ( a ) ，当动态内存被耗尽时，垃圾收集器将完全 停止用户程序，执行一个完整的垃圾收集周期。停止式收集器在没有用户 程序干扰的情况下工作，因而能够得到最精确可达数据集合。但较长的垃 圾收集停顿对用户程序的干扰在某些交互式和实时应用中是不可接受的。 4 趣 留一 堡；i- 一 区一 ；：= |用 第1 章绪论 ( a ) ( b ) ( c ) 图1 3 按交互方式的垃圾收集器分类 渐进式( i n c r e m e n t a l ) ，如图1 3 ( b ) ，一个完整的垃圾收集周期被分割为多个可 以在常数时间完成的部分，每次被触发时垃圾收集器只执行一部分收集工 作。这样就保证了用户程序总是能够在常数时间内得到相应。但由于垃圾 收集器的工作会受到用户程序的影响，渐进式收集器往往只能更加保守的 估计可达数据集合。 并发式( c o n c u 玎e n t ) ，如图1 3 ( c ) ，垃圾收集器和用户程序由不同线程执行，彼 此可以并发工作，但在需要执行某些原子操作的时候需要在线程之间同 步。 分代式( g e n e r a t i o n a l ) 也是一种控制垃圾收集造成的用户程序响应延迟的策略， 并为现代主流垃圾收集器所采用。分代策略的思想主要基于年轻的对象更 容易成为不可达对象的现象。典型的分代收集器将堆划分成多个子堆，采 5 第l 章绪论 用不同的算法对各个堆进行垃圾收集。收集器总是从年轻子堆中分配用户 所需的内存对象，因此年轻子堆上的收集更频繁。由于年轻子堆相对较小， 一次垃圾收集的延迟也相对较小，这样就能够较好地在通常情况下控制垃 圾收集造成的延迟。即便如此，在极端情况下分代垃圾收集的延迟仍然是 无法控制的。因此对于需要严格实时性的应用，仍然必须采用渐进式垃圾 收集。 本文第3 章中将详细讨论典型的停止式和渐进式垃圾收集器的形式安全性验证。 由于并发式垃圾收集器在很大程度上可以看做是渐进式收集器的扩展( j o n e s ， 1 9 9 6 ) ，而分代式收集也可以看做是多种收集算法的综合，本文的后续部分中并 不涉及对这两类垃圾收集策略的详细讨论。 1 1 4 精确的和保守的垃圾收集 在之前的讨论中，我们都假设垃圾收集器能够正确的跟踪内存对象中的引 用( 指针) ，这建立在垃圾收集器能够正确识别引用( 指针) 数据的基础上。通常 情况下，借助语言的定义、编译器收集的信息以及执行环境的支持，垃圾收集器 可以精确地分辨出每个内存单元中存储的数据是否是对其他内存对象的引用。 例如，c a m l 语言在3 2 位系统中使用3 l 位编码的整形数据，余下l 位作为区分整形 数据和指针的标记位；而j a v a 虚拟机在方法区中保存已分配的类对象的内存布局 等等。但在某些情况下，例如在c c + + 语言环境中，垃圾收集器并不能得到额外 的信息来区分普通数据和指针数据。这样，它只能使用内存对象的地址对齐信 息等来保守地估计可达数据集合。这种情况被称为保守式垃圾收集( b o e h ma n d w e i s e r 1 9 8 8 ) 。本文的后续部分将主要讨论精确的垃圾收集，但第5 将对保守式 垃圾收集进行讨论和分析。 1 1 5 垃圾收集的安全性问题 垃圾收集的安全性要求主要体现在两个方面： 1 垃圾收集器自身能够安全地运行； 2 垃圾收集器能够保证用户程序的安全运行。 对于第一个要求，垃圾收集器的算法和实现必须充分考虑用户程序的各种可能 6 第1 章绪论 行为，确保垃圾收集过程中收集器维护的内部状态不会被用户程序破坏。对于 第二个要求，垃圾收集器需要充分了解用户程序的安全性需求。通常来说，用户 程序对垃圾收集器最基本的安全性要求是垃圾收集器永远不破坏可达对象中的 数据和引用关系。 垃圾收集算法大都相对复杂，而渐进式和并发式收集算法更是其中的典型。 为了追求效率，诸如d s w 指针反转( s c h o r ra n dw a i t e 1 9 6 7 ) 之类的算法都相当精 巧，因而不容易让人理解。一些已发表的算法更是被发现存在漏洞( d 独s 帆c ta 1 ， 1 9 7 8 ) 。另一方面，即便有了正确的算法，垃圾收集器的实现也是一个复杂的过 程。包括m o z i l l af i r e f o x 、i n t e m e te x p l o r e r 在内的诸多软件中都出现过垃圾收集 相关的安全隐患( m o z i l l af 0 u n d a t i o n ，2 0 0 7 ，m s t 2 0 0 6 ) 。 为了将垃圾收集排除在安全语言的t c b 之外，我们必须以某种方式确保垃 圾收集的安全性。采用基于p c c 的形式程序验证技术对垃圾收集过程进行严格 的安全性验证就是一种行之有效的方法。 1 2 形式程序验证和携带证明的代码 形式程序验证技术在特定的形式系统( 通常是数理逻辑系统) 中对程序及 其执行环境构造形式模型。并在形式模型上对程序的各种特性进行逻辑推理和 证明。对比于包括程序分析在内的其他形式的程序研究方法，形式程序验证优 势在于它是一种能够保证结果完备性的技术。也就是说，如果能够证明程序满 足特定的性质，那么在相应t c b 的基础上程序就一定满足这个性质。相反的，程 序分析的结果往往只是部分的、可能的结果。 1 2 1经典h o a r e 逻辑 形式程序验证研究始于h o 眦( 1 9 6 9 ) 等提出的h o a r e 逻辑理论( 也被称为公 理语义体系) 。经典的描述程序部分正确性的h o a r e 三元组： 尸lp r o gi q l 是一个数理逻辑断言。它为真表示程序p r o g 从满足以程序状态为参数的逻辑断 言p 的状态开始执行，如果执行终止，终止时的状态将满足断言q 。把状态断言 7 第l 章绪论 对( 只q ) 看做描述程序行为的规范，那么证明h o a r e 三元组为真的数理逻辑证明 也就是对应程序满足其规范的证明。h o a r e 逻辑曾经为开发正确的软件系统构建 了美好的蓝图：如果所有软件系统都相应的正确性证明，那么看上去这个世界 上将不再有软件错误的容身之处了。 但现实并非总是美好的。经典的h o a r e 逻辑也存在着缺陷： 经典h o a r e 逻辑理论上允许使用通用的数理逻辑构造程序的规范( 状态断 言) ，因而具有很强的表达能力。但由于程序正确性往往难于描述和证明， 加之机械化的自动推理迄今为止仍然只能处理一些简单的问题，为复杂的 程序构造基于h o a r e 逻辑的正确性证明至今仍是一个有待研究的问题。 经典h o a r e 逻辑的所保证的安全性和正确性并不是绝对的，丽是建立在庞 大的t c b 之上。例如，我们必须相信h o a r e 逻辑复杂的推理规则是可靠的； 用来书写证明的逻辑是一致、可靠的；逻辑证明的检查是准确无误的；被 证明为安全的源程序确实被准确无误的翻译到可执行代码，等等。 1 2 2 携带证明的代码 由n e c u l a ( 1 9 9 7 ) 首先提出的携带证明的代码( 或携带证明的软件，c e n i f i e d s o f h a r e ) 将经典h o a r e 逻辑改进并应用到汇编程序的安全性质证明中，来支持 分布式计算和移动代码安全策略的实现。p c c 系统最大的特点在于移动代码或 软件包不仅包括了可执行程序，还包括了证明该程序能够安全执行的机器可检 查的逻辑证明。 如图1 4 所示，n e c u l a ( 1 9 9 7 ) 的p c c 系统以如下方式工作： 1 根据代码消费方提供的代码安全性规范，代码生产方编写源代码，并由编 译器生成相应的汇编代码和一定的规范注释； 2 代码消费方提供的验证条件产生器( v c r i f i c a t i o nc o n d i t i o ng e n e r a t o r ，简 称v c g e n ) 从安全性规范和汇编代码中生成相应的验证条件( 简称v c ) 。 3 代码生产方使用自动或半自动推理工具生成该验证条件的证明。汇编代码 和安全性证明一起就构成了一个p c c 包。 4 代码消费方接收到p c c 包后，根据安全性规范和汇编代码重新生成v c ，并 将v c 和p c c 包中的证明交由证明检查器判断。如果判断通过，p c c 包中的 8 第l 章绪论 图1 4p c c 系统构成 代码就可以安全的在代码消费方的硬件上执行了。 p c c 在一定程度上克服了经典h o a r e 逻辑存在的问题，为形式程序验证研究 带来了新的活力。具体来说： p c c 将关注的重点集中于程序的安全性而不是正确性证明上。由于安全性 的定义相对简单而系统，因此在大多数情况下程序的安全性证明都能够通 过机器辅助的自动或半自动推理来完成，简化了证明构造过程。 p c c 采用计算机辅助的证明和证明检查。相对于写在稿纸上的证明和人工 证明检查来说，这种方式提高了证明检查的可靠性。 p c c 的规范、证明构造和证明检查都在汇编语言级完成，从而将编译器排 除出了t c b 。 比较有代表性的p c c 系统包括t o u c h s t o n ep c c ( n e c u l a ，1 9 9 7 ) 、类型化汇编 9 第l 章绪论 语言( m o 币s e t te ta 1 ，1 9 9 9 a ) ( 耐p e da s s e m b l yl a n u g a g e ，简称t a l ) 、验证汇编编 程( y ue ta 1 ，2 0 0 4 ) ( 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 ) 等等。它们使用 了多种多样的程序推理系统，包括h o a r e 逻辑系统，类型系统等。相应的，它们的 安全性规范复杂程度以及安全性证明的产生和检查方式也各有差异。 1 2 3 基础的携带证明的代码 为了最小化p c c 系统的t c b ，a p p e i ( 2 0 0 1 ) 提出了基础的携带证明的代 码( f o u n d a t i o n a lp c c ，简称f p c c ) 。一个典型的f p c c 系统构成如图1 5 ，它包 括： 作为整个f p c c 验证框架基础的元逻辑( m e t al o g i c ) 。它通常是在计算机 辅助定理证明工具中实现的高阶谓词逻辑等通用逻辑。元逻辑及其证明检 查器是系统t c b 的一部分。 在元逻辑上构造的抽象机器模型。抽象机器模型的操作语义模拟对应的程 序运行环境。我们必须相信抽象机器模型确实正确地刻画了真实的机器， 所以抽象机器模型也是t c b 的一部分。 根据抽象机器模型的操作语义和具体应用的安全性需求设计的程序推理系 统( 程序逻辑) 。推理系统通常包括规范语言语法和推理规则，用来编写程 序的安全性规范和验证相应的程序代码。程序推理系统对操作语义的可靠 性可以在元逻辑中得到证明，因而可以将它排除出t c b 。 在元逻辑上构造的类似验证条件产生器、推理系统证明检查器之类的证明 辅助工具。因为可以在元逻辑中证明这些工具的正确性，它们也可以被排 除出t c b 。 使用程序推理系统定义的规范语言编写的程序安全性规范。同样的，我们 也必须相信这些安全性规范确实代表了程序真正的安全性需求，因而安全 性规范也必须作为t c b 的组成部分。 程序满足其安全规范的证明。这个证明使用程序推理系统提供的推理规则 以及相应的辅助工具来完成。把它和推理系统的可靠性证明以及辅助工具 的正确性证明结合起来，就得到了程序在元逻辑中的基础安全性证明。 如果程序的基础安全性证明通过了元逻辑的证明检查，那么在图1 5 中的t c b 的 l o 第l 章绪论 图1 5f i c 系统构成 基础上我们可以相信这段程序确实能够安全地在真实机器上执行。 形式研究方法通过使用数理逻辑等形式系统为真实世界中的事物和现象构 造形式模型，并在形式模型上对这些事物和现象的性质进行推理和证明。但形 式模型和真实世界之间始终存在着差距。形式研究方法能够通过构造更加真实 的模型来缩小这个差距，但不能完全消除它。正因为如此，基于f p c c 的形式程 序验证也并不能够做到完全消除t c b 。 另一方面，对于任何形式程序验证方法来说，元逻辑、机器模型和安全性规 范都是t c b 的组成部分。相对于图1 4 中的p c c 系统，f p c c 系统将程序逻辑、验 证条件产生器等部分排除在t c b 之外，从而达到了最小化t c b 的目的。同时，从 图1 5 中可以看到，使用f p c c 框架进行形式程序验证的难度并不会比使用传统 的p c c 框架有显著的增加，因为在f p c c 框架下程序的安全性证明仍然可以使用 特定的程序逻辑，而无需在元逻辑上直接构造的。 本文中的全部验证工作都在最小化t c b 的f p c c 系统中完成。为了更好地介 绍这些工作，本文第2 章将详细地给出一个f p c c 程序验证系统的形式描述。 第l 章绪论 1 3 相关研究工作 本文工作建立在大量已有的关于形式程序验证，特别是垃圾收集相关验证 的工作之上。本节回顾一些有代表性的研究工作。 1 3 1 形式程序验证 除了第l ，2 节中介绍的h o a r e ( 1 9 6 9 ) ，n e c u l a ( 1 9 9 7 ) ，a p p e l ( 2 0 0 1 ) 等工作，近年 来还有很多在h o a r e 逻辑和p c c 】f p c c 领域的相关研究。 类型化汇编语言( t a l ) 作为一种重要的p c c 技术一直是本领域的研究热点， 这其中包括了( m o 州s e t te ta 1 ，l9 9 9 a ，b ，h a i n i de ta 1 ，2 0 0 2 ，c i a r y ，2 0 0 3 ，h a w b l i t z e l e ta 1 ，2 0 0 7 ) 等工作。吖儿将高级语言的类型信息保持到汇编语言上，构成了携 带类型的汇编代码。通过在代码运行前进行类型检查，代码消费方能够检查 代码是否是类型安全的。而t 札类型的可靠性就保证了类型安全的代码能够安 全的运行。h a m i de ta 1 ( 2 0 0 2 ) ，c r a 巧( 2 0 0 3 ) 的后续工作采用f p c c 的思想在元逻 辑上构造了整个t 札系统，进一步减小了t a l 的t c b 。虽然相对于基于h o a r e 逻 辑的p c c 系统来说t a l 所提供的类型安全的表达能力相对较弱，但在多数情况 下卫让的类型推导和类型检查过程都能够自动完成。目前，基于 儿的技术已经 成功地应用在c y c l o n e ( m o m s e t t e ta 1 ，1 9 9 9 b ) 和s i n g u l a r i t y ( h a w b l i t z e le ta 1 ，2 0 0 7 ) 等大型软件系统中。 耶鲁大学的r i n t 小组长期进行以验证汇编编程( c a p ) 为代表 的p c c f p c c 相关研究。各种版本的c a p 已经能够方便地验证包括支持包含 函数调用( f e n g e ta 1 ，2 0 0 6 ) 、多线程并发( y ua n ds h a o ，2 0 0 4 ，f e n ga n ds h a o ，2 0 0 5 ) 、 函数指针( n ia n ds h a o ，2 0 0 6 ) 、自修改代码( c a ie ta 1 ，2 0 0 7 ) 等复杂特性的汇编代 码。而他们的开放式f p c c 验证框架( f e n ge ta 1 ，2 0 0 7 b ) 能够支持多种使用不同 推理方法验证的代码的链接，从而构造完整的f p c c 软件。本文工作正是建立 在r i n t 小组的f p c c 研究基础之上。第2 章将给出本文工作所使用的f p c c 框架的 形式描述和介绍。 分离逻辑( s e p a n i o nl o g i c ) ( i s h t i a qa n do h e 锄，2 0 01 ，r e y n o l d s ，2 0 0 2 ， o h e 锄e ta 1 ，2 0 0 4 ，b o m a te ta 1 ，2 0 0 5 ，p a r k j n s o na n db i e 咖a n ，2 0 0 8 ) 是近年来 最成功的对h o a r e 逻辑的扩展工作。通过将描述内存资源的逻辑连接词引入 1 2 第l 章绪论 到h o a r e 逻辑的断言语言中，分离逻辑能够很好地描述低级语言的内存行为。而 其局部推理( l 0 c a lr e 越o n i n g ) 的思想( o h e 锄e ta 1 ，2 0 0 1 ) 能够支持对程序进 行模块化地验证，并能够很好地扩展到对并发程序的验证当中( o h e 锄，2 0 0 7 ， l f e i a d i sa n dp a r k i n s o n ，2 0 0 7 ，f e n ge ta 1 ，2 0 0 7 a ) 。本文工作使用分离逻辑来描述 垃圾收集过程中的内存状态，文中涉及到的分离逻辑概念和定义会在第2 章给 出。 s o r ( p a u le ta 1 ，2 0 0 7 ) 项目旨在研究如何设计和改进相关的形式程序验 证工具和技术，并对完整的计算机系统进行形式验证。该项目希望验证的软 件系统包括操作系统、编译器等等，当然也包括本文工作所关注的垃圾收集 器。s i n g u l 枷t y ( h u n ta n dl a m s ，2 0 0 7 ) 项目是由微软研究院开展的针对下一代操 作系统的研究。该项目大量使用了基于c 的安全语言，以及以t a l 为代表的形 式验证技术，以期