（计算机应用技术专业论文）指令级安全策略语言的设计与实现.pdfVIP

中国f i 学技术大学硕士学位论文 摘要 摘要 随着互联网络的发展，移动代码的安全问题成为了计算机科学中一个富有 挑战性的问题。移动代码的形式有很多种，比如用户浏览网页时，主机执行的 插件程序；从互联网上下载的新的驱动程序或一个娱乐用的游戏程序等等。这 种代码的特点是代码来源复杂，代码的编写质量和执行后对主机的影响难于估 计。因此如何防止来自网络上的恶意代码对主机的破环就成为我们要解决的关 键问题。 以往的解决方法是实时检测、病毒签名、加解密等方法，这些方法的局限 在于只能阻止有限的已知恶意代码的破坏作用且缺乏灵活性。本文介绍了我们 从编程语言的角度为解决移动代码安全问题所做的研究工作，主要内容包括： 1 我们阐述了这种方法的基本原理：就是利用编译手段搜集到程序的类型、结构 等信息，在客户端对程序进行类型检查等基本安全检查。通过与传统的安全 检查方法进行比较，我们描述了这种方法的优缺点。 2 介绍了我们用于解决移动代码安全问题的综合模型。底层安全保证类型、控制 流和内存安全，中层安全对程序使用的资源数量进行限制，高层限制程序对 重要的资源的访问。我们介绍了每层的基本工作流程和技术路线。 3 详细描述了用于解决指令级安全问题的策略语言和实现技术：这种语言能够对 指令执行序列进行安全约束，可以描述所有e m 机制可以加强的安全属性， 也可以在扫描指令的同时进行统计工作。我们尝试用静态分析的方法对移动 代码的扩展安全属性进行检查，本文介绍了我们所使用的分析算法。 本课题得到国家自然科学基金项目( 6 0 1 7 3 0 4 9 ) 的资助。 ( 本文附录介绍了我攻读研究生期间在基于三维模型的人脸动画领域的研究工作) 生里! ：兰垫查奎兰堡主兰堡堡壅 塑墨 一 a b s t r a c t f o l l o w i n gt h ed e v e l o p m e n t o f i n t e r n e t ，s e c u r i t yo f m o b i l ec o d ei sam a j o ri s s u e i nt o d a y sc o m p u t e rs c i e n c e t h e r ea r em a n yd i f f e r e n tf o r m so f m o b i l ec o d e ，s u c ha s p l u g i nc o d et h a tt h eh o s te x e c u t e sw h e n u s e re x p l o r e st h ew e b s i t e ；ad r i v e rp r o g r a m o ras m a l lc o m p u t e rg a m ed o w n l o a d e df r o mi n t e r a c t m o b i l ec o d e sc o m ef r o m c o m p l e xs o u r c e s ，s ow ec a nn o tk n o wt h ec o d e sq u a l i t ya n dt h ee f f e c t a f t e ri ti s e x e c u t e d h o wt op r e v e n tm a l i c i o u sm o b i l ec o d ef r o mh a r m i n gh o s t i n gn o d e si st h e p r o b l e m t h a tw e t r yt oa n s w e r 7 f r a d i t i o n a l a p p r o a c h e s t ot h e s e c u r i t yp r o b l e mi n c l u d ek e r n e l a sr e f e r e n c e m o n f l o r ，i d e n t i t yc o d eo fv i r u s ，c r y p t o g r a p h ya n ds oo n ，t h e s em e t h o d sc a no n l y p r e v e n tw e l l k n o w n m a l i c i o u sc o d ea n do f f e raf i x e ds e to fb a s i cs a f e t yp o l i c i e sw i t h l i t t l e f l e x i b i l i t y i nt h i st h e s i s ，w ei n t r o d u c eo i l r e s e a r c hw o r k i ti n c l u d e st h e f o l l o w i n ga s p e c t s ： 1 d e s c r i b i n gt h ep r i n c i p l eo f p r o t e c t i n gs e c u r i t yo f h o s tm a c h i n e b a s e do n t e c h n i q u e s o f p r o g r a m m i n gl a n g u a g et h e o r ya n di m p l e m e n t a t i o na n ds h o w i n g t h em e r i t sa n d d r a w b a c k so f t h i sm e t h o d c o n t r a s t i n gt ot r a d i t i o n a lo n e s 2 i n t r o d u c i n go u rs e c u r i t ym o d e lt op r o t e c th o s t i n gn o d e s ，i ti n c l u d e st h r e el a y e r s ， t h e r ew ed i s c u s se a c h l a y e r ss a f e t ya i m ，w o r k f l o wa n d i m p l e m e n t a t i o n t e c h n o l o g i e s 3 d e m o n s t r a t i n gm i d d l e - l a y e rs e c u r i t yp o l i c y l a n g u a g e a n d i m p l e m e n t a t i o n a r i t h m e t i c ：t h i sl a n g u a g ec a nr e s t r i c ti n s t r u c t i o nf l o wa n de x p r e s sa n yp o l i c yt h a t e mm e c h a n i s mc a n e n f o r c e ，i na d d i t i o n s ，i th a sc a nc o l l e c ts t a t i s t i c sw h e n w es c a n c o d e s w et r yt oc h e c km a c h i n ec o d eu s i n gs t a t i ca n a l y s i si m p l e m e n t t h e r ei so u r a n a l y s i sa r i t h m e t i c t h i sr e s e a r c hp r o j e c ti ss u p p o r t e db yn a t i o n a ln a t u r a ls c i e n c ef o u n d a t i o n ( 6 0 1 7 3 0 4 9 ) t h ea p p e n d i xi n t r o d u c e sm yr e s e a r c hw o r ko ft h r e e - d i m e n s i o n a lm o d e l - b a s e df a c i a l a n i m a t i o nw h e nip u r s u e m y m a s t e rd e g r e e 中国科学技术大学硕士学位论文 第一章绪论 1 1 研究背景和意义 第一章绪论 随着因特网的迅猛发展，软件的丌发和使用出现了两种新的趋势。其一是 动态扩展( d y n a m i ce x t e n s i b i l i t y ) ，即用户通过从网上下载和执行移动代码 ( m o b i l ec o d e ) 来扩充主机功能，如浏览器的一个插件程序，新的打印驱动程序等。 其二是基于组件的软件开发( c o m p o n e n t sb a s e ds o f t w a r ed e v e l o p m e n t ) ，通过这 种方法若干组件( c o m p o n e n t s ) 分别由多个软件开发商编写，再组成一个复杂 的应用软件，这样可以提高软件的复用性( r e u s a b i l i t y ) 和生产率。这些趋势给用户 和软件开发商带来了方便，同时也提出了重要的安全问题：这样的移动代码一异 地编写，主机执行一是否可信，它会不会破坏主机的数据，访问未授权的资源， 最终造成主机崩溃，重要数据丢失? 当此代码是恶意代码时如何防止它的破坏 作用? 回答和解决移动代码的安全问题越来越成为计算机科学要面对的挑战之 。 以往的解决这些问题的方法是实时检测、病毒签名、加解密等方法，这些 方法的局限在于只能阻止有限的已知恶意代码的破坏且缺乏灵活性，本文致力 于研究一些新的的安全检查方法，它们使用基于编程语言的理论和实现技术， 通过分析程序语义、类型和系统调用等特征，对程序进行检查。这些方法突破 了传统方法只检查程序的外部特征的局限，是传统安全解决方法的有力补充， 可以用来增强网络主机的安全性。 本章将先引入一些有关移动代码安全的基本概念，然后通过比较传统方法 和基于语言的安全检查方法来介绍目前这个领域的研究现状。 中国利学技术大学硕士学位论文 第一章绪论 1 2 移动代码安全概述 1 2 1 移动代码及其特点 移动代码是指可以在网络中迁移执行的代码段或程序。它与其他程序相比 有一些特点： 1 用户下载这样的程序有明确的目的性。如一个娱乐用的小游戏，一个f l a s h 动画陧序，一个更新的打印驱动程序等。这个特点规定了代码的一般行为集合， 如果分析程序代码能确定程序的反常行为，就可以阻止它的破坏行为。比如我 曾经搜集到一个恶意程序的版本，它外表是经典的俄罗斯方块的游戏，实际上 在执行过程中搜集主机的系统文件，并将它们移动到隐蔽的文件夹中。它如果 删除这些文件，或向其他主机散布个人信息，其破坏力就不只是如此了。 2 移动代码通常比较短小。限于网络的速度和代码的应用，移动代码规模较小， 这就为在有限时间内分析代码的某些语义特征来确定其安全性提供了可能。 3 移动代码的来源复杂。传统的反病毒技术如特征代码法不能对如此庞大的样 本程序做一一鉴定。未知恶意代码层出不穷，要求有更好的安全机制。 1 2 2 移动代码的安全 理想的移动代码是一种具有智能的可执行代码，它具有跨地址空间持续运 行的能力，可以在网络中自主迁移到不同主机上去执行代码的不同部分。移动 代码的安全包括两个方面：( 1 ) 从代码的角度看，当它在网络中不同主机上持 续执行时，它会在不同主机之间进行传输，因此它需要防止恶意主机对自己的 修改，以免恶意主机利用它对网络中别的主机进行攻击；( 2 ) 从主机的角度看， 当移动代码迁移到本地时，如何保证它的执行不会破坏主机的系统数据。本文 讨论的移动代码安全是指其第二个方面。 那么什么样的移动代码是安全的呢? 如何保证其安全性? 我们在总结前人 的工作和分析典型的恶意代码之后认为，满足基本的安全性质和主机扩展安全 策略的移动代码是相对安全。 基本安全性质包括1 。控制流安全：程序的跳转指令和调用指令所指向的地 中国干 学技术人学硕士学位论文 第一章绪论 址，必须是在程序代码段的地址之中，而不能跳到别的位置上。所有的调用都 应指向合法的函数入口并且所有的返回地址是合法的。2 。内存安全：程序只能 访问其静态数据区范围内的数据，或者是系统分配给它的堆中的数据，或者是 合法的栈帧上的数据，而不能随意访问内存中的其它位置；3 。栈安全。对于基 于栈式分配的语言实现，运行时栈应该在函数调用的过程中被保存下来。这三 个基本的安全性质是相互独立的。 为了保证主机安全，扩展的安全规定还应包括c p u 的有限利用，移动代码 不能随意读写关键文件以及来自不受信任的网站的程序不能任意访问外部设 备，如打印机，网络端口等。从实践中抽象出来的安全规则较为复杂，我们可 以将这些安全规则用某种安全语言描述出来，用来指导对移动代码的安全检查。 f 第三蕈1 1 3 研究现状 传统的解决移动安全问题的方法包括特征代码检查、内核监督、代码检测 以及加解密技术。这些方法按照固定的安全策略对移动代码进行检查，因而缺 乏灵活性。以安全自动机( s e c u r i t ya u t o m a t a ) 和p c c ( p r o o f - c a r r y i n gc o d e ) 为 代表的一些基于语言的安全检查方法提供了灵活解决移动代码多方面安全需求 的通用框架。t a l ( t y p e da s s e m b l yl a n g u a g e ) 和e c c ( e f f i c i e n t c o d ec e r t i f i c a t i o n ) 也属二f 这种方法。 1 3 1 传统方法的局限 特征代码检查法需要事先采集恶意移动代码的样本，抽取特征代码组成病 毒库，然后在被检测可执行文件中搜索恶意程序的特征代码，从而保证该程序 不会对主机进行危害。这种方法的优点是准确、快速且误报率低，但是它不能 检测未知的恶意代码。 内核监督把重要的系统组件和关键的数据放在系统内核中。外部进程通过 内核提供的接口以有限的方式访问这些数据。这种方法允许用户阻止移动代码 对系统的破坏，而且还可以监视所有的数据访问、完成验证以及加强其它的安 全策略等。这种方法的缺点是非内核进程不能直接访问关键的系统组件和数据， 中国科学技术大学硕士学位论文 第一童绪论 从而影响了性能的提高，内核调用过程中，上下文切换的时间开销很大。人们 更希望让所有的非内核进程能安全的直接访问关键数据。 代码检测是指通过修改或加强机器码艘关键操作可以在执行时被监视。它 使用如下策略：若代码行为与预期的行为一致，则代码可以安全执行，否则让系 统截获控制权并终止该错误进程，或者阻止其产生不良后果。代码检测的优点 是，接收方可以在不对代码做任何假设以及无需有关代码的任何附加信息的情 况下，独立地执行代码检测。缺点是在每个敏感操作之前都必须执行运行时检 查，会使得运行时开销过大。 加解密方法保证了数据在网络中传输时不会被修改和泄密。但是它并不能 保证来自一个不被信任的代码生产者的移动代码对主机是安全的。 1 3 2 基于语言的安全检测方法 s c h n e i d e r 将基于语言的安全检查方法定义为基于编程语言的理论和实现 技术来解决安全问题的一组方法，可以利用的检查手段包括语义、类型、优化 和验证等。p c c ，t a l ，e c c 等方法是这样的一组方法的代表。它们的基本想法如 下： 编译器在编译高级语言的过程中收集许多关于程序的信息，比如变量的类 型信息或变量值的界限，还有结构信息、命名信息等等。这些信息通过某种方 法保留下来与编译后的指令序列一起移动到代码的接受方，代码接收方可以利 用这些信息来判定移动代码是否满足主机既定的安全策略。 f 图1 1 】显示了基于上述想法的一个典型的工作流图。代码发送方编译高级 语言的过程中对源代码收集上述的额外信息，这些信息，称之为”证书”，附属 在目标代码之中。接受方在得到代码的同时也得到这些附加的信息。他运行一 个验证器检查代码和证书，验证代码是否符合某种主机安全策略。若验证成功， 那么代码可安全执行。在这里，除了验证器是接收方可信任的组件外，编译器、 目标代码以及证书均可以不是，这样有效的缩小了信任基。这种方法最大好处 是将创建正确性证明的任务留给了代码生产方，接受方的任务只是验证证明过 程是否正确，工作量极大降低。 证书可以采用不同的形式。例如，p c c 的证书是验证条件的一阶逻辑证明， 中国科学技术大学硕士学位论文 第一章绪论 其验证过程是检查该证书是否为有效的一阶证明；t a l 的证书是类型注解，验 证过程是类型检查。虽然各种方法在表达能力、有效性和灵活性上有差别，但 它们有共同的目标：利用编译时产生的额外信息来帮助解决移动代码的安全问 题。以下较为详细的介绍p c c ，t a l ，e c c 等方法，它们在解决类型安全等基本 安全的问题上取得了好的结果。 1 3 2 1 携带证明的代码( p r o o f - c a r r y i n gc o d e ) 携带证明的代码 文献l 一9 】允许安全特性的证明在代码运行之前产生和验 证。这种方法包括两个关键的步骤，即代码发送方产生证据，代码接受方验证 在p c c 检查机制中，代码发送方先产生一个带有注解的目标代码并发送给 接收方，注解包括循环不变式和函数的前后条件等。接受方根据已有的安全策 略和接收到的注解代码产生验证条件并发还给发送方。验证条件是一系列的一 阶逻辑公式。发送方用个定理证明器，产生关于该程序是安全的形式证明， 再把该证明发送给接收方。接受方运行证明检查器，验证该证明是有效的。 在一个实际的p c c 实现中，最初的注解是由验证编译器产生的。这个编译 器通过对源程序的分析得到循环不变式和函数的前后条件。这里函数的前条件 应该提供足够的信息使得下一阶段可以为该函数提供产生验证条件。验证条件 中国科学技术大学硕士学位论文 第一章绪论 保证函数满足安全策略并且满足其后条件。p c c 使用t o u c h s t o n e 编译器 3 作为 验证编译器，它实现了一个类型安全的c 语言的子集。t o u c h s t o n e 的主要优点 是实现了许多代码的优化技术，如死代码删除、公共子表达式删除、复写传播、 指令调度、寄存器分配、循环不变计算外提、冗余代码删除以及数组越界检查 的删除等等。 下一步，代码的接受方根据目标代码和证书产生验证条件，g e o r g ecn e c u l a 和p e t e rl e e 【1 提出使用一阶逻辑规范来表达安全策略。在他们的系统中接收方 扫描待验证代码的每一条指令来产生一阶逻辑的谓词作为验证条件，并且还提 供一些证明公理给发送方。该谓词随后由发送方利用给定的定理证明器和接收 方提供的公理给出该谓词的证明，然后将证明发回给接收方。证明的过程是独 立的。目前，e d i n b u r g 逻辑框架( 简称l f ) 1 0 被用做表示验证条件及其证明的 语言。l f 是一种元语言，用作高级的逻辑规范，本质上它是一种类型化九演算， 它把证明表示成表达式，把谓词表示为类型。使用l f 的一个优点是可以使用 l f 的类型检查机制，通过检查表达式的类型来验证证明是否正确。t o u c h s t o n e 采用l f 来表示证明，它扩展了n e l s o n 和o p p e n 提出的组合判定过程 1 1 的方 法来实现定理证明器，增加了处理相等性的同余闭包判定过程和处理线性计算 的s i m p l e x 判定过程【7 。最后的验证可以利用l f 的类型检查机制，这种机制 通常只需要一到二百行程序就可以解决问题，这得益于l f 类型系统的简单。 p c c 的优点是它的表达能力和处理代码优化的能力。原则上，可以产生验 证条件并可以用一阶逻辑证明的安全策略就可以用这种方法加以检查。p c c 的 另一个优点是，如果代码、证明或验证条件在传输过程中被恶意改动或由于网 络故障而丢失部分数据，也不会影响代码的安全执行。因为，接收方只根据自 己产生的验证条件和发送方发来的证明进行验证，以判断代码是否满足安全策 略。如果代码改动导致不满足安全策略的话，则拒绝执行；如果仍满足，则说 明相应改动并未破坏安全策略，仍然可安全执行，只是代码的语义与原来的可 能不一样。缺点是安全策略的证明可能很大，如果证明太长的话，验证时间相 应地加长这是难以接受的。 p c c 使得移动代码安全的责任从接收方转移到了发送方。接收方只需做少 量工作即可认定移动代码是否安全，这有利于那些内部资源不很充足的便携式 中国科学技术大学i 蕊l 学位论文 第一蕈绪论 殴备下载代码。 1 3 2 2 类型化的汇编语言( t y p e da s s e m b l yl a n g u a g e ) 类型化的汇编语言方法( t a l ) 是一种基于语言的系统，在编译强类型高级 语言的过程中，类型信息先被转化为平台无关的类型化中间语言( t i l ) ，最后 附在目标代码之中。产生一种可以被类型检查器检查的带类型注解的目标代码。 人们可以把1 a l 看成是一种特殊的携带证明的代码。这里完整的类型注解是类 型安全的证据，类型检查器就是具体的证明检查器。 t a l 的理想目标 1 2 是提供种低级的、静态的类型化目标语言，使之比 j a v a 字节码更加适合于支持众多的源语言以及大量的优化。 最初的t a l 版本是通过对一种类m l 的多态类型抽象语言进行一系列变换 而得刮的结果 1 0 ，这些变换被称为保类型变换，最终形成的t a l 是基于传统 的r i s c 汇编语言。t a l 的静态类型系统加强了高级的语言抽象，例如闭包、 元组以及用户自定义的抽象数据类型等。t a l 的类型系统保证类型正确的程序 不会违反这些抽象。而且，t a l 的类型系统不会阻碍如寄存器分配，指令选取 和指令调度之类的低级优化。 早期t a l 版本的变换中包括了后续传递语义( c p s ) 变换，c p s 使用堆分配 的活z 力记录取代栈分配的活动记录。堆分配与传统的栈分配的实现相比有不少 优点 1 4 ：易于实现一些控制原语如异常，一阶后续 1 5 等；a p p e l 和邵中 1 6 指出堆分配可以节省空间，因为它更容易共享环境；堆分配有统一的内存管理 机制( 垃圾回收) 来分配和释放各种对象，包括活动记录。但是有两个重要的 因素使得提供对栈的支持很有必要 1 4 1 ：基于栈的活动记录所占用空间比基于 堆的活动记录要小；许多芯片的体系结构设计要求应用程序使用基于栈的方法， 例如，奔腾p r o 芯片内部有一个用来预测过程返回地址的内部栈 1 7 1 ，它来源于 使用标准控制栈的调用返回原语。因此，t a l 的后续版本添加了栈，它的文法 请参见 1 4 1 。 n e a lg l e w 和g r e g m o r f i s e t t 1 5 指, “d , 将t a l 扩展成m t a l ( m o d u l at a l ) ，并 在每个目标文件的开始处添加引入和导出接口，使得连接时的类型检查与目标 文件自身的类型检查分离开来，如果检查得出各个文件的接口是良类型的，则 中国科学技术大学硕士学位论文 第一章绪论 可以保证目标代码在连接时的良类型性质。 如果不采取任何优化手段的话，t a l 中类型注解的大小超过实际执行代码 的大小，这使得t a l 还不能适合大规模工业应用。d a ng r o s s m a n 和g r e g m o r r i s e t t 1 9 提出使用b a k e i ti n 方法，“不优化”方法，以及重构和压缩算法等， 可以得出相当精简的注解，最后形成的注解大小大约为代码总量的1 0 。 目前，1 a l 已实现的版本叫做t a l x 8 6 软件包 1 2 】。它定义了类似于c 的 高级语言p o p c o r n 。t a l 还不完善，还需要进一步的扩展。目前t a l 类型系统 的一个重要缺点是，不能有效地释放内存对象，而是依靠一个垃圾回收程序来 回收对象，从而阻止了对内存的及时重用，而这种重用在类型化低级语言中是 很关键的。f r e d e r i c ks m i t h 和d a v i d w a l k e r 2 0 提出使用指针别名的方法，将指 向内存位置的指针也作为一种类型加入类型系统，可以保证在释放内存对象时 不会破坏t a l 代码的良类型性质。这样需要对现有的类型系统做很大的变动， 因此目前还没真正使用这一扩展。其他处于研究之中的对t a l 的扩展还包括， 删除数组越界检查 2 1 1 和运行时的代码生成f 2 2 。 t a l 没有p c c 表达能力强。t a l 可以处理所有可用类型系统的表达的安 全策略，包括了内存安全，栈安全和控制流安全等基本安全策略。并且，t a l 在面对编译优化时非常健壮，因为它的类型注解是与代码一起变换的。 最后，d a ng r o s s m a n 和g r e gm o h i s e t t 【1 9 证明了t a l 是完全适合于大规模 工业应用的。 1 3 2 3 j a v a 虚拟机语言 j a v a 语言是基于语言的安全方法的一个成功的实例。人们用j a v a 编制程序 时，j a v a 编译器产生平台无关的字节码，它在执行之前由接收方检验其安全性， 然后j a v a 虚拟机解释执行字节码，或者字节码被进一步编译成本地的机器指令 来执行。 在j a v a 的安全运行环境中包括一个字节码检验器，用来保证代码的内存安 全、控制流安全和类型安全。它还包括一个安全管理器，用来加强一些高层的 安全策略，如限制a p p l e t 对磁盘i 0 的访问。这些概念与类型检查合并在一起， 组成了有效的“沙箱”模型，限制j a v a 代码在没有用户明确同意的情况下不能 中国科学技术大学硕士学位论文第一章绪论 执行敏感操作。j a v a 也实现了代码的签名安全。用户可以根据对签名的信任来 决定是否执行该程序。安全机制在实际应用中被证明是安全的，一些j a v a 安全 被突破的实例主要是因为在实现中没有坚持设计原则的缘故。另外一些安全漏 洞被认为是因为j a v a 缺乏一个足够完备的语义模型，j a v a 并没有形式规范，它 的规范只是非形式的描述。在这方面，和j o h nc m i t c h e l l 和s t e p h e nn f r e u n d 2 3 2 4 提出了一种比较完善的j a v a 类型系统，包括了j a v a 字节码语言 的大部分，有类、接口、方法，构造函数、异常以及字节码子例程等，为开发 字节码语言以及j a v a 虚拟机验证器的形式规范奠定了基础。 1 3 2 4e f f i c i e n tc o d e c e r t i f i c a t i o n ( e c c ) d e x t o rk o z e n 2 5 提出一种有效代码验证( e c c ) 的方法，它用于保证从网络 中下载的次性应用的小程序的执行安全。它给代码添加的注解主要是代码的 基本结构信息和类型信息。这些信息能够在一定程度上保证代码的基本安全。 e c c 在本地代码上迸行安全操作，减少了j a v a 解释执行的实时代价。 e c c 工作时，利用编译器在编译源代码的同时产生代码的结构注释。这在 编译上下文无关程序设计语言时是可以做到。比如一个c a l l 结构块包含一个函 数的结构体，而一个计算块则包含了计算表达式值的语句。e c c 对程序进行抽 象后，得到了一个结构注释和残余代码的组合体。残余代码是不能归于任何既 定结构的支离指令。在检查基本安全时，该方法借助于编译时搜集的结构信息， 对些既定的安全规定进行检查来保证基本安全。比如规定通常控制流指令( 条 件转移或无条件转移，c a l l 或r e t u r n 指令) 不可以穿越块结构的边界。在残余代 码中p u s h 和p o p 指令应该成对出现且p u s h 指令永远在p o p 指令之前执行等。 e c c 的注解易于产生，易于验证，并且它在目标代码级进行操作，因此效 率较高。其缺点是依赖于平台和依赖于编译器的实现。 1 3 2 5 其他研究 基于语言的方法能够用于互不信任的机器之间传递控制信息流。这里，安 全策略是基于信息流模型的 2 6 1 。用户在高级语言中增加注解来限制信息在程 序内和程序闯流动。加注解的程序在编译时被检查，保证程序遵循流规则。目 中国科学技术大学硕士学位论文第一蘑绪论 前已经有一个原型实现j f l o w ，它给j a v a 增加了流原语。j f l o w 是一个源语言到 源语言的翻译器，它使用类型检查机制来检查信息流安全，然后丢弃注解，还 原为普通的j a v a 程序。如果这些控制信息传递到目标代码，则可以用与t a l 和e c c 类似的方法进行验证。 f l i n t 项目 2 7 2 8 】致力于为高阶的类型化语言构造一个通用的编译器架 构。他们希望使用一个类型富有的类型化中间语言，作为编译其它语言的目标 语言。目前，f l i n t 已经作为s m l n j 2 9 1 编译器的中间语言而广泛使用。 s c h e i d e r 对传统的代码检测的方法进行了扩展，提出“安全自动机”的概念 2 4 。可以处理所有由有限自动机表示的安全策略。代码检测使得任何可能影 响安全自动机状态的指令都必须在对该自动机调用之后执行。安全自动机使安 全策略的规范变得很灵活，并且允许按照代码接收方的特定需要来构造安全策 略。它的主要缺点是在运行时对自动机的模拟存在一定的开销。 1 4 本章总结 移动代码的安全是计算机安全领域面临的主要问题。本章介绍了一些基于 语言的特殊方法。这些方法大多数都是在编译高级语言时获得安全信息，并把 它们附在目标代码中。这些信息以形式化的证明、类型注解或其他的注解信息 存在。它们随目标代码一起被下载，并在代码运行之前自动被检查器验证。在 这些方法中，基本安全策略得以保证，比如内存安全、控制流安全、栈安全等。 仅仅检查器( v e r i f i e r ) 是必须被用户信任的，编译器、代码、证书是不必被信 任的。j a v a 的字节码验证就是这种方法的一个实例。本文以下将介绍项目组提 出的解决移动代码安全的三层安全结构，并分别详细介绍每层的基本原理和关 键技术，最后是结论和进一步的工作。 我的工作是通过搜集、分析恶意代码的实例，总结出移动代码的特点，需 要加强的扩展安全策略的内容。 中困干 学投术火学硕士学位论文第二章三甚安全榆奁结构 2 1 引言 第二章三层安全检查结构 一个安全的移动代码至少应该满足 12 1 】小节中所提到基本安全策略。以 p c c 和t a l 为代表的基于语言的技术较好的解决了移动代码的基本安全，如类 型安全、控制流安全和栈安全。但是在调研网络主机受侵犯的实例中，我们感 觉到单一的安全机制难以保证移动代码多方面的安全要求。主机用户往往在实 际操作中要求对代码进行更高级的约束。比如限制代码的执行时间、使用的空 间，限制代码对网络端口、敏感文件的进行读写等等。为了满足移动代码多层 次上的安全要求，我们认为应该采取多种检查方法对移动代码进行检查并提出 了一个综合的安全模型。 以下介绍了我们的三层安全模型，我的工作是参与制定三层安全模型的工 作，提出了有关底层类型安全检查机制和高层安全保护机制的若干设想，设计 并实现了中层安全策略语言。 2 2 可供选择的检查方法 移动代码的安全检查主要包括三种方法：静态、动态和混合检查。 静态检查方法是指在不实际执行移动代码的情况下，利用编译、静态分折 等手段尽可能多的确定有关代码的信息，然后利用这些信息对代码进行安全约 束。这个过程是在代码执行前就已经完成，因此它不产生运行的时间开销。与 动态约束相比，未通过检查的程序不会产生难以消除的运行结果。但是，即使 最复杂的静态分析也不能完全确定程序的运行时状态，恶意程序的误报和漏报 是难于避免的。p c c 和t a l 都应该属于这种方法。 动态检查在程序运行时对程序的行为进行约束。较为典型的是内核检测。 程序在运行时会请求代理程序访问关键的文件和数据，内核可以在此时对代码 进行检查。这种方法会产生运行时的时间开销，且能检测的安全特性依赖于具 体的实现机制。s f i 方法【3 0 和s c h n e i d e r 3l 】所提出的安全自动机都可以用这种 中国 学技术大学硕士学位论文 第二章三层安全检查结构 方法实现。但是s c h n e i d e r 在他的报告中也指出这种方法只能加强能用e m 2 检查的安全策略。 混合检查则是将静态检查与动态技术结合起来代码进行检查。实践中，j a v a 的沙箱模型，m e s a 和m o d u l a 等语言中都采用混合检查方法来保证代码的安全， 这是由需要保障的安全特性的多样性决定的。我们下面介绍的三层体系结构也 遵循这样的混合检查方法。 2 3 解决移动代码安全问题的一个综合模型 我们项目组提出了一个移动代码检查的综合体系结构 图2 1 】。 在这个综合的模型中，代码的生产者协助代码的接受者对代码进行安全检 查。首先要求代码的生产者和使用者遵循一组共同的基本安全策略如类型安全。 然后移动代码的源程序经过认证编译器编译，生成携带注解的代码。注解包括 在编译过程中得到的类型信息、代码的结构信息和循环不变信息等。代码先经 过代码生产者的安全检查，即安全检查器在注解的基础上，按照一组基本安全 中国科学技术大学硕士学位论文 第二章三层安全检查结构 策略对该代码进行推理检查。然后把代码连同检查过程中的用到的推理提示发 送给代码接收方。在代码接收方对代码进行三层检查，它们是： ( 1 ) 低级代码安全检查。由于代码的接受者与生产者共有相同的基本安全策略， 这个层次检查的任务是借助代码生产者提供的注解和推理提示验证代码满足一 些基本安全，如控制流安全、内存安全、类型安全等。代码接收方和发送方低 级安全策略组件的功能基本相同，所不同的是代码产生方的安全策略组件要完 成基本安全策略推理的全过程，如匹配规则、回朔、子目标的证明等，而代码 接受方只要借助发送方证明过程的提示( h i n t s ) ，再完整的验证一次推理过程 即可，因此省去了寻找证据的时间。 ( 2 ) 中级代码安全检查。中级安全策略在指令级解决解决资源消耗问题，如限制 代码执行指令数、限制代码所能使用的堆栈空间等。 ( 3 )高级代码安全，则是采用动态检查方法来截获代码运行的系统调用，达到 保护主机资源的目的。 中级和高级的安全要求是复杂的，而且具体内容随主机用户的需要而变化。 如果我们将安全策略编码到安全分析程序中，其改变和维护工作都是很困难的。 提供通用的安全语言来描述安全策略，将其与安全分析程序的实现分离是一种 理想的解决方法。 2 4 低级代码安全 低级代码安全解决最基本的安全策略，我们这里把筒合类型安全的代码看 作是符合低级安全的代码。在系统的这个部分，我们可以使用各种已有的架构， 如p c c 和t a l 模式。在我们的实践中，采用的是p c c 架构。我们用一阶逻辑 描述基本的安全策略，用一阶逻辑的谓词构造器来构造安全策略的谓词，用推 理规则来描述谓词的证明过程，并且使用e d i n b u r g h 逻辑框架 3 2 ( e d i n g b u r g h l o g i c a lf r a m e w o r k ，e l f ) 来对接收到的目标代码做类型检查和验证。当然，我们 要求该目标代码必须包含了用一阶逻辑描述的验证条件和相应的证明过程。 2 4 1 基本安全策略 基本安全策略用一阶逻辑描述。 图2 2 】中给出了一个例子，描述了仅具有 - 1 3 一 中国科学技术大学硕士学位论文 第二章三层安全检查结构 指针类型，整型，布尔型，数组类型的语言的一个简单的类型安全策略。第一 部分给出了一些谓词构造器。“t y p eet ”判定某个表达式的类型为t ：“a r r a y t ”指明元素类型为t 的数组类型；“p t r t ”表示指向t 类型的指针；“a s i z e a l e n ”指明数组a 的元素个数为l e n 个：“s a f e r das i z e ”和“s a f e w ra s i z e ” 表示可以安全读写地址a 处的s i z e 个字节；“u p dm evs i z e ”，表示把内存m 中地址e 处的值改为v ，v 占s i z e 个字节：“s e lmes i z e ”指从内存m 中的地 址e 处读s i z e 个字节；“s i z et n u m ”描述类型t 的值的大小为n u m 字节；“乙t e le 2 ”，“u l te 1e 2 ”，“e qe 1e 2 ”，“n e qe 1e 2 ”，“g ee 1e 2 ”，“u g ee 1e 2 ” 描述布尔表达式，分别为e 1 符号大于e 2 ，e 1 无符号大于e 2 ，e 1 等于e 2 ，e 1 不等于e 2 ，e 1 符号大于等于e 2 ，e 1 无符号大于e 2 ：这些谓词构造器，可以 用来定义基本的类型安全策略。 第二部分给出了一些推理规则，用来证明由第部分定义的谓词构造器所 构成的谓词。这里只给出了一部分推理规则。规则l 描述了具体的各种类型应 该占据几个字节，这里我们考虑整型占4 个字节，布尔型变量占1 个字节，指 针类型4 个字节；规则2 是说，如果某个地址a 中值类型为指向类型t 的指针， 那么对于该地址中的值所表示的地址，其值的类型为t ；规则3 用来判定数组 元素的类型，如果a 为t 类型的数组，且a 有l e n 个元素，类型t 的大小为b ， 而且偏移o f f 小于数组元素个数，那么地址a + o f f * b 处的值的类型为t ；规则 4 是说，如果两个表达式的类型均为t ，则对它们做算术运算得到的值的类型为 t ，t 可以是整型，布尔型，甚至指针类型：规则5 是说，在算术运算中，如果 有一个表达式类型为整型，则结果也为整型；规则6 描述了安全读数组中某个 元素的判定规则，如果a 为t 类型的数组，元索个数为l e n ，t 类型占b 字节， 且下标o f f 不超过l e n ，则可以安全的读地址a + o f f * b 处的b 个字节；规则7 描述了最简单的内存读写的安全规则，地址a d d r 处的值类型为t ，且地址小于 某个上限，大于某个下限，类型t 占b 个字节，则允许对a d d r 处的b 个字节 进行读写，这里的上下限制是机器的最大虚拟内存，3 2 位机器通常是o _ _ 2 3 l 。 综上所述，我们给出了一个非常简单的基本安全策略的描述。它保证 了读写数组元素的安全，保证了算术表达式的类型安全，以及读写内存时必须 按照地址的类型来读写相应的字节数。例如，如果某个地址a 的值类型为整型， 生璺盟兰堡查查兰堡主堂垡堡壅箜三兰三星兰兰垄星堕i ! l 则一次读出4 个字节是安全，只读一个或两个字节被认为是违反安全策略( 规则 7 汞18 1 ：还有，如果两个布尔型的变量相加，如果代理程序在其中施加了强制 类型转换，转换成整型，则它将不能通过由我们所定义的安全策略，因为规则 4 要求两个布尔变量的结果必须是布尔类型 t y p e et a r r a y t p t rt a s i z eal e n s a f e w ras i z e s a f e r das i z e u p d mevs i z e s e l mes i z e s i z et n u m l te 1e 2 u l te le 2 g ee le 2 u g ee 1 e 2 e qe 1 e 2 n e q e 1e 2 s u b e le 2 a d de 1e 2 ( 1 ) 一阶谓词构造器 p f ( s i z ei n t4 ) p f ( s i z eb o o l1 ) p f ( s i z e ( p t rt ) 4 ) p f ( t y p ea ( p t rt ) - ) p f ( t y p es e l ( m a 4 ) t ) p f ( t y p ea ( a r r a yt ) ) - - ) p f ( a s i z e a l e n ) p f ( s i z e t b ) - - p f ( u l to f f l e n ) - ) p f ( t y p e ( s e lm ( a d da ( m u l bo f 0 ) b ) t p f ( t y p e a t ) - - - ) p f ( t y p e 0 t ) - - ) p f ( t y p e ( a d d a b ) t ) p f ( t y p e a i n t ) - - ) p f ( t y p ebt ) p f ( t y p e ( a d d a b ) i n t ) p f ( t y p ea ( a r r a yt ) ) p f ( a s i z ea l e n ) - - - ) p f ( s i z et b ) 专 p f ( u l to f f l e n ) - - ) p f ( s a f e r d ( a d d am u i ( bo f f ) ) b ) p f ( t y p e a d d r t ) - - p f ( u l ta d d ru l i m i t ) - - - ) p f ( l t a d d rl l m i 0 - - p f ( s i z e t b ) - - ) p f ( s a f e r d a d d r b ) ( 2 ) 部分推理规则 图2 2 低