（计算机软件与理论专业论文）模块化构造软件系统安全性证明的研究.pdf

中文摘要 摘要 计算机程序正逐步影响到人类社会的方方面面。无论在互畎网还是个 人电脑上，计算机程序的安全问题日益严峻。然而现实世赛中的程序并不 尽如人意，病毒肆虐。网络攻击防不胜防。这些问题都源于程序中潜伏着 许多错误，其中一个小的错误有可能会导致整个软件系统的崩溃。而在诸 多关键的领域，例如核反应堆、航天飞机的控制系统等等，计算机程序的 半点闪失都将带来不可计数的惨痛损失。在软件开发过程中使用形式化的 方法是提高软件质量的途径。在众多的形式化方法中，程序的静态验证是 一种非常可靠的方法。 本文采用方法是在携带证明的代码的框架中静态地验证程序。所谓携 带证明的代码是首先静态地验证代码的安全性，然后将这个验证的详细过 程作为安全性证明附加在程序上。主机在运行程序前检查程序携带的安全 性证明的正确性。如果安全性证明是正确的，那么说明程序满足主机的安 全策略，可以安全地运行而不破坏主机上的软件系统。 本文首先在一个简单的验证框架中定义了程序、抽象机器、抽象机器 的操作语义、安全，还有一个用来静态验证程序的推理系统。此框架可以 用来构造简单的携带证明的代码。然而与以前的许多相关研究一样，此框 架不能很好地支持模块化的程序验证。现实中的大量程序通常使用模块化 的开发方式，模块化的开发方式可以把一个复杂的程序分解为若干个小的 模块，不同的模块分别被开发，最后这些模块可以被链接到一起从而构成 完整的程序。模块性在软件工程方面占有重要的地位。程序静态验证也应 该具备模块性，即不同模块的验证可以分别进行，然后链接成为完整的安 全性证明。另方面，一个程序的不同模块可能是不同风格的代码，难以 使用同一种验证推理系统去验证所有的模块。 本文在简单验证框架上进行扩展，使之支持模块化验证。在此模块化 框架中不同的模块可以分开进行验证并分别得到各自的安全性证明，模 块在链接的同时安全性证明也被链接到一起，从而得到整个程序的安全性 证明。而且此框架支持不同的模块使用不同的验证逻辑进行验证。框架的 中文摘要 特点是采用一个抽象的程序推理系统，它支持良好的模块验证。多个验证 推理系统可以被统一嵌入到这个抽象的程序推理系统中。通过采用这种方 法，一个模块不管使用哪些推理系统进行验证，只要这个验证推理系统可 以被嵌入到抽象层次上，那么这个模块的安全性证明就可以被转换成抽象 的推理系统中的安全性证明。 本文研究了如何将一个支持控制栈推理的验证推理系统( 被称 为s c a p ) 嵌入到验证框架中，并移植了一个已有的动态内存分配模 块( n e w p a i r l 。同时本文还研究了如何将一个类型化的验证推理系统( 被称 为t a l p ) 嵌入到验证框架中，并验证了一个小的调用动态内存分配的模 块( m a i n l 。最后本文介绍了如何将两个使用不同的推理系统验证的模块连同 安全性证明链接到一起。 本文还研究了框架中的各个模块的安全性证明产生的自动性问题。本 文不仅提出了验证推理系统s c a p 中的验证条件生成器，而且提出了验证推 理系统t a l p 的类型检查器。通过验证条件生成器与类型检查器的可靠性证 明。模块的安全性证明的构造过程被大大简化，有利于验证规模较大的模 块。 文中所有的形式化定义，形式化描述以及证明都己使用的定理辅助证 明工具c o q 实现。因此所有的证明，包括框架的性质证明，示例程序的安全 性证明的正确性可以使用机器自动检查。 本文的工作虽然是对模块化验证框架的研究的初步探索但是本文中 的验证框架所表现出的良好的模块性为大规模程序的安全性验证带来良好 的应用和研究前景。 本文由中国国家自然科学基金资助f 编号6 0 6 7 3 1 2 6 ) 。 关键字：软件安全，程序验证，汇编语言，携带证明的代码，模块化验证 i 】 英文摘要 a b s t r a c t a sc o m p u t e rk e e p st h et r e n do fe x e r t i n gi n f l u e n c eo v e rv a r i o u sa s p e c t so f h u m a ns o c i e t y , s a f e t yi s s u eo fc o m p u t e rp r o g r a m si sb e c o m i n gm o r ea n dm o r e t h r e a t e n i n go nb o t hi n t e r n e ta n dp e r s o n a lc o m p u t e r s u n f o r t u n a t e l y , h rf r o m e n s u r i n gt h es a f e t yo fa l lp r o g r a m s ，t h ee n d l e s s l ye m e r g i n gv i r u sa n dn e t w o r k a t t a c ka l w a y sp u to u rc o m p u t e r si ng r e a td a n g e r s u c hm e n a c e sa r er e s u l t e d f r o mt h el u r k i n gb u g si np r o g r a m s ，a n de v e nas m a l lb u g g yp r o g r a mm a y c a u s et h ec r a s ho ft h ew h o l es o f t w a r es y s t e m ，i nm a n yp a r a m o u n ts y s t e m s l i k en u c l e a rc o n t r o ls y s t e ma n da e r o s p a c e p l a n ec o n t r o ls y s t e m ，s u c hb u g s w o u l db eu n p a r d o n a b l e f o r m a lc e r t i f i c a t i o nm e t h o d o l o g yd u r i n gs o f t w a r e d e v e l o p m e n ti sa na p p r o a c ht oi m p r o v eq u a i l t yo fp r o g r a m sa m o n g a l lt h e f o r m a lc e r t i f i c a t i o nm e t h o d s ，s t a t i cp r o g r a mc e r t i f i c a t i o nd i s t i n g u i s h e si t s e l f a sar e l i a b l ea n df e a s i b l em e t h o d t h et e c h n i q u ea d o p t e db yt h i sp a p e ri sc a l l e dp r o o s c a r r y i n gc o d ep r o o f c a r r y i n gc o d ei sap r o g r a mw i t ha t t a c h e dp r o o f , w h i c hd e s c r i b e st h ew e l l - f o r m e d n e s so ft h ec e r t i f i e dp r o g r a m b e f o r er u n n i n gt h ep r o g r a m ，ah o s tw i l l c h e c kt h ev a l i d i t yo ft h ep r o o ft oe v a l u a t et h es a f e t yo ft h ep r o g r a m t h e v a l i d a t i o no ft h ep r o o fi n d i c a t e st h a tt h es a f e t yp o l i c yo ft h eh o s tw i l ln o tb e v i o l a t e db yt h ep r o g r a ma tr u n t i m e t h i sp a p e rf i r s t l yp r e s e n t st h ed e f i n i t i o no ft h ec o n c e p t so fp r o g r a m ， a b s t r a c tm a c h i n e ，o p e r a t i o n a ls e m a n t i c s ，s a f e t yd e f i n i t i o na n dac e r t i f y i n g s y s t e mi nap r o o f - c a r r y i n gc o d ef r a m e w o r k t h ec e r t i f y i n gs y s t e mi su s e dt o c o n s t r u c ts i m p l ep r o o f - c a r r y i n gc o d e s n o n e t h e l e s s 3 si nt r a d i t i o n a lr e s e a r c h o np r o o f - c a r r y i n gc o d ef r a m e w o r k s ，m o d u l a rc e r t i f i c a t i o ni sn o ts u p p o r t e db y t h i sf r a m e w o r ke i t h e r a si sw e l lk n o w n ，r e a l i s t i cp r o g r a m sa r ed e v e l o p e d i nam o d u l a rw a y t h ew h o l ec o m p l i c a t e dp r o g r a mm a yb ed i v i d e di n t o s e v e r a lm o d u l e s ，w h i c ha r ee a s i e rt od e v e l o ps e p a r a t e l y , a n da l lt h em o d u l e s c a nb el i n k e dt of o r mt h ec o m p l e t ev e r s i o n t h e r e f o r e ，m o d u l a r i t yp l a y sa l u 英文摘要 v e r yi m p o r t a n tr o l ei nt h em o d e r ns o f t w a r ee n g i n e e r i n g ，w h i c hn e c e s s i t a t e s t h em o d u l a r i z a t i o no fp r o g r a mc e r t i l y i n g ，t oc o m p l i c a t et h ep r o b l e m ，t h e s e m a n t i c so fd i f f e r e n tm o d u l e sm a yb ei nd i f f e r e n ts t y l e sa n di m p o s e sm u c h d i f f a c u l t yt ob ec e r t i f i e di nas a m ec e r t i f y i n gs y s t e m i nt h i sd i s s e r t a t i o n ，ap r o o f - c a r r y i n gc o d ef r a m e w o r kt os u p p o r tm o d u l a r c e r t i f i c a t i o ni sp r o p o s e d i nt h i sf r a m e w o r k ，a f t e rt h es e p a r a t ec e r t i f i c a t i o n ， d i f f e r e n tm o d u l e sw i t ha t t a c h e dp r o o fc a nb el i n k e dt o g e t h e rt of o r mac o m - p l e t ep r o o f - c a r r y i n gc o d ep a c k a g e ，a d d i t i o n a l l y , d i f f e r e n tm o d u l e sc a l lb e c e r t i f i e di nd i f f e r e n tc e r t i f y i n gs y s t e m s t h eb a s i ci d e ab e h i n dt h ef r a m e w o r k i st h ea d o p t i o no fa l la b s t r a c tp r o g r a mr e a s o n i n gs y s t e m ，w h i c hs u p p o r t s g o o dm o d u l a r i t y , a n di nw h i c ho t h e rc e r t i f y i n gs y s t e m sc a nb ee m b e d d e d t h i sd i s s e r t a t i o nd e l v e si n t ot h ee m b e d m e n to fac e r t i l y i n gs y s t e m ( s c a p ) ， w h i c hs u p p o r t sc o n t r o ls t a c kr e a s o n i n g ，a n dt h et r a n s p l a n to ft y p e dc e r t i f y i n g s y s t e m ( t a l p ) i n t ot h ep r o o f - c a r r y i n gc o d ef r a m e w o r k t 怕m o d u l e s ，m a i n c e r t i f i e di nt a l pa n dn o - p a i rc e r t i f i e di ns c a p ：a sw e l la st h e i rp r o o f , c a n b el i n k e dt o g e t h e r t h i sd i s s e r t a t i o na l s oa d d r e s s e st h ep r o b l e m so fs a f e t yp r o o fa u t o m a t i c g e n e r a t i o n av 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 rf o rs c a pa n dat y p e - c h e c k e r f o rt a l pa r ep r o p o s e d e m p l o y i n gt h e s et o o l s t h ec o n s t r u c t i o no fs a f e t y p r o o fo fe a c hm o d u l ea r el a r g e l ys i m p l i f i e d ，w h i c hp r e d i c a t e st h ep o s s i b i l i t y o fl a r g e rs c a l em o d u l e sc e r t i f i c a t i o n a l lt h ef o r m a ld e f i n i t i o n s ，d e s c r i p t i o n sa n dp r o o f sh a v eb e e nf o r m a l i z e d i nt h ep r o o fa s s i s t a n tc o q s oa l lt h et h e o r e m sp r e s e n t e di nt h i sd i s s e r t a t i o n a r em a c h i n e - c h e c k a b l e t h ew o r ko ft h i sd i s s e r t a t i o ni st h ef i r s ts t e pt om o d u l a r i t yc e r t i f i c a t i o n f r a m e w o r k ，w h i c hd e m o n s t r a t e sg o o dm o d u l a r i t y , a n db r i n g sab r i g h tp r o s p e c t t ot h er e s e a r c ha n da p p l i c a t i o no fh 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 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 y w o r d s ：s o f t w a r es a f e t y , p r o g r a mc e r t i f i c a t i o n ，a s s e m b l yl a n g u a g e ，p r o o h c a r r y i n gc o d e ，m o d u l a rc e r t i f i c a t i o n 插图 插图 p c c 框架， n e c u l a 等人的p c c 框架 a p p e l 等人的f p c c 框架 h a m i d 等人的f p c c 框架 c r a r y 的f p c c 框架 s h a o 等人的f p c c 框架 本文的f p c c 框架 个简单的f p c c 框架 个简单的f p c c 框架( 侧面) 抽象机器模型定义 抽象机器操作语义 c a p 推理规则 支持模块化验证的框架 o c a p 规范定义， 0 c a p 规则， o c a p 规则( 续) ， 链接策略， s c a p 规范结构 s c a p 推理规则， 函数的调用与返回， v 2 2 2 3 2 7 2 9 3 3 6 9 n n m 玷玛 盯鸽弧以 够加n h 他“ m 牝粥“躺 弛粥“弘 “纰档 插图 函数的尾调用与返回。 s c a p 推理规则( 续) s c a p 验证条件产生器 分离逻辑 动态分配算法n e w p a i r 与其内存数据结构 s c a p 规范在o c a p 中的定义 t a l p 类型系统语法定义 t a l p 定型规则 t a l p 指令规则， 合一算法， h d q i 胃词定义 一个调用n e w p a i r 的模块m a i n 。 t a l p 类型规范在o c a p 中的定义 v i 记他粥两缸 鲫缸g卯g毗 1 l ， ， ， “蛳”蛐蚰 鼬锄瞄：耄 中国科学技术大学学位论文相关声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工 作所取得的成果。除已特别加以标注和致谢的地方外，论文中不 包含任何他人已经发表或撰写过的研究成果。与我一同工作的同 志对本研究所做的贡献均已在论文中作了明确的说明。 本人授权中国科学技术大学拥有学位论文的部分使用权， 即：学校有权按有关规定向国家有关部门或机构送交论文的复印 件和电子版，允许论文被查阅和借阅，可以将学位论文编入有关 数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、 汇编学位论文。 保密的学位论文在解密后也遵守此规定。 5 作者签名：空掣圣 2 0 0 7 年5 月3 1 日 绪论 1 1研究背景 第一章绪论 计算机正在人类社会中扮演着前所未有的角色，从家用电器到核反应 堆控制系统。从医疗系统到航天飞机，越来越多的任务正在被移交给计算 机来完成。由此可以预见，由软件驱动的计算机芯片将会控制着人类生活 的各个领域。然而软件系统的日趋庞大与复杂也意味着计算机的使用将带 来巨大的风险。根据美国政府报告，每年由于软件错误导致的经济损失达 数百亿美元。而在诸多关键领域，例如核反应堆、火箭、飞机的控制系统 等等，计算机程序的半点闪失都将可能带来无法估量的惨痛损失。 计算机网络的兴起与应用使得程序可以同数据一样在网络上自由传 送。w e b 浏览器随时可以从互联网上下载运行软件；在一些移动计算平台 上，移动代码体( a g e n t ) 可以在网络上进行移动计算。此外，网格计算平台 也可以使大规模的计算任务通过移动代码的形式被分发到网络上的各个节 点进行计算。于是在计算机网络环境中，程序有可能在网络传输过程的任 何一个环节中遭到恶意修改，从而导致严重的安全问题。 1 1 1程序与安全 为了解决日趋严峻的程序安全问题，人们采用了多种方法来试图提高 程序的安全性，降低软件错误的发生率。程序测试是最常见的确保程序安 全性的方法，软件测试人员使用人工、计算机辅助或者两者相结合的方法 对程序进行大量的测试，期望通过寻找程序中导致安全性问题的错误( b u g ) 来保证程序的安全性。但是程序测试并不能十分有效地解决程序的安全性 问题。如果一个程序被发现了包含许多b u g ，并且及时修复b u g ，这并不意 味着程序安全的：首先，可能程序还有更多的潜在b u g ；其次是无法确认程 序因为修补这个b u g 的同时，是否会引入了更多的b u g 。重复的测试导致软 件系统的成本大幅度提升，而且程序测试方法难以对付规模大，结构复杂 l l r l 研究背景 的程序。 程序分析是另一种方法，分析人员利用辅助工具对程序进行静态分 析，如数据流分析、控制流分析等等，通过这些数据和控制流的走向来检 查程序是否安全可靠。静态程序分析通常可以找到程序员意识不到的b u g 。 但仍然无法保证个程序没有b u g 而且可以安全运行由于程序的语义复 杂。进行程序分析的算法无法理解程序的语义，通常会发生误报与漏报的 情况。因而程序分析可以作为程序员编写程序时的辅助工具或者作为寻 找b u g 的一种有效方法，但是也不能保证程序的安全性。 还有一种保证程序安全性的方法是监视运行程序的整个计算机系统， 一旦系统出现不安全的情况就采取定的恢复措施将系统从错误中恢复。 然而这种方法同样存在些问题：首先程序的监视器必须能够事先预料 到程序可能存在的错误或者可能出现的行为；其次监视器程序也是软件 系统，整个系统的安全性监视仍然依赖到监视器的正确性；通常程序的运 行环境非常复杂，程序状态集合庞大，监视器难以事先预科到各种出错情 况。 1 1 2形式化的程序验证 无论是程序测试、程序分析还是程序监视都不能有效解决程序的安全 性问题。对于关键程序而言，只要程序中存在一个b u g ，即使这个b u g ? d , 现 的概率很小，旦b u g 被触发也有可能带来灾难性的后果。程序测试、程序 分析与程序监视这些方法的共同特点是在不理解程序语义的基础上寻找程 序中隐藏的不安全因素，显而易见。这是非常困难的。如果要找到尽可能 多的b u g ，通常需要程序员能够完全理解程序语义。于是我们可以考虑首先 理解计算机程序的语义，然后在此理解的基础上去检查程序是否存在违反 语义的b u g 。 目前有很多表达程序语义和理解程序语义的方法，比如最常见的方法 是使用自然语言为程序添加注释。程序注释是对程序语义的一种描述， 注释有利于程序员开发、维护、调试程序。程序注释通常使用自然语言 编写，自然语言的语义模期性和二义性常常会带来对程序语义的模糊的甚 至是错误的描述。因此有许多形式化程序规范的研究【1 3 】，程序规范使 用形式化的语言编写，避免自然语言的二义性缺点。仅有程序的形式化规 范不是够的，程序对象是否真正满足了程序规范需要采用分析程序语义的 2 绪论 方法去验证。形式化验证是一种静态的程序行为检查，这种方法的优点是 不会增加程序动态运行的开销，所有的验证工作都在程序运行前进行。早 在2 0 世纪7 0 年代，就有多种使用形式化的方法去研究如何描述程序的语义 以及如何证明程序正确性的研究，比如指称语义【4 1 ，h o a r e 逻辑【5 ，6 1 等等。 形式化验证过程不可能完全由人工来完成。一方面程序员对程序的理 解并不可靠，而且不会持久，随着软件规模的增加，程序员更加难以理 解和把握庞大的软件系统行为。同时，形式化的验证过程也不可能完全 由计算机程序来自动完成，因为我们无法开发出一个可以理解所有程序的 程序。但是我们可以把尽可能多的工作交给计算机来自动完成，计算机无 法自动完成的验证工作再交由人工完成。传统的程序验证中产生的程序安 全性证明需要人工去检查，而n e c u l a 等人提出了将程序的安全性证明显式 得表达出来，使用计算机程序来检查证明的正确性，这就是所谓的机器可 检查的证明( m a c h i n e - c h e c k a b l ep r o o f ) 。程序的安全性证明是用某种形式化 语言编写，因此可以排除自然语言的不可靠性，作为程序安全性的证据。 将安全性证明与程序捆绑在一起就构成了携带证明的代码p r o o fc a r r y i n g c o d e ，p c c ) 7 t p c c 与传统的程序验证研究的区别在于：首先，安全性证明不在是写 在纸上，而是使用某种程序设计语言编写。换言之，p c c 中的安全性证明 也是某种形式的程序；其次，安全性证明并不需要完全手工构造。许多辅 助工具可以大大减轻这一构造过程；最终的安全性证明也许较为庞大，但 是可以通过简单的计算机程序进行安全性证明的检查，不需要人工干预。 随着数理逻辑理论与程序语言理论相关研究的发展。人们发现程序本 质上也是某种数学对象。而数学理论同样可以用程序的形式表示。从这个 角度，我们就可以将p c c 看作是由两种不同形式的程序部分构成，一部分 是程序，另一部分是程序的安全性证明。在类型化确i 算f 8 1 中，程序部分与 证明部分，这两种看似不同的概念可以被统一编码。这种统一性背后的原 理被称为c u r r y h o w a r d 同构原理f 9 1 。 在详细介绍p c c 之前，本文先介绍两个基础概念，信任计算基 础( t r u s t e dc o m p u t i n gb a s e ，t c b ) 与c u r r y - h o w a r d 同构原理。 1 1 3信任计算基础 世界上不存在绝对的安全，本文讨论任何系统的安全性，都要基于一 3 1 1 研究背景 个已经被( 无条件的) 信任的基础。例如上文所提及的软件系统安全是 建立在硬件正确性的基础之上的，硬件的安全性则是建立在硬件运行的 环境满足要求的基础上，如硬件环境的温度，湿度等。又如计算机网络 的安全性建立在单个主机运行的操作系统的安全性基础之上，程序源代码 的安全性建立在其语言编译器的正确性基础之上等等。一个完整的安全的 系统中我们必须信任的部分被称作信任计算基础( t r u s t e dc o m p u t i n gb a s e ， t c b ) 。如果整个系统都是t c b ，那么也就不需要进行安全检查。但是此时 我们不相信系统是安全的。只有当我们把复杂的部分都排除出t c b 之外， 我们才会相信系统比较安全。显而易见，如果一个软件系统的t c b 比另一 个系统小，那么我们可以相信前者的安全性更高。 1 1 4c u r r y - h o w a r d g 构原理 c u r r y 1 0 1 - 与h o w a r df l l 】分别发现了程序设计语言理论领域的类型化a 演算【4 ，8 ，1 2 - 与数理逻辑【1 3 1 的对应关系。这一发现将多年以来两个不相干 的研究领域联系在一起。下面是简单类型化a 演算与直觉主义一阶命题逻 辑之间的同构关系： 简单类型化a 演算直觉主义一阶命题逻辑 类型 p 一0 p q 2 ：p 存在一个项z ，其类型为p 项z 的规约过程 定型规则 逻辑命题 尸) q p 口 工为p 命题的证明项 尸命题是可证的 尸命题证明z 的化简过程 命题逻辑自然演绎规则 演算的强范式性( s t r o n gn o r m a l i z a t i o n ) 逻辑的一致性( c o n s i s t e n c y ) 简单类型化a 演算中任意类型项都可以被看作是直觉主义命题逻辑中的一 个命题，如函数类型p 一0 同构于命题逻辑中的蕴涵命题p ) q ，笛卡尔 积类型p t q 同构于命题逻辑中的paq 。此外，而任意一个命题的证明 都同构于类型化a 演算中的一个表达式p ，如果存在某个类型的项z ，则说 明p 所同构的逻辑命题是可证的。换个角度，任意一个命题逻辑中的证明 都可以用简单类型化a 演算的项表示， 4 绪论 随后，人们又发现了多态类型化a 演算同构于直觉主义二阶命题逻 辑 9 】带依赖类型的类型化a 演算同构于直觉主义一阶谓词逻辑：高阶类 型化a 演算同构于直觉主义高阶逻辑；带控制流操作的简单类型化a 演算对 应经典的一阶命题逻辑等等。越来越多的研究表明，类型化a 演算和逻辑 系统本质上是同一种数学实在。 a 演算既是一个逻辑系统，同时又是一个可以编码递归函数的计算模 型。c u r r y - h o w a r d 同构原理使得计算与推理两种看似不同的概念统一在了 一起。 1 2携带证明的代码( p c c ) 所谓p c c 就是将程序与其安全性证明打包在一起，安全性证明表达了 对程序语义的详细理解过程，运行程序的主机只需要检查一下证明正确与 否就可了解程序是否安全。这个证明检查过程可以由一个简单的计算机程 序来自动完成，而不需要人去理解证明细节。这种方法相当于将对计算机 程序的语义的理解转化成了严格的数学证明。 对于编写p c c 程序提供方，如何产生这些证明才是关键所在因为安 全性证明是对程序语义的理解过程，因此开发程序的程序员可以清晰地表 达出程序的语义，并给出形式化的理解过程，最终产生安全性证明。这种 方法并不一定会增加程序员的开发负担，因为这些安全性证明可以通过计 算机辅助、半自动的甚至是全自动的产生。程序员所要做的是为程序的语 义给出一些标注信息，或者为证明产生工具给出一些提示。然后通过计算 机程序来产生最终的安全性证明。 携带证明的代码( p c c ) 与普通的程序代码的关键区别在于程序必须携带 一个形式化的证明，这个证明用来证明程序满足安全性要求。这个证明从 何处来，如何表达、产生和检查这个证明? 本文下面介绍的p c c 框架将会 解答这些疑问。p c c 框架最早由g n e c u l 卿pl e e | 7 1 提出，之后p c c 框架 演变成一个一般性的概念。这个框架提供了一种安全机制：运行程序的主 机可以快速高效地检查程序是否满足安全策略。 下文介绍一个简单的但完整的p c c 框架，然后分别解释p c c 框架中的 概念。本节只对这些概念进行非形式化的描述，而这些概念的形式化定义 和框架的细节将是下一章的主要内容。此p c c 框架如下图所示： 5 1 2 携带证明的代码( p c c ) t c b 酗1 一l ：p c c 框架 所谓代码生产者是提供代码，或者产生代码的一方，代码生产者可以 是程序员，编译器，提供代码下载的网站，或者移动代码的发送者等等。 代码消费者是将要运行p c c 中可执行程序的主机系统，p c c 框架的目的是 为了保证主机系统不会受到恶意代码的破坏。保护主机的安全。p c c 框 架要求代码生产者必须提供一个p c c 实体，而不仅仅是可执行程序。每 一个p c c 实体由两部分组成：可执行程序与安全证明。本文后面把一 个p c c 实体称为”p c c 包”。 为了保护主机系统的安全性代码消费者必须提供一个安全策略，这 个安全策略是对可执行程序的约束，是对程序运行期行为的一个安全性限 制，比如安全策略可以是要求程序运行占用的内存不超过某个阈值可 以是要求程序不破坏系统的某些环境，或者是程序运行的行为满足一定的 规范等等。安全策略必须由形式化语言严格定义，安全策略语言可以是各 种形式的逻辑语言，比如阶逻辑语言，高阶逻辑语言等等。 代码生产者在提供一个可执行程序的同时，必须能够证明提供的可执 行程序能够满足代码消费者的安全策略，而且生产者必须将详细的证明附 加在可执行程序上，构造一个p c c 包。代码消费者得习 p c c 包之后可以 利用一个证明检查器来自动的检查证明。如果p c c 包能够通过检查器，那 么代码消费者就可以知道p c c 包中的可执行程序是可以安全运行的。 应该注意的是，可执行程序的安全不仅依赖证明的正确性，还依赖 此p c c 框架的t c b 。此框架的t c b 包括：1 ) 安全策略：2 ) 检查器；3 ) 6 运行代码的机器。安全策略必须能够正确定义安全性，否n p c c 包中的证 明就毫无意义。检查器必须能够正确工作如果检查器允许携带错误证 明的p c c 包通过，那么机器的安全也无法保证。最后一点是将要运行程序 的机器系统必须能够正常工作，保证硬件不出故障，操作系统足够安全等 等。除了t c b 之外的p c c 框架的其余部分，都不再需要被信任，包括代码 生产者、可执行程序以及安全证明。可以看出，p c c 框架的优势是极大的 缩小了代码消费者一方的系统安全性的t c b 。 p c c 框架的另一个优势之处是p c c 包可以作为移动代码在网络上传输 和执行，并且不需要依赖加密和认证等措施就可以防止p c c 包被恶意篡 改。在p c c 包中的程序部分与安全证明部分必须致。如果程序不变而同 时安全证明被恶意地篡改，错误的证明将会被代码消费者的检查器发现。 如果p c c 包的程序部分被篡改，而证明部分不变。那么原来的证明不是被 篡改过的程序的安全证明，同样不会通过检查器的检查。p c c 包的篡改者 如果篡改了程序部分，那么也必须相应地修改证明部分。以保证证明部分 始终是证明前一部分程序的安全证明。 1 3p c c n 关的研究 在p c c 的概念与p c c 框架f 7 ，1 4 1 被提出后，n e c u l a 等人开发了一个出 具证明的编译器( t o u c hs t o n e ) 【1 5 1 。t o u c hs t o n e 框架中使用一个类c 语 言( s a r e e ) 的编译器，它可以把添加过类型标注的c 语言源程序编译 成p c c 包。c o l b y 等人还设计了一个j a v a 语言的编译器s p e c i a ljf 1 6 1 ，同 样可以将j a v a 字节码编译成p c c 包。a p p e l 等人提出了一个更一般的p c c 框 架，基础p c c ( f o u n d a t i o n a lp c c ，f p c c ) 框架1 7 ，1 8 1 。f p c c 框架通过为 验证稚理系统建立语义模型的方法将t o u c hs t o n e 中的验证条件产生器排 除在t c b 之外，进一步减小了系统的t c b 。h a m i d 等人随后提出了f p c c 框 架f t a lf 1 9 1 ，f t a l 采用了基于语法的证明方法来证明验证推理系统的可 靠性，从而避免t a p p e l 等人的语义模型过于复杂的问题。k c r a r y 提出了 一个基础类型化汇编语言t a l t 2 0 ，2 1 1 ，可以作为f p c c 框架。l 和s h a o 将 基于类型规则的验证推理系统改为更一般的验证逻辑c a p 2 2 l 。他们 的f p c c 框架可以描述更复杂的安全策略，并可以证明程序的部分正确性。 p c c 框架研究的重点在于： 7 l3p c c 相关的研究 如何表达程序的语义标注： 如何表达程序满足安全策略的证明： 对于具体的程序，如何产生安全证明 如何检查证明。 本节将介绍这些已有p c c 框架的相关研究，并对比这些p c c 框架的差异。 1 3 1 t o u c hs t o n ep c c 框架 n e c u l a 和l e e 最早为操作系统设计了一个扩展。网络包过滤器f 1 4 1 。这 个程序由汇编语言编写，由于过滤器携带了安全证明，通过静态检查就 可以确保过滤器的安全性，不破坏宿主操作系统的运行。随后n e c u l a 正 式提出了p c c 与p c c 框架的概念7 1 。1 9 9 8 年，n e c u l a 和l e e 提出了出具证 明编译器的概念f 1 5 卜所谓出具证明编译器就是将使用类型安全的高级 语言编写的程序编译成p c c 。他们首先实现了一个编译器，将类型安全 的c 语言程序编译到带标注的d e ca l p h a 机器目标程序；随后c o l b y 等人实 现了一个j a v a 编译器s p e c i a ljf 1 6 1 ，s p e c i a lj 可以将j a v a 字节码编译到带标 注的x 8 6 机器目标程序。 此p c c 框架的描述见图1 2 。源程序经编译器编译产生汇编代码和一些 逻辑标注，然后汇编代码和标注通过验证条件产生器( v e r i f i c a t i o nc o n d i t i o n g e n e r a t o r ，v c g e n ) 之后产生验证条件( v e r i f i c a t i o nc o n d i t i o n ，v c ) ，验证 条件通过证明器之后产生验证条件为真的证明。当代码消费者得蛩 p c c 包 之后，首先将汇编代码与逻辑标注输入到验证条件产生器( v c g e n ) 中产生 验证条件，然后使用证明检查a ( e l f 类型检查器) 来检查p c c 携带的证明 是否是验证条件的证明。如果证明检查通过，则说明汇编程序是满足安全 策略的。 在这个p c c 框架中，p c c 包、庞大的编译器与源程序不需要被信任。 此框架的t c b 包括四部分：( 1 ) 安全策略，包括一个验证推理系统的公理与 规则和程序规范( s p e c i f i c a t i o n ) ；( 2 ) 验证条件产生器( v c g e n ) ：( 3 ) 证明检查 器；( 4 ) 运行程序的机器。 安全策略中的验证推理系统系统是一个受限的一阶谓词逻辑加上源语 言类型相关的规则和一些谓词声明。包括逻辑语言语法定义、逻辑公理 与逻辑推理规则。这个逻辑系统存在判定过程。即逻辑中的命题可以通过 一个自动定理证明器得到安全性证明。验证推理系统用来检验一个程序是 8 绪论 c b 陶1 2 ：n e c u l a 等人的p c c 框架 否良形( w e l l f o r m e d ) ，良形的程序满足安全性要求。此p c c 框架中的验证 推理系统是一个与源语言类型相关的逻辑系统。比如关于源语言的数组边 界安全，j a v a 语言中的对象、类、异常等等。关于类型的安全可以静态检 查，因此s p e c i a lj f i ；i 译器编译出的本地代码可以消除动态检查数组边界，以 及动态检查空指针引用的相关代码。但是由于验证逻辑本身的可靠性并没 有得到严格证明，因此验证逻辑本身必须在t c b 内部。 安全策略的另一部分是程序规范，程序规范是运行程序的机器对程序 的语义约束。规范的形式是验证推理系统中的命题，通常是一个前条件和 一个后条件。 验证条件产生器( v c g e n ) 用来产生验证条件( v c l 。当输入一个带逻辑 标注的汇编代码，v c g e n 返回个逻辑命题，此逻辑命题等价于汇编代码 在验证推理系统中的良形性判断。v c 产生器在此框架中扮演重要的角色。 代码生产者将带标注的程序与程序规范输入到验证条件产生器中产生v c ， 然后使用一个定理自动证明器来为这个验证条件为真的命题产生证明。代 码消费者也通过验证条件产生器得到验证条件后，使用证明检查器来检查 证明是否确实是验证条件的证明。v c g e n 是一个庞大的程序，它本身没有 9 1 3p c c 相关的研究 携带安全性证明，因此v c g e n 也在t c b 内部