（计算机软件与理论专业论文）类型化低级语言的设计与实现.pdf

中国科学拙术人学顺。l j 学位论文 摘蛰 摘要 因特网舰模的不断扩大使锝移动计算成为一个重要的研究领域。在该领域内， 代码安全性问题( c o d es a f e t y ) 受到学者的广泛关注。移动代码的特点是异地编 写，本地执行。这种代码的来源复杂，代码的编写质量和执行后对主机的影响都 难以估计，因此如何防止来自网络上的恶意代码对主机的破坏成为成为代码安全 领域研究的热点之一。 本文的工作基于i n t e l 的开放式运行平台( o p e n r u n t i m ep l a t f o r m ，简称o r p ) 。 提出了一种类型化低级语言( t y p e dl o w l e v e ll a n g u a g e ，简称t l l ) ，将利用类型 信息所带来的类型安全性带到接近于汇编语言的一层。应用t l l 作为o r p 的即 时编译器新的中间语言，这个工作可以作为将来进一步缩小o r p 的可信任计算基 的重要起点。 t l l 比j a v a 虚拟机语言更接近汇编语言层，用t l l 编写的代码更容易进行 优化，且它基于多态类型化 算子，具有比j a v a 虚拟机语言更严格和更具有表 达力的类型系统，可以表达出很多高层语言的语言特性。 本文的主要内容包括： 1 阐述类型化低级语言提出的背景，对已有的几种有比较大的影响力的类型 化巾间语言进行概括和抽象。提出t l l 的理想特性。 2 给出t l l 的形式化描述，包括语法形式，操作语义规则和静态语义规则。 3 重点描述t l l 对数组和对象这两个高层数据类型的处理。为了给出更直 观些的感觉，文中还就这方面的具体的例子来详细解释t l l 程序是如何 通过类型检查获得类型安全性的。 4 描述了从j a v a 虚拟机语言到t l l 的翻译过程，给出翻译算法。 5 类型化中问语言是提高代码安全性的一类重要方法，然而在其实现过程 中，庞大的类型信息很难被高效的表达和操作。一个未经优化的实现将会 给系统带来指数级增长的开销，因此本文还描述了在实现过程中用到的一 些优化实现技术。 关键字：类型化语言，代码安全，类型制导编译器 本课题得到国家自然科学基金项目( 6 0 1 7 3 0 4 9 ) 和i n t e l 中国研究中心资助。 中国科学技术大学坝， j 学位论j 摘要 a b s t r a c t t h ee x p l o s i v e g r o w t h o fw o r l dw i d ew e bh a si n d u c e di n t e r e s ti nm o b i l e c o m p u t a t i o nf o r “p r o g r a m m i n gt h e w e b ”i nt h i sd o m a i n ，t h es a f e t ya n ds e c u r i t y p r o p e r t i e so fp r o g r a m s a r em o r ec r u c i a lt h a ne v e rb e f o r e ，w r i t t e nb yt h et h i r dp a r ta n d r u na tt h ei o c a lh o s t 、m o b i l ec o d e sc o m ef r o mc o m p l e xs o u r c e s ，s ow ec a nn o tk n o w t h ec o d e sq u a l i t ya n dt h ee f f e c ta f t e ri ti se 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 e c o d ef r o mh a r m i n gh o s t i n gn o d e s i st h ep r o b l e mt h a tw e t r yt oa n s w e r t h i st h e s i si n t r o d u c e st l l ，at y p e dl o w l e v e ll a n g u a g e ，d e s i g n e dt ob r i n gt y p e s a f e t yt oal e v e lc l o s et oa s s e m b l el a n g u a g e o u r w o r ki sb a s e do ni n t e lo r p , w h i c hi s av i r t u a lm a c h i n e a sg e n e r a l ，i th a sav e r yh e a v yt c b w et r yt ou p d a t ej i t c o m p o n e n t o fo r p t h r o u g ho u rt l l a n da i ma to b t a i n i n gt y p es a f e t ya n dt h e nb u i l d i n g as m a l l e rt r u s t e dc o m p u t i n gb a s e t l li sc l o s e rt oa s s e m b l el a n g u a g et h a nj v m l ，a n dc o d ew r i t t e ni nt l li s c o n v e n i e n tt ob eo p t i m i z e d t l lt y p es y s t e mi sb a s e do np o l y m o r p h i ct y p e dl a m b d a c a l c u l u s ，w h i c h i s e x p r e s s i v e a n dg e n e r a lt oe n c o d ev a r i o u s h i g h l e v e ll a n g u a g e f e a t u r e s t h em a i nw o r k so f t h i st h e s i sa r ei nt h ef o l l o w i n g ： 1 e x p l a i n o u rr e s e a r c hb a c k g r o u n da n da n a l y z ee x i s t i n gs e v e r a lt y p e d i n t e r m e d i a t el a n g u a g e s ，w ep r o p o s e dt h ee x p e c t e da n di d e a lf e a t u r e so f o u r t l l 2 g i v et l l sf o r m a ls p e c i f i c a t i o n ，i n c l u d i n gs y n t a x ，o p e r a t i o n a ls e m a n t i c s ， a n ds t a t i cs e m a n t i c s 3 p r e s e n tt w oc a s es t u d i e s ( o b j e c t e n c o d i n g a n d a r r a ya c c e s s ) a n d e x p a t i a t eo n h o w t l l p r o g r a mg a i ns a f e t yb yt y p ec h e c k i n g 4 t r a n s l a t i n gf r o mj v m l 0t o t l li so u rm a i np u r p o s e ，s ow eg i v et h e f o r m a lt r a n s l a t i o na l g o r i t h mi nag l o b a lt r a n s l a t i o ne n v i r o n m e n t 5 t y p e d i n t e r m e d i a t el a n g u a g ei sa ni m p o r t a n ta p p r o a c ht oc o d es a f e t y u n f o r t u n a t e l y , t y p ei n f o r m a t i o ni s d i f f i c u l tt or e p r e s e n ta n dm a n i p u l a t e e f f i c i e n t l y an a t i v ei m p l e m e n t a t i o nc a ne a s i l ya d de x p o n e n t i a lo v e r h e a d t ot h ec o m p i l a t i o na n de x e c u t i o no fap r o g r a m t h i sp a p e r d e s c r i b e so u r 中国科学技术大学坝：l 学位论文 摘美 e x p e r i e n c e a n d t e c h n i q u e s w i t h i m p l e m e n t i n g o u r t y p e d l o w - l e v e l l a n g u a g ei nt h ej i tc o m p i l e ro f i n t e lo p e nr u n t i m ep l a t f o r m k e y w o r d s ：t y p e dl a n g u a g e ，c o d es a f e t y ，t y p e d - p r e s e r v i n gc o m p i l e r 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 i7 3 0 4 9 ) a n di n t e lc o r p c h i n ar e s e a r c hc e n t e l 1 1 1 第一辑绪论 1 1 研究背景和意义 第一章绪论 因特网规模的不断扩大使得移动计算成为一个重要的研究领域。在该领域内， 代码安全性问题( c o d es a f e t y ) 受到学者的广泛关注。移动代码的形式有很多种， 比如用户浏览网页时，主机执行的插件程序；从互联网上下载的驱动程序或一个 娱乐用的游戏程序等等。这种代码的特点是代码来源复杂，代码的编写质量良莠 不齐。这种以异地编写，本地下载执行为特征的移动代码是否是可信的? 运行它 会不会破坏主机的数据，访问朱授权的资源，最终造成主机的崩溃，重要数据丢 失? 更甚者，当此代码是恶意代码时如何防止它的破坏作用? 传统的解决移动安全问题的方法包括特征代码检查，内核督察，代码检测以 及加解密技术。这些方法按照固定的安全策略对移动代码进行检查，因而缺乏灵 活性。而些基于语言的安全检查方法提供了灵活解决移动代码多方面安全需求 的通用框架。s c h n e i d e r 将基于语言的安全检查方法定义为基于编程语言的理论和 实现技术来解决安全问题的一组方法，可以利用的检查手段包括语义，类型，优 化和验汪等。无论使用何种手段，它的基本想法是一致的： 编译器在编译高级源语言的过程收集许多关于程序的信息，比如变量的类型 信息或变量值的界限，还有结构信息，命名信息等等。这些信息通过某种方法保 留下来与编译后的指令序列一起移动到代码的接受方，代码接受方可以利用这些 信息来判定移动代码是否满足主机既定的安全策略。 图l l 显示了基于上述想法的一个典型的工作流程。代码发送方在编译高级 语言的过程中对源代码收集上述的额外信息。这些信息，称之为“证书”，附加在 目标代码之中。接受方在得到代码的同时也得到这些附加信息。它运行一个验证 器检查代码和整数，验证代码是否符合某种主机安全策略。若验证成功，则代码 可安全执行。在这里，除了验证器是接受方可信任的组件外。编译器，目标代码 和证书均可以不是，这样就有效的缩小了信任基。这种方法最大好处是将创建正 确性证明的任务留给了代码生产方，接受方的任务只是验证证明过程是否正确， 因此工作量得到极大降低。 根据“证书”采用的形式不同，目前这种基于语言的研究代码安全性的方法 里壁堂垫查盔兰塑：! 兰丝堡兰 主要分为两类：l ，逻辑证明法：2 ，类型注释和类型检查法。前者用逻辑来表达 机器代码的安全特性和安全性证明，p c c 是这类研究的代表 n e c 9 7 。它的证书 是验证条件的一阶逻辑证明，其验证过程是检查浚证书是否为有效的一阶证明。 后者的证书是类型注释，验证过程是静念的类型检查。它基于一个良类型假定： 一个良类型的程序不会崩溃，它的行为遵循定型规则对它的约束 m i l 7 8 。 图1 1 基于语言的安全原理图 每个方法都有自己的优缺点。基于逻辑的方法，使用通用目的的逻辑 ( g e n e r a l p u r p o s el o g i c ) ，它们可以对非常复杂的安全属性编码。但是，因为它使 用这些低层逻辑原语建立抽象结构，所以很难获得一个紧凑的验证代码。类型化 的方法则不如逻辑方法表达力强而灵活，但是它可以提供更加简洁，同时也相当 精确的代码信息。这些信息可以自动通过一个类型检查器的验证。与基于逻辑的 方法比较，类型化方法更为大多数语言设计者所熟悉。有些相关技术，比如类型 推导、类型检查等等都是成熟的。另外，类型系统可以渐增式的开发，逐步增添 新的类型来表达不同的抽象概念。有些研究，例如u 1 a l 【n i 0 2 ，甚至将两种方法 结合应用。 但是不管采用哪种方法，它们都有共同的目标：利用编译时产生的额外信息 来帮助解决移动代码的安全问题。基于本项目的研究内容和背景，这里不准备对 逻辑证明的方法展开讨论。主要介绍的是类型化方法这个领域的研究内容。 在高级语言中，m l ，j a v a 都是类型安全的语言。它们都有自己丰富的类型系 统。类型化中间语言试图将高层的这种类型安全性带到编译器的中间语言 s h a 0 9 7 t m c 9 6 】，甚至是汇编语言的层次【m w c g 9 9 , m c g 9 9 】。耶鲁大学的研究项目 “t y p e b a s e dc e r t i f y i n gc o m p l i l e r ”显示了一种扩展现存类型系统的可行道路。可 墨二量竺丝 以使用静态类型信息来帮助生成可被证明的安全代码，使用类型信息柬验证高级 的数据结构，例如u n b o x e d 数据结构不带边界检查的数据访问，运行时类型指 派，方法调用和内存管理等等。通常把具有这种能力的编译器称为类型制导编译 器( t y p e p r e s e r v i n gc o m p i l e r ) 。这样的编译器也是验证编译器( c e r t i f y i n gc o m p i l e r ) 的种( 所谓验证编译器就是用户可以自己验证它所生成的代码的安全性的编译 器) 。在一个类型制导的编译器中，源代码被翻译为目标代码。同时，源代码的类 型信息也同样被翻译为目标代码的类型信息。这样，一个良类型的源程序经过这 样的编译器编译得到的目标代码也是良类型的，也即享有同样的类型安全性质。 只要对这样的类型化目标代码进行类型检查就可以保证程序的类型安全性。图1 1 中的验证器在类型化的方法中就是静态的类型检查器。 1 2 研究现状 在过去的十年间，出现了大量的利用这种基于语言的方法来获取低层语言的 安全性质的研究工作 a n a 0 2 ，n e c 9 7 1 。其中j a v a 字节码是第一个得到成功的商 业运作并具有广泛影响力的类型安全语言。耶鲁大学的f l i n t 项目正在开发一种 通用类型化中间语言 s h a 0 9 7 ，l s t 9 9 。康奈尔大学的t a l 项目开发了能生成类 型化汇编语言的验证编译器 m w c g 9 9 ，m c g 9 9 。上述研究项目都有一个共同点： 利用验证编译器，将用类型来表达的信息一直从源程序层保留到目标代码层。这 样的信息将被接收方用来进行安全验证，证明程序遵守规定的安全策略。它们都 对本项目组的工作有重要启发作用，因此下面分三个小节逐个对它们进行一个概 诛。 1 2 1 类型化的汇编语言( t y p e da s s e m b l yl a n g u a g e ) 类型化的汇编语言t a l 的理想目标是提供一种低级的，静态的类型化目标语 言，使之比j a v a 字节码更加适合于支持众多的源语言以及大量的优化。理论上它 是个理想化的精简指令集风格的汇编语言，是为一个简单的抽象机设计的形式 化操作语义。它是一个形式化类型系统( 多种类型系统的集合) ，这个类型系统可 以抓住处理器的寄存器状态的性质，以及栈和内存的性质。严格的证明可以显示 1 i a l 将一些重要的安全保证嵌入了汇编语言程序中。 最初的t a l 版本是通过对一种类m l 的多态类型抽象语言进行一系列变换而 中国科学技术大学颤i j 学位论史 得到的结果 r f g 9 3 】这些变换被称为保类型变换。最终形成的t a l 基于传统的 r i s c 汇编语言。t a l 的静态类型系统加强了高级的语言抽象，例如闭包，元组 以及用户自定义的抽象数据类型等。t a l 的类型系统保证类型币确的程序不会违 反这些抽象。而且，t a l 的类型系统刁i 会阻碍如寄存器分配，指令选取和指令调 度之类的低级优化。 早期t a l 版本的变换中包括了后续传递语言( c p s ) 变换，c p s 使用堆分配 的活动记录取代栈分配的活动记录。堆分配与传统的栈分配的实现相比有不少的 优点 g k n d 9 8 】：易于实现一些控制原语如异常，一阶后续等：a p p e l 和s h a oz h o n g 指出堆分配可以节省空间，因为它更容易共享环境：堆分配有统一的内存管理机 制( 垃圾收集) 来分配和释放各种对象，包括活动记录。但是有两个重要的因素 使得提供堆栈的支持很有必要；基于栈的活动记录所占用空间比基于堆的活动记 录要小：许多芯片的体系结构设计要求应用程序使用基于栈的方法，例如，奔腾 p r o 芯片内部有一个用来预测过程返回地址的内部栈，它来源于使用标准控制栈 的调用返回原语。因此t a l 的后续版本添加了栈，它的文法参见 m c g 9 9 。 n e a lg l e w 和g r e gm o r r i s e t t 指出将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 gm o r r i s e t t 提出使用b a k ei ti n 方法，“不优化”方法，以及重构和压缩算法等，可以得出相 当精简的注解，最后形成的注解大小约为代码总量的l o 。 目前，t a l 已实现的版本叫做t a l x 8 6 软件包。它定义了类似与c 的高级语 言p o p c o r n 。p o p c o m 是一个安全的c b a s e d 语言，它提供一级多态，抽象类型， 带标签的联合，异常和一个简单的模块化系统的支持。另外，p o p c o r n 还支持其 他的类似c 的特性，如栈分配的数据等。软件包中包括了一个类型检查器，它对 几乎所有的i n t e lp e n t i u m i a 3 2 的体系结构都适用；一些为了汇编，反汇编，链接 t a l 二进制文件( 一对机器代码段和类型段) 的工具：以及个为p o p c o r n 做的 原型编译器。 t a l x 8 6 本身是i n t e li a 3 2 汇编语言的一个静态类型化的形式。它的指令和数 据使用m a s m 的语法，还增添了一部分类型注释的语法用来给验证时用。类型 的注释可以被分为以下一种类别： 第一臂绪论 1 2 3 4 5 6 输入输出接【 信息用来对每个目标文件进行类型检查 类型构造符声明一用来声明新的类型和类型的简写。 代码入口标签的类型前条件一用来指定寄存器必须具有的类 型，这样控制流彳一叮以进入稠联系的代码。 数据标签的类型一用来指定一个静态数据项的类型 指令的操作数的类型强制用来强制转换类型 宏指令一用来装入一一系列小的指令，这样类型检查器计待这一 个系列就像对待一个原子操作。 t a l 还不完善，还需要进一步的扩展。f l 前t a l 类型系统的个重要缺点是 刁i 能有效的释放内存对象，而要依靠一个垃圾回收程序来回收对象，从而阻止了 对内存的及时重用而这种重用在类型化低级语言中是很关键的。f r e d e r i c ks m i t h 和d a v i d w a l k e r 提出使用指针别名的方法，将指向内存位置的指针也作为一种类 型加入类型系统，可以保证在释放内存对象时不会破坏1 1 a l 代码的良类型性质。 这样需要对现有的类型系统做很大的变动，因此目前还没有真正使用这扩展。 其他处于研究之中的对t a l 的扩展还包括，删除数组越界检查和运行时的代码生 成等。 1 2 2 类型化中间语言f l i n t 高阶类型化( h i g h o r d e r t y p e d ) 语言，推动了可扩展、模块化软件的发展。 它包括了那些对象包含方法并且能够静态和动态定型的类型化语言，如m l 、j a v a 。 虽然这些h o t 语言通常是安全语言，且实现的程序具有结构良好、易于扩展的 特性，但是在目前操作系统下它们缺少好的底层平台和工具，也不具有和一些低 层语言( 如c ) 高效的互操作性，因此使它不能重用低层的库。不同的h o t 语言 通常具有自己的运行时系统，包括特殊的垃圾收集器，异类语言函数调用接口。 在这些语言中进行互操作和通信是不可能的事情。如果要开发一类新的h o t 语 言的编译器，考虑到传统的中间语言c 不支持强类型检查、自动内存管理，只能 另外编写这些模块。 耶鲁大学的f l i n t 项目的目的就是为多种高阶类型化语言建立一个良好的系 统环境。项目中主要的部分就是使用一种一般化的类型化中问语言，也就是 f l i n t ，来为各种h o t 要素的语义建模。f l i n t 建立在多态 演算f 。的个谓 词多态变种之上，并用一个丰富的基本类型构造符和类型函数集将其扩展。尽管 h o t 语言在语义上有很大的区别，但是它们都在数学意义上具有严格的类型系 统，而且f 。演算通常作为一种原语言来分析形式逻辑和语义，所以几乎所有的 ! 壁l 型兰丝查查兰竺! ：兰些堕兰 h o t 要素都能被坡编译成类f 。，演算，这也是f l i n t 的理论基础。 f l i n t 提供了一个一般的编译器后端，能够快速的产生一个新h o t 语言的 编译器。由于它统一的类型系统，且这个类型系统决定了运行时的所有表示，所 以f l i n t 可以作为多个h o t 语占的连接平台以实现互操作它的系统以及的垃 圾收集、异类语占函数调用接口也可以被多个高阶类型化语言所共享。由于其丰 富的类型系统，项目的开发者认为f l i n t 具有比j a v a 虚拟代码更强大的功能， 在互联网编程上具有良好的前景。 f l i n t 编译系统是围绕着强类型化中间语言f l i n t 组织的，图1 - 2 展示了 f l i n t 系统的结构。该结构分成四层：前端、中端、后端、运行时系统。 各种源语言编写的程序输入前端。前端是源语言相关的，它的工作是对各种 源语言程序进行分析、加工、类型检查、模式匹配编译，源程序将被翻译成f l i n t 中间格式。 中端不仅对f l i n t 中间语言程序进行传统的优化工作：数据流分析、循环结 构优化、局部和交叉模块类型特殊化( s p e c i a l i z a t i o n ) 而且还要进行基于 演算的 紧缩和规约，产生优化版本的f l i n t 代码。 后端通过以下几个步骤将f l i n t 编译成机器代码：多态表示分析、高阶函数 的闭包转化、寄存器分配、指令序列规划、机器代码生成。为了使中间语言f l i n t 的类型系统比较简单，多态和高阶函数留到后端处理。把类型信息传输到低层还 是为了在后端产生类似于n e c u l a 的p c c 风格的携带证明代码。 运行时系统提供了对垃圾收集、异类语言函数调用接1 ：3 的支持，还提供了到 底层操作系统的连接。 在这样一个结构上产生新语言的编译器，只要写一个从源语言到f l i n t 的前 端。如果这个新语言是嵌入到一个一般的语言中的，那么只需要修改宿主语言的 前端，使它支持嵌入语言。当新语占有新的原语操作、类型构造符时，目前的f l i n t 系统需要在中间语言中加入这些成分，并对优化器进行相应的修改。f l i n t 系统 的开发者认为绝大多数的语言成分能够被抽象到一个代数数据类型集中，它有着 基本类型、基本构造府和正确的重写规则，对中间语言和中端的修改将会实现自 动化。 f l i n t 中间语言作为f l i n t 系统的核心部分，披设计为一个强类型化的一般 语言这对建立一个类型安全的中间语言有许多的优点： 一个严格的类型系统能够在中间语言阶段就能对程序的安全性进行分 析。这对象j a v a 虚拟机代码这样移动的应用时十分重要的a 塑二：里堕堡 m ls a f ec j a v ah a s k e l | d s l s l e x e r p a r s e r l e x e r p a r s e r l e x e r p a r s e r l e x e r p a r s e r l e x e r p a r s e r t y p e lj t y p eli t y p eli t y p eli t y p e c h e c k e ril c h e c k e rll c h e c k e rif c h e c k e rli c h e c k e r t h ef l i n ti n t e r m e d i a t el a n g u a g e b a c k - e n dc o d e g e n e r a t o r i n t e lx 8 6 lls p a r cll a l p h a iij a v a v m i1 0 t h e r m i d d l e - e n d o p t i m l z e r t h ef l i n tp o r t a b l ec o m m o nr u n t i m es y s t e m r s y s t e ml i b r a r i e s ，b o o t s t r a p p i n g ，g a r b a g ec o l l e c t i n g ) 图1 2 f u n t 的系统结构 类型信息有助于分析在不同的语言中的互操作性。由于数据表示和函数 凋用规则建立在统一的类型系统之上，不同源语言的程序能够共享一个 运行时系统。 类型信息对于静态定类语言( 如m l ) 的高效编译是很有价值的。类型也 有助于编译器逐步调试和验证程序的正确性。 f l i n t 的核心语言是多态 演算f 。的一个谓词多态变种，再加上用a 范式( a n o r m a lf o r m ) 写的项语言。f l i n t 的核心语言在标准f 。上作了三点重要的变化： 在标准的f 。演算中，多态类型和单态类型具有相同的种类( k i n d ) ，这 使语义复杂且演算具有非谓词的多态。在f l i n t 中，把类型结构分成两 层：构造符( c o n s t r u c t o r ) 一层用来刻画单态类型和类型函数：类型一层 来刻画多态类型。 值调用的项语言也分成两层，用值来指示简单变量和常数。通常的项表 ：! 里壁兰丝查查兰竺! ! ：兰竺堡苎 达式必须满足a 范式。标准演算中f 。的函数应用项被重写成嵌套1 e t 表 达式。 新的积种类k x 被加入种类语言，用来表示一系列的类型构造符。这 样类型函数可以用一系列的类型构造符柬作为参数或返回值。 f l i n t 包括五个语法级别：种类( k ) 、构造符( u ) 、类型( 0 ) 、项( e ) 、 值( u ) 。种类为构造符分类，类型为项和值分类。q 种类的构造符只包含单态 类型，单态类型由变量、整数，通过构造符一产生。构造符的抽象和应用相应于 函数种类k 一k 。；积和选择构造符相对应于积种类k 。ok ! 。类型包括单态类型， 及其在函数空问的闭包，以及多态量词。f l i m 的静态语义规则以及类型推导规 则可以参见 s h a 0 9 7 j 。 f l i n t 的完全语言在核心语言上增加了更多的语法成分：在项层次上的l e t r e c 函数，允许相互递归函数：构造符一层上的“和”类型构造符来表示类m l 语言 的复合数据类型：在构造符一层上的递归操作符，以及相应的项一层上的操作符 r o l l 和u n r o l l 在递归类型值和“和”类型值之间转化；异常操作原语等。 ( k i r ld s )盯：= q 】r 1j 2 1 彭1 盯2 ( c o n sj：= ，fi n tf 斗( 1l ，2 ) 五t ：茁i l 卢2 】 l ( t 2 ) l1 7 ，l 兀2 ( t y p e s )o - ：= t ( ) vt ：f 盯i 盯l jo - 2 t er ms ) p ：= v i 兄x ：o - ei v i v2 1 人t ：盯elv a 】 li e tx=p1i ne2 ( v a i u e s ) v ：= x j i 图1 3f l i n t 核心语言语法 目前，f l i n t 已经实现了对诸如m l ，j a v a 等语言的支持 l s t 9 9 】，提供了从 这些高层语言到f l i n t 核心语言的转换前端。2 0 0 1 年，f l i n t 系统正式发布作 为s m l n j 编译器( h t t p ：c m b e l l l a b s c o m c m c s w h a t s m l n j s o f t w a r e h t m l ) 的一 部分。 1 2 3j a v a 虚拟机语言 j a v a 语言是基于语言的安全方法的一个成功的实例。它开创了不依赖于平台 第一章绪论 的网上编程的先河，在这个领域上安全是最重要的因素。人们用j a v a 编制程序时， j a v a 编译器产生平台无关的字节码( j a v ab y t e c o d e ) ，又称为j a v a 虚拟机语言( j a v a v i r t u a lm a c h i n el a n g u a g e ，简称j v m l ) 。j a v a 到j v m l 的翻译是类型保持的。 j a v a 虚拟机语言包含了足够的类型信息使自动验证器能够证明内存安全和其他属 性， 字节码程序在执行之前由接收方检验其安全性然后j a v a 虚拟机解释执行字 节码或者字节码被进一步编译为本地的机器指令来执行。 在j a v a 的安全运行环境中包含一个字节码检验器，用来保证代码的内存安全， 控制流安全和类型安全。它还包括一个安全管理器，用来加强一些高层的安全策 略，如限制a p p l e t 对磁盘i o 的访问。这些概念与类型检查合并在一起，组成了 有效的“沙箱”模型。限制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 m p h e nn f r e u n d 提出了种比较 完善的j a v a 类型系统 s j 9 8 ，s j 9 9 1 ，包括了j a v a 字节码语言的大部分，有类，借口， 方法，构造函数，异常以及字节码子例程等，为开发字节码语言以及j a v a 虚拟机 验证器的行事规范奠定了基础。 1 3 本文主要工作和创新点 本文研究工作的重点是设计一个类型化低级语言做为即时编译器的中间语 言，并实现相应的编译器前端。涉及的内容包括类型安全的概念、类型化方法的 目的和意义、类型化方法的应用、类型化低级语言的提出、类型化低级语言的形 式化描述、对象编码、数组定型、从j a v a 虚拟机语言到类型化低级语言的翻译环 境、对方法的翻译、类型表达式的表示法和类型操作等。在研究过程中，笔者对 大量相关研究文献进行了分析理解，为类型化低级语言的设计提出若干设想，负 责其中的数组设计，包括数组类型、数组指令系列、j v m l 的数组指令翻译序列 等工作。提出类型表达式的表示法和其操作的可实现方案。并做为主要人员参与 了以t l l 为中间语言的即时编译器的前端实现工作。 本文的章节安排、具体工作和创新点如下： 叶1 冽科学坎术= 学坝l 学位沦史 第一章阐述了类型化方法的分类和背景，类型化方法的特性以及它的研究- f 段和意义。介绍做为移动代码安全领域的一个重要研究方向，它目前的研究现状。 并对现有的几种具有较大影响力的相关研究项目进行了概括和抽象，做为本文研 究工作的基础。 第二章从具体应用的角度，解释和介绍类型化低级语言t l l 的提出。介绍 了t l l 的应用环境o r p ，在文中给出了o r p 的模块图和特性；通过对可信任计 算基的分析，引出设计t l l 的动机和最终目的，晚明t l l 是这项工作的一个重 要起点。并最终概括出t l l 的三点理想特性。 第三章给出t l l 的形式化描述，包括语法形式，操作语义规则和静态语义 规则。文中对组成t l l 程序的四个要素，堆，变量表，寄存器文件和全局变量声 明和指令序列都进行了详细的描述：解释t l l 的类型系统，包括堆值类型，类型 强制和复杂类型等：逐个指令分析介绍t l l 的操作语义；最后通过对静态语义规 则的阐述，说明了t l l 程序的良定义性质。 第四章重点描述t l l 对数组和对象这两个高层数据类型的处理。t l l 中的 对象编码采用了一种紧凑而高效的编码方法，源于n e wo l e w 的s e l f 类型编码 o l e 0 0 】。文中详细描述了为此引入的类型和类型操作，并给出t l l 中对象的翻泽 过程。对t l l 中的数组，我们使用单元素类型描述数组长度。在翻译过程中将数 组长度类型表达式和代表数组本身的表达式打包在一起，以便做越界检查时可以 获得正确的数组大小。为了给出更直观的感觉，这里还结合了一些具体的例子来 详细解释t l l 程序是如何通过类型检查获得类型安全性的。 第五章描述了从j a v a 虚拟机语言到t l l 的翻译过程。给出翻译算法。首先 描述用来记录从对象翻译过来的记录，类成员的类型注释，类方法表等信息的全 局翻译环境( g t e ) 。并给出在实现时使用的g t e 伪结构以及在g t e 中类的形式 化翻译算法。然后描述方法体的翻译过程。同样给出实现时使用的伪数据结构基 本块c f gn o d e ，方法翻译的伪过程m e t h b o d yt r a n 。该方法在翻译过程中收集类 型信息，并将每个j v m l 指令都翻译到相应的t l l 指令序列。 第六章类型化中间语言是提高代码安全性的一类重要方法。然而在其实现过 程中，庞大的类型信息很难被高效的表达和操作。一个未经优化的实现将会给系 统带来指数级增长的丌销。因此在这个章节中给出t l l 类型表达式的实现方案。 它结合d eb r u i j n 表示法，哈希联想存储法( h a s h c o n s i n g ) 以及懒惰代换( l a z y s u b s t i t u t i o n ) 的技术以达到提高效率的目的。文中对它们都进行了详细的分析和 介绍。 第一帝类型化低级浯吉的提 2 1 引言 第二章类型化低级语言的提出 因为类型化方法的各种优点，所以考虑将类型化技术应用到现存的某个具体 的j a v a 虚拟机实现上，整合类型化中间语言技术到该虚拟机的即时编译器 ( j u s t i n t i m ec o m p i l e r ) 中，以获得类型化技术所带来的种种好处。根据这个想 法，本项目组提出了类型化低级语言( t y p e dl o w 1 e v e ll a n g u a g e ) ，一个接近汇 编语言层的低级语言。我们探索使用t l l 作为该虚拟机的通用中间语言的可能 | 生，目的是为了支持多种高层语言，并尽量缩小它的可信任计算基。 以下分节具体介绍t l l 提出的动机，应用环境以及设计目标。第一节简要介 绍t l l 的应用环境。第二节提出可信任计算基的概念，从一个实用的角度说明 t l l 的需要性。第三节解释现有的虚拟机中间语言j v m l 和c i l 的不足之处，进 一步给出设计t l l 的动机。最后总结出希望得到的t l l 的特点。 2 2 开放式运行平台( o p e n r u n t i m ep l a t f o r m ) i n t e l 中国公司所研究开发的开放式运行平台o r p 是一种虚拟机的实现，由即 时编译器，垃圾收集器( g a r b a g ec o l l e c t i o n ) 和虚拟机内核( c o r e v i r t u a lm a c h i n e ) 三个主要模块构成，大多数这些模块都是用c + + 实现的。o r p 试图成为一个安 全的，可以支持多种高级语言的通用运行平台，并作为研究垃圾收集技术和编译 技术的一个丌放式平台。o r p 的优点在于灵活的体系结构，而且是开放源码的。 研究者可以更换三个主要模块中的任何一个，随时使用自己的新模块代替，以提 高整个虚拟机的性能。本次工作也是以它为研究平台，使用类型化方法来改造 o r p 中的即时编译器模块，替代原来的j i t 模块，期待可以整体的提高o r p 的安 全性。 目前o r p 已经有w i n d o w s 和l i n u x 两个版本，相应的软件包可以从 丝p 丛! ! ! ：嫂! ! 竖b ! 卫r ! q 业下载。目前它的性能也是很优越的，有关报告可以 参见h t t p g r o u p s , y d m o c o m g r o u p o r p 。 中国科学技术大学埘。学位论二：【： 囡囡日圉 0000 图2 1o r p 的主要组件 2 3 更小的可信任计算基( t r u s t e dc o m p u t i n gb a s e ) 在衡量一个系统是否容易受攻击的性能时，人们往往使用一个叫做可信任计 算基的概念。任何在t c b 之内的软件错误都能引起系统的安全漏洞。t c b 越大， 系统就越脆弱。 作为j a v a 虚拟机的一个具体实现，o r p 跟其陋的虚拟机一样，拥有的主要模 块类加载器，即时编译器，垃圾收集器，核心运行时系统和用来支持a p i 的本地 方法库模块都是t c b 的部分，其中的任何一个软件错误都可能导致安全漏洞。 图2 2 给出来o r p 的t c b 组成模块。 o r p 并没有严格的字节码验证器，而是选择在编译的过程中进行一些简单的 验证工作。在其他带有字节码验证器的j a v a 虚拟机中，即时编译器会在验证通过 以后再对字节码程序进行翻译。两种做法在实质上是一致的，同样不能保证在翻 译的过程中仍然保持住字节码层的安全性质。攻击者可以设计恶意的程序，利用 编译器的漏洞破坏安全性质，因此编译器被包含在t c b 之中。 类型安全的t l l 的一个优点就在于目标的t l l 代码不会进行不合法的行为， 因为它需要通过类型检查器的验证。因此人们可以想象出一个理想的高安全性的 j a v a 虚拟机实现，如图2 3 。它一样拥有类加载器，垃圾收集器和运行时系统， 同时还包含一个从j v m l 到t l l 的翻译器。这些组件都用t l l 实现。类型安全 性保证在这些组件中没有安全漏洞。一个t l l 运行系统是t c b 的唯一模块。它 第二章类型化低级语言的提出 图2 2 0 r p 的t c b 构成图 包含t l l 类型检查器，从t l l 到本地代码的一个翻译器，虽后还有一个很小的 启动系统。在核心虚拟机启动以后，应用程序的类文件将被进g 亍- p n 下程序的处理： 加载，连接，从j v m l 到t l l 的翻译，t l l 到本地代码的翻译。运行时系统将 扮演个对操作系统界面的角色。因为t l l 接近于机器代码，从t l l 到本地代 码的翻译器是一个很小的模块。如果t