（计算机科学与技术专业论文）一个出具证明编译器系统的设计与实现.pdf

摘要 摘要 随着软件逐渐被应用到国家、社会的更广、更深的领域中，随之而来的软 件安全性问题也不容忽视。重要领域、行业的关键软件的安全性问题尤为迫切， 关键软件的安全漏祸让国家和社会蒙受了巨大的损失。现有的保证软件安全的 方法主要依靠软件测试，这种方法只能保证经测试的特定情状不出错，未经测 试的或者无法测试的情况下的行为往往不可知。通过形式化程序的性质，并给 出形式化证明的方法，被称之为形式化程序验证，这种方法是提高软件安全性 的一个有效途径且前人已经取得了丰硕的成果。 程序验证方法能够从理论上保证软件不发生程序中禁止的错误，而出具证 明编译器技术结合了编译器技术和程序验证方法，它作为验证编译器的一个重 要分支，在生成目标代码同时，给出目标代码对应的安全证明。出具证明编译 器的出现降低了形式化程序验证的开销，它能够( 半) 自动地给出形式化的证 明。 本实验室前期也完成了一个出具证明编译器的原型系统，但它不能够自动 产生证明，这个缺陷极大的制约了其功用性和实用性，因此我们在吸取前期原 型系统的经验后，重新设计的一个出具证明的编译器。新的编译器处理一个类c 的p o i n t e r c 语言，它保留了c 语言的动态存储管理的特性，便于我们研究存储 安全方面的隐患；同时我们设计了一种断言语言方便程序员书写安全规范。出 具证明的编译器除了完成传统的代码编译和代码发射外，还将源级的安全规范 翻译到目标级。在目标级包含一个验证系统，该验证系统中的验证条件产生器 根据翻译得到的安全规范，生成程序对应的验证条件，验证条件包括整型断言 和指针断言两类：其中整型断言是机器模型上变量值的约束关系谓词，指针断 言是关于指针表示信息是否等价的谓词，且指针断言中的指针变量可以用整型 断言中的变量来精确地描述其在堆中的偏移，能够描述更复杂的性质。目标级 验证系统中还包括一个定理证明器，它能够自动地产生两种验证条件的证明： 整型断言的自动证明主要借助于一个整数谓词自动证明算法和一个将目标机器 模型上的寄存器变量、栈变量和堆变量范化成一种符号化变元的算法；指针断 言的自动证明通过计算满足同种性质的指针的闭包集合是否等价来证明指针蕴 含断言的前后件是否等价，从而得到指针断言的证明。此外我们还设计实现了 摘要 一个定理检查器，它从文件中读取我们产生的携证明代码，经词法、语法分析 无误的程序，迸步较验其证明和代码的合法性。这样我们不但提供了一种对 产生的携证明代码机器自动检查的方法，还将编译器模块排除出信任基础，增 强了系统的可信性。同时我们通过代表性的示例程序对系统可用性进行了实验 评测，实验结果也在本文末尾给出。 本文介绍的系统实现了一个可信计算框架，这是对程序验证的一个新的试 验，其中的经验教训可作为今后完善出具证明编译器系统的借鉴。 本文由中国国家自然科学基金项目( 6 0 6 7 3 1 2 6 ，9 0 7 1 8 0 2 6 ) ，i m e l 中国研究中心 资助。 关键词：软件安全，程序验证，出具证明编译器，指针断言，整型断言。验证 条件，验证条件产生器。定理证明器 u a b s t r a c t a b s t r a c t s o f h a r eh a sb o o m o di nm o r ea n dm o r e e l d s ，a n d 也ea c c o m p a n y i n gs a f e t ) ， h a z a t d sc a n tb en e g l e c 协b l ea n ym o r e t h es a f e t yc r i t i c a ls o 胁a r ef a u l t si nc r i t i c a l 五e l d sa r ee v e ns e v e r e t h o s ef 乱l t sh a db m u g h te n o r o 岫sd 帅a g et oo u rc o l l l l t 哆 t h ec u r r e n tw i d e l yu s e dm e t l l o dt oi n c r e a s es o f c w a r es a f e t yi ss o 角a r et e s t i n g ，w l l i c h c 锄o i l l ye n s u r el l st h et e s t e dp a 廿l sa r es o u n d ，a r eu 1 1 | ( i l o w nt ot 1 1 ep a t h st l l a ta r e n tb e t e s t e do rc a n tb et e s t e df o rs o m er e a s o n s t h ef o m l a lp m g r a mv 甜f i c a t i o n ，w h j c h f i r s t l yf o 珊a l i z e sp r o g r 枷p r o p e n i e st h e ng e n e r a t e sf o n n a lp r o o f s ，s e e m st ob ea e 娲c t i v ew a y ，a 1 1 di th a so b t a i n e ds o m ea c h i c v e m e n t s p r o 盯锄v c r i f l c a t i o ni saf b 肌a lt h e o r i c a im e t h o dt oe n s u r es o 丘w a r e 仔e eo f f o r b i d d e n r s w h i l em ec e n i 旬i n gc o m p i i e r ，w h i c hc o m b i n e st l l et e c m i q u e si n c o m p i l e ra n dp r o 掣蛐v 甜f i c a i i o n ，a i d st h ep r o g r a mv e r i f i c a t i o na n dd e c r e a s et h e c o s to fp r o g r 锄v e r i n c a t i o n t h ec e r t i 母i n gc o m p j l e rc o m p i l e st 1 1 es o u r c ec o d e sa 芏1 d e m “sa s s 锄b l yc o d e s ；i ta l s og e n e r a t e st h ec o r r e s p o n d i n gp m o f s 0 u rl a bh a df i n i s h e dac e r i t i 母i n gc o m p i l e rp r o t o t y p es y s t e m b u ti tr e s 研c t st l l e s y s t e m s 缸c t i o n a l i t ya 1 1 dp r a c t i c a l 酊t l l a tt h ep r o t o y es y s t e mc a l l tg e n c r a t ep r o o f s a u t o m a t i c a l ly s oi i lo u rn e wc e r t i f y i n gc o r n 【p i l e r sd e s i g n ，w eh a ds t u d i e dt h e c x p e r i e n c ea 1 1 d1 e s s 伽sl e a n l tf r o mp r e v i o u sp r o j e c t o u rn e ws y s t e mc o n l p i l e sa c 1 i k el 锄g u a g ep o i n t e r c ，w h i c hp r e s e ( 、，e sc sd y n a m i cm a i l a g e m e n tf e a t u r e ss ot h a t w ec a i ld om r t h e rr e s e a r c ho nt h em e m o r ys a f e t yh 越：a r d s a l s o ，w ed e s i g naa s s e n i o n l a n g u a g et ow r i t es a f e t ys p e c m c a t i o n s b e s i d e sc o m p i l e ss o u r c el a l l g u a g ei na 呻i c a l c o m p i l e r ，a u rc e r i t y f i n gc o m p i l e ra l s o t 珊s l a t e ss o u r c e - l e v e i ss p e c 谕c a t i o ni n t o 嬲s e r n b l yl e v e l t h ea s s e m b l yv e r i f i c a t i o n 疗a m e w o r kl o c a t e d i nn e ws y s t e m s b a c k e n di n c l u d e sv e r i f i c a t i o nac o n d i t i o ng e n e r a t o rm o d u l ea i l dat h c o r e mp r o v e r m o d l l l e t h ev e 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 rg e n e r a t e st l l ea s s e m b l y c o d e s v e r i 丘c a d o nc o n d i t i o n s 。t h o s ev e r i 6 c a t i o nc o n d i t i o n sc a nb ec l a s s i f i e di m oi n t e g e r a s s e r t i o na 1 1 dp o i n t e ra s s e r t i o n i i l t e g c ra s s e r t i o n s a r e p r e d i c a t i o n sa b o u t 廿1 e r e s 伍c t i o nr e la t i o n s h i pa m o n gt h em a c h i n em o d e l si n t e 唱e rv a r i a b l e s ；w h i l ep o i n t e r 嬲s e n i o n sa r ep r e d i c a i i o n sa b o u tm ei n f o n a t i o ne q u a l i t yr e l a t i o n s h i p 锄o n gp o i m e r t t i a b s t r a c t v a r i a b l e s p o i n t e ra s s e m o n sv 撕a b l e sc a l lu s ea 1 1i m e g e rv 耐a b l et oa c c u r a t e l y d e s 嘶b em eo 施e ti nt h eh e a p ，a 1 1 di nt 1 1 i sw a yw cc a l le x p r e s sm o r ec o m p l e x a s s e r t i o 璐t h em e o r e mp r o v e rc a ng e n e r 砒ep r o o f sf o rt h et 、v ol 【i n d s a s s e m o n s a u t o m a t i c a l l y i n t e g e ra s s e r t i o n sp r o v em a i n l yc o m r i b u t et 0ai n t e g e rp r e d i c a t i o n a u t o m a t ep r o v i n ga i g o r i t 王l i l la i l daa l g o r i t w h i c ht r a n s l a t er e g i s t e rv a r i a b l e s ，s 切c k v 撕a b l e sa 1 1 dh e 印v a r i a b l e si n t ou n i f i e ds y m b 0 1 - f b mv 撕a b l e s t op o i n t e ra s s e n i o n ， 、v ef i r s tc a l c u l a t e 血ea l i a sc l o s u r es e to fp o i n t e rv 撕a b l e s ，a n dt 1 1 e nd e t e n 】n i n e w h e t h e rt h e 卸把c e d e ma n dt h ec o n s e q u e n to fi m p l i c a t i o nc o m 血e q u a l i 耐b m a t i o n i fs o ，w ep r o v e 血ep o i n t e ra s s e m o n a l s o ，w ed e s i g nap r o o fc h e c k e r 1 1 1 ep r o o f c h e c k e rf i r s tr e a d sp r o o fc a n 了i n gc o d e sf r o mm e s ，a i l dt h e nd 0s o m el e x i c a la n d s y r l t a xp a r s i n g i f n ol e x i c a la 1 1 ds y n t a ) ( e r r dr ，t l l ep m o f c h e c k e r 州uc o m i n u et oc h e c k w h e m e rt l i ep m o f sc l e a v et om ev e r i f i c a t i o nc o n d i t i o n st 1 1 ec o d e ss t a t e d t h ep r o o f c h e c k e rm a l ( e st h ep r 0 0 f sm a c h i n e - c h e c k a b l e ，a i s ol e tu se x c l u d ec o m p i l e ri n o d u l e s 丘d mt h et m s tb a s e ，w h i c hm a k eo l l rs y s t e mm o r ec r e d i b i e i nt h e 血e s i s se n dw ea l s 0 g i v es o m er e p r e s e n t a t i v ee x 咖p l e st ot e s tm es y s t e m sa v a i l a b i l i 够 t h en e ws y s t e mw ei n t r o d u c e di nm i st h e s i sa c h i e v e sac e n i 母i n gc o n l p u t e 丘锄e w o r k t h es y s t e mc a nb et r e a t e da san e we x p e r i m e n to nt h e 、v a yo fp m g r a m v 甜f i c a t i o nr e s e a r c h t h el e s s o n sa i l de x p 甜e n c ew el e a m tf b mt 1 1 es y s t e m sd e s i 9 1 1 w i l l 岫d o u b t e d l yh e l p m lf o rm t h l l ri m p r o v e m e ma i l dr e s e a r c h 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 l l r a ls c i e n c ef o u n d a t i o n 吼d e r g r a n t n 0 6 0 6 7 3 1 2 6 ，g r a i l t n o 9 0 7 1 8 0 2 6 ，a 1 1 d i n t e l c h i n ar e s e a r c hc e n t e l k e yw o r d s ：s o f c w a r es a f b 吼p m g r 砌v e r i f i c a t i o n ，c e r t i 母i n gc o m p i l e r ，p o i l l t e r 踮s e r t i o n ，i m e g e ra s s e n i o n ，v e r i 母c o n d i t i o n ，v 甜母c o n d i t i o ng e n e r a t o r t h e o r e mp r o v e r 中国科学技术大学学位论文原创性和授权使用声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工作 所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含任 何他人已经发表或撰写过的研究成果。与我一同工作的同志对本研究 所做的贡献均已在论文中作了明确的说明。 本人授权中国科学技术大学拥有学位论文的部分使用权，即：学 校有权按有关规定向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进行检 索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 保密的学位论文在解密后也遵守此规定。 作者签名：遏! 盘 2 0 0 8 年劝3 1 日 第l 章绪论 1 1 引言 第l 章绪论 现今，多核处理器的普及使得微型计算机的计算能力得到了极大的提升， 互联网技术和移动通讯技术如g s m 、c d m a 、3 g 等的迅速发展加速了移动计算 终端的普及。越来越多的计算终端需要软件的支持，计算机软件已经深入到我 们的日常生活和社会基础设施中。同时一些关键领域，如银行系统软件、航天 器控制系统、医疗行业软件、通讯行业软件等，则对软件有更多更高的要求。 这些关键领域的软件除了要考虑软件的执行速度和效率外，更多还要关注软件 的可靠性和安全性，因为任何微小的错误都可能导致灾难性的后果。2 0 0 2 年美 国商务部的一份报告就曾指出，由软件缺陷在美国造成的损失每年可达到5 9 5 亿美元。对这些领域的软件，我们希望能够通过付出一些额外的代价来获得对 软件安全性的信心，这个需求直接催生了高可信软件的诞生。 高可信软件是一种必须携带软件满足某些关键性质的证明的软件，这些关 键性质包括安全性、存活性、容错性等。其中安全性是重点，软件的安全性包 括s 疵田和s e c u r i t y 两方面。s 疵t y 是指软件运行时不引起危险、灾难的能力； 而s e c 面母是指软件系统对数据和信息提供保密性、完整性、可用性、真实性保 障的能力。其中可以看出s a f e t y 位于高可信框架的底层，是s e c 吲t y 的基础。黑 客通常利用缓冲区溢出、数组访问越界、悬空指针访问等低级的s a f e t y 错误，来 破坏系统并获得未经授权的控制权等。所以s a f b t y 是高可信软件体系中极为重要 的一环。本文的研究主要是从程序设计语言层面上来尝试解决软件( 程序) 的 s 獭y 。本文以后提及的安全性，如未明确声明均指s a f e t y 。 目前主要通过测试的方法来提高软件的安全性。虽然有各种各样的测试方 法、半自动的测试工具( 框架) 等，这些措施对提高软件安全性起到了一定的 作用，但由于测试方法有其自身的局限性，测试不可能穷举所有可能的执行路 径( 分支) ，或者其测试成本太高、时间太长以至于无法完成。经过测试的软件 依旧存在很多潜在的安全隐患。如何才能得到高可信软件的要求昵? 上世纪七 s a f j t ) ，和s e c u r i t y 在中文中均翻译为安全，此处用英文来区分。 第1 章绪论 十年代提出的程序性质证明( 也称程序验证) 的方法便是一种实现高可信软件 的方法之一。程序性质证明相关的研究在七十年代取得了丰硕的成果 ii 。八十 年代趋于沉寂，9 7 年随着gc 。n e c u l a 发表的p r o o f _ c a n y i n gc o d e ( 简称p c c ) 【2 】， 程序验证焕发了新的生机。gc n e c u l a r 同时为此设计了一个出具证明的编译器 t o u c h s t o n e 【3 】。本文所探讨的编译器即是一个符合p c c 规范的一个类c 语言 p o i n l e r c 的出具证明的编译器。本节接下来介绍些该领域的基本概念。 1 1 1 程序性质证明 程序性质是关于程序变量满足的性质( 约束) 的断言。断言用逻辑的方式 描述一些类型系统不能描述的程序性质。如j a v a 语言在j s r l7 5 4 j 规范中也引入 了断言，并在j a v a 5 中实现。这种断言机制已广泛应用于后续的j a v a 版本中关 于w e bs e n r i c e 、w s d l 等类库中。我们在出具证明编译器系统中用到的程序性 质有：类型约束，i n tv 来表示变量v 的类型是整型；还可以表示和值相关的断 言，例如变量v 的取值在0 到i o 之间：另外一种形式是不变式，常见的不变式 是循环不变式5 ，它是在循环内和循环结束时都能成立的断言。描述了循环要 完成的任务。 程序性质证明，即是证明程序的行为是否满足我们施加给程序的安全性断 言的过程。 1 1 2 被信任计算基础 上世纪七十年代提出了软件安全研究领域的两个基本原则：最小权限原则 和最小被信任计算基础原则。第一个原则指在程序执行过程中，应只给各个实 体分配能够完成任务的最小权限；第二个原则指在被信任计算基础尽可能小的 情况下保证整个系统如预期工作，其中被信任计算基础( t m s t e dc o 川p u t i n g b a s e ， 简称t c b ) 【6 ，7 】指的是实现系统的代码中不能证明为安全或者尚未被证明为安 全时，而不得不给予信任的那些部分。例如所有的计算机硬件必然包含在t c b 中，如果不信任这些硬件，则无法去证明软件的安全性。且从传统的眼光看， 操作系统也被包含在t c b 中。但现代操作系统都包含了进程管理，内存管理和 对硬件支持等服务。所以将整个操作系统纳入t c b 是不符合最小被信任计算基 础原则的。考虑到程序设计语言和编译器是构成操作系统的基础，而现在的主 2 第1 章绪论 流操作系统大都是用不安全的语言( 如c 语言) 实现的，为了减小t c b ，我们 可以从程序设计语言和编译器来自底向上的解决软件安全的问题。 1 2 研究背景及现状 本节先介绍程序性质证明的相关研究，之后介绍验证编译器的相关研究 最后介绍由葛林、刘诚等在0 6 年完成的出具证明编译器原型系统。 1 2 1 程序性质证明的相关研究 程序性质证明的研究主要分为基于类型的方法和基于h o a r e 逻辑的方法。 本小节将首先介绍基于类型的方法和基于h o a r e 逻辑的方法，之后介绍一个应用 h o a r e 逻辑的携带证明代码的方法，最后介绍结合这两种方法的验证汇编程序设 计的方法。 1 2 1 1基于类型的方法 类型在程序语言的设计中扮演着重要的角色，在描述程序安全规范上也有 着广泛的用途。类型系统是一种静态检查程序行为的语法方法，编译器根据变 量声明或推导得知程序中变量、值的类型信息，并检查这些变量、值的使用是 否是类型安全的。类型系统的可靠性保证了通过类型检查的程序不会有类型错 误。传统的类型系统的表达能力较h o a r e 逻辑要弱，不能够描述某些安全性质。 但今年来也涌现了一批旨在增强类型系统表达能力的新的类型系统：对传统类 型系统进行类型细化( t y p er e f i n e m e m ) 的研究 8 ，9 】：基于依赖类型的命令式语 言x a l l a d u 【1 0 】以及类型化汇编语言( t y p e da s s e m b l yl a n g u a g e ，简称霸i l ) 1 l ， 1 2 ，1 3 1 等。这些工作扩充了现有的类型系统，使得它们可以捕捉更丰富的安全性 质。 基于类型系统进行程序验证的方法的优点是简单且容易实现：通过类型系 统的检查排除有类型错误的程序，能够保证无类型错误，而且这些扩充类型系 统的类型检查能实现自动化。但这种方式的缺点是：类型系统的表达能力越强， 该类型系统就越复杂难懂，这使得使用该类型系统的程序员难以上手，较难被 更多的程序设计人员所接受，同时类型检查算法也不易实现。 3 第1 章绪论 1 ，2 。1 2 基于h o a r e 逻辑推理的方法 h o a r e 逻辑最早见于f l o y d 【1 】和h o a r e 1 4 】在1 9 6 9 年的论文中。基于h o a r c 逻辑的特定语言的公理系统通常由以下两者组成：关于该语言的断言；用于推 导断言成立的推导规则。例如，h o a r e 逻辑中的部分正确性断言由h o a r e 三元组 构成：尸 q ) r ，其中p ，尺表示命题，q 表示程序语句。该三元组表示：如果 当q 执行前命题p 为真，那么或者g 不终止，或者q 终止且r 成立。另外h o a r e 逻辑中包含一些常见的推导规则，如赋值公理、组合规则和迭代规则。 规则1 1 赋值公理p 【z hp 】缸：= p 尸。工是左值变量，p 是表达式，p 是命 题断言。p 口卜e 表示把p 中自由出现的x 用p 代换后的命题。 删1 2 组合删等拦警一心厶r 是命麟言倒、缈 是相邻的程序语句。 规则1 3 迭代规则瓦罚主竺。b 是w l l i l e 循环条件表达式， s 是循环体语句，p 是命题断言，一般称为循环不变式。 利用h o a r e 逻辑进行程序性质证明的框架是：首先定义公理和推导规则。 之后逻辑系统给出基于程序状态的断言规范，这些规范用于描述关键程序点需 要满足的条件( 如函数前后条件) 和某些证明提示2 ：最后再由程序员根据推导 规则手工地或借助某些证明辅助工具( 如c o q 【1 5 】) 半自动的给出断言成立的证 明。 h o a r e 逻辑用于程序正确性证明似乎预示着所有计算机程序的正确性都可 以形式化的严格证明。h o a r e 逻辑诞生后的十几年里，大量的工作由此展开，以 便来验证更复杂的语言结构，寻求更好的方式来表示、构造和检查程序性质。 如谓词转移语义 1 6 】、最弱前条件【1 7 】和最强后条件【1 8 j 的观点，以及验证条件 产生器( v e r i f i c a t i o nc 0 n d i t i o ng e n e r a t i o n ，简称v c g ) f 1 9 ，2 0 】和自动定理证明 器【2 1 】迸行程序的验证等。h o a r e 逻辑用于j a v a 【2 2 】语言程序上的验证如【2 3 】。 ：常见的证明提示是循环不变式，因为现有的程序验证方法在验证循环的性质时 候要进行不动点计算，这个计算有时候会不终止，一种常见的做法是要求程序 员给出循环不变式。 4 第1 章绪论 但是h o a r e 逻辑的推理规则并非全是语法制导的，如趣迅41 ：3 垫盐趣巫且 这导致了许多证明无法自动完成。从八十年代起，关于h o a r e 逻辑的研究一度进 入了停滞阶段。一方面是由于形式化描述程序的正确性是非常困难的，另一方 面证明过程不能自动化，而且证明冗长。d e m i l l o 【2 4 给程序的正确性证明下了 一个结论：程序正确性证明“绝不会成功”。 进入九十年代，g e o r g ec n e c u l a 提出了携带证明代码p c c 【2 技术。从此 人们把研究重点放在了对程序安全性质的证明上。这些安全性质通常是关于程 序部分正确性的规范，如“数组下标不能越界”、“指针变量p 不能是n u l l 指 针”等，证明这些规范要比证明程序正确性简单的多。从此h o a r e 逻辑再次受到 广泛关注。 1 2 1 3携带证明代码p c c 最初p c c 框架 2 ，2 5 由n e c u l a 提出，他将h o a r e 逻辑应用到汇编语言的安 全性质证明中，这样可以将编译器排除出t c b 。p c c 的核心思想是可执行代码 和证明捆绑传递，此外它还提出了一个传递安全移动代码的协议。 p c c 框架图见图1 一l ，代码生产方和代码消费方共同协商一套安全策略( 代 码的安全规范) 。代码生产方通过出具证明编译器产生带标注的目标代码和满足 安全规范的证明。出具证明编译器的代码生产方包括代码编译、验证条件产生 器和定理证明器：其中代码编译完成代码；验证条件产生器根据代码和代码中 的标注生成验证条件；定理证明器负责生成这些验证条件的证明。代码消费方 包括验证条件产生器和定理检查器，其中验证条件产生器根据目标代码中的标 注产生验证条件；定理检查器检查携带的证明是否能够证明验证条件产生器生 成的证明。 5 第】章绪论 生产方 消费方 图l - 1p c c 框架图 p c c 传递安全代码中只包含带标注的目标代码和验证条件的证明，并不包 含验证条件。代码消费方接收到p c c 目标代码后，使用和代码生产方同样的验 证条件产生器为目标代码生成验证条件。之后代码消费方不需要为这些验证条 件生成证明( 因为产生证明往往非常耗时) ，而只是验证随代码携带的证明是否 能够证明这些在消费方生成的验证条件。证明检查的过程类似一个类型检查过 程，检查器检验每一步推断是逻辑系统中的一个公理或者是推理规则的一个实 例。验证条件由消费方生成，这防止了恶意代码携带伪造的验证条件来破坏主 机。 p c c 框架具有通用性，能够用来确保包括内存安全、类型安全以及共享资 源限制在内的各种安全性质。p c c 还是一种有效的移动代码传递协议：代码生 成方承担了对代码安全性质的复杂冗长的证明工作，而代码消费方仅包含一个 验证条件产生器和证明检查器，这两个模块功能简单且都能自动化完成，时间 开销也可忽略。之后a p p e l 提出的f p c c ( f o u n d a t i o n a lp c c ) 【2 6 】在原有的p c c 基 础上进一步缩小了p c c 框架中的t c b 。在卜c c u l a 提出的p c c 框架中，p c c 的 逻辑系统中某些公理和推导规则沿用了类型系统中的定型规则和结论，而类型 系统中类型可靠性定理的证明是由手工完成的，不能确保其正确性。而f p c c 则 采用了带有一些基本数学公理的高阶逻辑系统作为基础逻辑，机器语言的操作 6 第1 章绪论 语义以及安全规范能够用基础逻辑定义，证明在基础逻辑上给出，不依赖于特 定的类型系统。 1 2 1 4验证汇编程序设计c a p 类型系统在自动化验证方面见长，而逻辑系统的表达能力较强，这两者具 有很大的互补性。近年来出来了一些结合两种方法的研究，如h x i 在应用类 型系统( a p p l i e dt y p es y s t e m ，简称a t s ) 【2 7 3 0 方面的研究和s h a o 提出的针 对汇编程序验证的框架。下面介绍s h a o 的这个验证框架。 验证汇编程序设计( c e 币目i n ga s s e m b l yp r o 掣a r m i n g ，简称c a p ) 【3 1 】是 s i l a o 和n a d e e mh 锄i d 等提出的一个汇编程序验证框架。它基于一种语法的 f p c c 3 2 】，借助证明辅助工具c o q 1 5 为机器代码产生安全性证明。现有的p c c 系统仅针对安全证明可以自动化产生的程序，许多底层的系统库、函数库( 如 内存管理、线程调度等) 都没有被形式化证明。c a p 实现了机器模型上的内存 管理函数m a l l o c ，矗e 库函数的证明，使得m a l l o c ，舶e 库函数脱离出t c b 中， 提高了系统的可信性。 c a p 可以验证程序的普通属性和正确性。在c a p 框架中，用高阶逻辑定 义安全规范，采用h o a r e 逻辑的推理方式，用户给出程序点程序具有的安全属性。 这样证明由语言类型系统的可靠性证明和逻辑推理组成。每一种符合安全策略 的机器状态都与一个类型正确的程序对应，而机器状态的转换则与程序的计值 联系。这样类型系统的前进性( p r o g r e s s ) 和保持性( p r e s e a t i o n ) 证明可以用 来构造相应的程序安全性证明。而类型系统的前进性和保持性证明比较容易得 到。逻辑推理可借助证明工具完成。因此c a p 可以较简单地得到汇编程序的证 明。 c a p 给出了构造系统底层的验证系统库、验证函数库的方法，减少了传统 p c c 、f p c c 中t c b 的大小。c a p 的思想也得到了进一步的延伸，如c c a p 【3 3 】 和c m a p 3 4 将c a p 的思想应用到多线程安全编程：s c a p 3 5 】在c a p 的基础上 设计了一个灵活的模块化验证框架，该框架包括所有基于栈的控制抽象：函数 调用和返回、尾调用、s e q m p ，l o n g i m p 、弱连续( w e a l ( c o m i 加a t i o n ) 、栈剪切( s t a c k c u n i n g ) 、栈回滚( s t a c ki l i l w i n d i n g ) 、多返回值函数调用、协程、线程上下文切 换；a 帕r e w m c c r e i 曲t ，z h o n gs h a o ，c n u i a o l i n 和l o n g “在 3 6 中提出了一个 7 第1 章绪论 用于验证汇编语言实现的垃圾收集算法的通用框架。此外耶鲁大学的f l i n t 项目 组正在基于c a p 思想来完成一个微型操作系统的验证，该操作系统包括内核、 线程调度、i o 驱动等。 但c a p 和其衍生系列也存在着不足：如需要手工书写汇编代码满足的安 全规范，这个过程是很困难的，安全规范太强或太弱都会导致证明变得极其复 杂甚至不能证明。 1 2 2 验证编译器的相关研究 1 2 2 1验证编译器 验证编译器( v e r i 母i n gc o m p i l e r ) 【3 7 】是现代编译器的一个重要分支。验 证编译器借助数学和逻辑推理检查经它编译的目标代码的正确性。程序的正确 性通过伴随代码的类型、断言、规范和其它额外的标注信息描述。 验证编译器结合了编译器技术和程序性质证明技术，它可以和现有的软件 开发、测试工具结合使用，这样可以验证关键模块的正确性，提高系统的可靠 性。上世纪六、七十年代的软件规模很小，软件市场也很有限，处在发展初期 验证编译器没有引起足够的重视。如今，软件已成为世界性的支柱产业，软件 的规模也很庞大，动辄需要花费上百、上千个入年3 来完成。这种“怪兽”级的 项目让软件测试人员、开发人员望而却步。测试的作用变得微乎其微，开发人 员对“怪兽”的排错往往会带来更多的潜在的错误。人们迫切需要找到一种能 够击败“怪兽”的“银弹”4 。随着计算机科学技术日新月异的发展，方面， 计算机理论的发展带动了自动定理证明器和证明辅助工具的发展；另方面现 代编译器中采用了更为复杂的程序分析技术来检查程序的类型安全性和其它性 质，断言也已经广泛的应用到了单元测试中，如j u n i t 【3 9 】，甚至在j a v a 5 【4 0 】中 已经内置了断言的语法和相应的断言检验的支持。这些工具软件和实践方法的 发展使得验证编译器可行性得到了很大的提高。 叭年：衡量软件工作量的单位，表示一个人一年的工作量。其它常用的单位还 有人月，表示一个人一个月的工作量。相关概念见人月神话【3 8 】。 银弹是欧洲神话传说中杀死浪人的致命武器。 8 第1 章绪论 1 2 2 2验证编译器的主要分支 当前验证编译器的相关研究主要有两个方向：其一是形式化的证明编译器 本身是正确的，即编译器携带一个声明其自身正确性的形式证明，这样的编译 器称为携带证明的编译器( c e 一是e d c o m p i i e r ) ；其二是编译器除了生成目标代码 外，还生成这些目标代码关于其安全规范的形式化证明，这样的编译器被称为 出具证明的编译器( c e r t i 匆i n gc o m p i l e r ) 。 携带证明编译器的发展历史中，m o o r e 首先针对一个简单的特定语言和特 定处理器机械地验证了一个编译器保语义( s e m a n t i cp r e s e 几，a t i o n ) 4 1 】。随后的 研究者对l i s p 语言子集的编译器、j a v a 语言子集的字节码编译器【4 2 和c 语言 子集c o 到d l x 汇编语言的编译器 4 3 】进行了验证。最新的代表成果是l e r o y 对 一个简单的低级命令式语言c m i n o r 的编译器后端进行验证 4 4 】，该后端能够把 c m i n o r 编译到p o w e r p c 汇编代码并带有部分优化，l e r o y 在其研究工作中使用 了证明辅助工具c o q ，并用纯函数式语言完成编程工作。 但另一方面，现代的编译器本身就是个非常庞大、复杂的软件，证明一 个编译器是非常困难的。前人的工作也只是针对非常简单的编译器，这些编译 器往往针对非常小的语言，几乎没有什么优化。从可行性考虑，证明一个编译 后目标程序的正确性比证明编译器本身容易得多。在前文介绍的p c c 框架中， 包括一个n e c u l a 实现的称之为t 0 u c h s t o e 3 】的出具证明的编译器。这个编译器 针对c 语言的一个类型安全的子集s a f c c ，s a f e c 限制了c 语言中的指针类型和 动态存储管理。之后c o l b y 又为j a v a 语言的一个较大子集实现了一个从字节码 到i n t e ix 8 6 目标代码的出具证明编译器s p e c i a l j 4 5 】，s p e c i a l j 按照p c c 的方式 构成底层安全规范和证明。它实现了将p c c 和出具证明编译器技术应用到一定 规模和复杂度的程序设计语言上。和t o u c h 砒o n e 相比，它支持的语言具有更丰 富的特征，如对象表示，动态方法调度和异常处理等，同时它还加入了很多局 部优化和全局优化策略。 9 第l 章绪论 1 3 出具证明编译器原型系统 1 3 。1 原型系统简介 编译器后端 巫型墅口 至垂困 编代码+ 汇编级安全规 毋r 汇编代码i + 目标级验证系统 网整瓣 1 目标级验证条件l 验证条佳厂璺篓1 2 慧罂 竺兰广一弋兰：鲎竺 目标级安全规耙目标级的c 叩证明 汇编代码+ 目标毁安全靓范+ 目标级的c o q i 正明 图1 0p l c c 框架图 本实验室5 的葛林、刘诚、华保健等人在【4 6 4 9 】中设计并实现了一个出具证 明编译器的原型系统p l c c ( p o i n t e rl o g i cc e r t i 匆i n gc o m p i l e r ，简称p l c c ) ，其 框架图见图1 2 p l c c 框架图。p l c c 的源语言是类c 语言p o i n t e r c ，它支持指 针类型和部分动态存储管理。同时还设计了种断言语言p a l ( p o i n t e rl o g i c a s s e n i o nl a i l g u a g e ，简称p a l ) 来描述源级的指针安全的规范。 程序员用p a l 标注p o i n t e 陀源程序。这些带标注的源程序经过传统编译器 前端，产生带标注中间表示。之后这些带标注的中间表示将通过源级验证系统， 冲国科学技术大学苏州研究院软件安全实验室，虹p 丛! g ：女堂望：鱼g ：! 坠 l o 第1 章绪论 在源级证明系统中，验证条件产生器生成源级的验证条件，这些验证条件被保 存在v 文件中，将交给证明辅助工具c o q ，由程序员手工的离线证明。最终，程 序员在c o q 中的证明构成了源级的证明。 带标注的中间表示同时也被编译器后端做进一步的处理，产生汇编代码和 汇编级的安全规范。这些输出交由目标级验证系统产生目标级的验证条件，再 由程序员在c o q 中证明。目标级验证系统和源级验证系统类似。最终，由带标 注的目标代码和目标级的c o q 证明构成了p l c c 后端的输出。 1 3 2 原型系统存在的问题 原型系统提出了一个可信软件开发框架，该框架使程序设计人员可以在源 级书写较丰富的安全规范，提高了程序开发效率；引入了源级验证系统和目标 级验证系统，能够产生符合c o q 规范的定理，由程序员借助定理证明辅助工具 c o a 手工离线地证明源级和目标级产生的验证条件。 但同时我们也看到，原型系统还存在着很大的不足： 1 ) 原型系统中的验证系统( 包括源级和目标级) 实际上只是一个验证条 件产生器，验证系统只是产生要验证的验证条件，之后把这些验证条件的证明 交给程序员来手工离线证明： 2 ) 程序员