（计算机软件与理论专业论文）基于逻辑的程序验证方法在高可信软件开发上的应用.pdf

中文摘要 摘要 随着软件规模的越来越大，软件的安全越来越引起软件开发人员的关注，而 现有的编程语言以及软件开发方法所能提供的安全保证是脆弱和不可靠的，例如 通过标准的软件工程方法和大量的测试减少软件漏洞的发生，但是即使经过高强 度测试的软件，也不能保证它没有漏洞，另外一方面，对一个漏洞的修复也往往 会引起新的漏洞。可以说，现有的软件工程方法对软件安全的提高已经越来越微 弱。而基于语言的程序验证方法能为软件安全提供可靠的保证。 基于语言的程序验证方法通过对程序设计语言添加静态的类型以及规范结 构，使得用这种语言写出的良形式程序是安全的。现有的关于认证代码技术以 及类型系统方面的研究已经能够验证低级语言和高级语言程序的多种安全属性。 例如，当前的大部分程序设计语言都有一个类型系统，它一般用于检查程序的一 些简单语义错误，可靠的类型系统可以以较低的代价保证程序的一些基本安全属 性。安全的高级语言和通用中间层语言的类型系统的研究已经对安全计算做了有 意义的贡献，但是用这些语言写就的安全程序还需经过多步的未经编译和优化才 能在最终的硬件上运行，这使得最终运行的代码是未经验证的。基于这个原因， 很多工作转向研究低级代码的验证，特别是研究从类型化高级语言代码产生可验 证低级代码的认证编译器。但是由于类型的弱表达能力，使得类型系统只能保证 代码一些最基本的安全属性，对用户指明的一些安全属性，比如算法正确性，信 息流安全等基本不能触及。也正由于这个原因，对于现实的底层软件如启动引导 程序，操作系统内核，用户态运行时函数库等，都没有相应的经过验证版本发布 出来，而这些底层软件的安全性对整个计算系统的安全性来说是至关重要的。但 是，类型系统对栈式函数调用的模块化验证有比较好的支持。另一方面，h o a r e 逻 辑具有很强的表达能力，因为相对于类型的弱表达能力，逻辑谓词能够表达更丰 富的程序属性，但是h o a r e 逻辑对栈式函数调用的支持比较弱。基于此，本文的研 究目标是以逻辑谓词代替类型作为规范标注程序，、鲒合类型系统和h o a r e 逻辑 两方面的优点，设计可以模块化地构造程序满足规范的证明的框架，并使用它 进行安全代码的开发。 本文提出一个基于逻辑的使用汇编语言的高可信软件开发方法，并运用此方 法开发出经过严格安全验证的运行时库和操作系统组件。此方法源于h o a r e 逻辑的 程序推理以及耶鲁大学的认证汇编编程( c a p ) ，它首先需要定义一个推理需要的 目标机器和一组静态推理规则，并且证明推理规则的可靠性( 安全性) 。本文的 贡献有如下几个方面： 设计并使用c o q 实现一个现实的x 8 6 平台上的认证汇编语言r c a l 8 6 ，并证明 中文摘要 它静态语义的可靠性。此语言避免了c a p 的在函数模块化验证支持上的不足 以适合实际的安全代码开发。 使用c o q 形式化基于栈的c a p ( s c a p ) ，并证明它的可靠性。s c a p 是一 个m i p s 风格的汇编语言，有着栈式的函数调用约定。 在r c a l 8 6 和s c a p 的推理框架里开发认证的操作系统和运行时函数库模 块。安全代码开发的实践表明，使用这种新的高可信软件开发模式是可行 的。 设计并实现分离逻辑( s e p a r a t i o nl o g i c ) 的c o q 模块。此模块能减轻进行数据 指针推理的难度，能显著减少用户输入的证明策略的数量，从而提高证明开 发效率。 提出机器字的位矢量表示，从而同时支持位运算和算术运算的h o a r e 逻辑风 格推理。据作者所知，目前还没有对位运算形式化推理的研究。 文中所有的形式化描述和证明都使用高阶逻辑的定理证明工具c o q 进行了形 式化。本文的工作表明，相对于类型系统以及其他一些自动定理工具，为低级代码 手动构造安全性证明能使验证后的程序满足更多的安全属性，但是目前要花费比 较大的代价。即便以这种方法构建携带证明的代码比较困难，但仍有着比较大的 开发效率上的提升空间，所以具有较大的研究和应用前景。 本文由中国国家自然科学基金资助( 编号6 0 4 7 3 0 6 8 ) 。 樾：南曩篇软叶， 气植寸百警珥，彳畸诧乞 a b s t r a c t 英文摘要 t o d a y ，m o s ts o f t w a r e ea r eo fl a r g es c a l e ，s ot h ep r o g r a m m e r s h a v ep a i dm u c h m o r ea t t e n t i o nt ot h e i rs a f e t y b u tu n t nn o w t h es a f e t yg u a r a n t e ep r o v i d e db ye x i s t i n gp r o g r a m m i n gl a n g u a g ea n ds o f t w a r ee n g i n e e r i n gt e c h n o l o g yi sw e a ka n du n r e l i a b l ef o ri n s t a n c e ，i nt h ep r o d u c t i o no fs o f t w a r e ，s t a n d a r de n g i n e e r i n gm e t h o d a n di n t e n s i v et e s t i n g sa r eu s e dt od e c r e a s eb u g sh o w e v e r 、i tc a n tb eg u a r a n t e e d t h a tt h e r ea r el i eb u g sa f t e ri n t e n s i v et e s t i n g s ，i nf a c t ，n e wb u g sw i l lb ei n t r o d u c e d w h e nt h eo l db u g sa x ef i x e di tc a nb ea s s e r t e dt h a te x i s t i n gs o f t w a r ee n g i n e e r i n g t e c h n i q u e sc a l l l ti m p r o v et h es o f t w a r es a f e t ya n ds e c u r i t ye s s e n tay o nt h eo t h e r h a n d ，l a n g u a g eb a s e da p p r o a c ho fp r o g r a mv e r i f i c a t i o nc a np r o v i d eg u a r a n t e ef o r s o f t w a r es a f e t y l a n g u a g eb a s e da p p r o a c ho fp r o g r a mv e r i f i c a t i o nm a k e st h ep r o g r a m so ft h i s l a n g u a g es a f et h r o u g ha d d i n gl a n g u a g ec o m p o n e n t so ft y p e s ( 1 0 9 i cp r e d i c a t e s ) ， w h i c ha r ec a l l e dp r o g r a ms p e c i f i c a t i o n su n i v e r s a l l y ，a n dt y p i n gr u l e s ( r e a s o n i n g r u l e s l ，w h i c hs h o u l db ed e 丘n i t e l yp r o v e dt ob es o u n d e x i s t i n gr e s e a r c ho nc e r t i - f l e dc o d ea n dt y p es y s t e mh a sc o n t r i b u t e dm u c ho nt h eg u a r a n t e eo fav a r i e t yo f p r o g r a m ( h i g h - l e v e lo rt o w - l e v e l ) s a f e t yp r o p e r t i e s ，s u c ha st h es i m p l et y p es y s t e mo f m o d e r np r o g r a m m i n gl a n g u a g e ，w h i c hc a nb eu t i l i z e dt oc h e c ks o m es i m p l es e m a n - t i c se r r o r sa n dg u a r a n t e ef u n d a m e n t a ls a f e t yp r o p e r t i e sw i t hl i t t l ec o s ta l t h o u g h r e s e a r c ho i lt y p es y s t e mo fh i g h l e v e la n di n t e r m e d i a t el a n g u a g eh a v ec o n t r i b u t et o c o m p u t a t i o ns a f e t ys i g n i f i c a n t l y , t h eu l t i m a t ec o d e se x e c u t e di nm a c h i n ea r eb i n a - r i e s ，w h i c ha x eo r i g i n a t e df r o mc e r t i f i e dp r o g r a m sa n dn o tc e r t i f i e dt h e m s e l v e s f o r t h i sr e a s o n ，m a n yr e s e a r c h e r sb e g i ne x p l o r et h ea p p r o a c h e so fl o w - l e v e lp r o g r a m v e r i f i c a t i o na n dc e r t i f y i n gc o m p i l e rw h i c hp r e s e r v e st h ep r o g r a ms p e c i f i c a t i o nf r o m h i g h l e v e lt ol o w l e v e lc o m p a r e dw i t hl o g i cp r e d i c a t e s ，t y p e sa r el e s se x p r e s s i v e ， s ot y p es y s t e mc a n td e a lw i t hc o m p l e xs a f e t yr e q u i r e m e n t s ，s u c ha sp r o g r a mc o t r e c t n e s s ，i n f o r m a t i o nf l o ws e c u r i t y t h u s ，a l t h o u g ht y p es y s t e mi sw i d e l yu s e d ， u n t i ln o w ，n oc e r t i f i e dv e r s i o no fb o o tl o a d e r ，o p e r a t i o ns y s t e mk e r n e l ，a n dr u n t i m e l i b r a r ya r er e l e a s e d tw h o s es a f e t ya r ec r i t i c a lf o r t h es a f e t yo fw h o l ec o m p u t a t i o n s y s t e m i nt h eo t h e rh a n d ，h o a r el o g i ch a se n o u g he x p r e s s i v e n e s ss i n c el o g i cp r e d i c a t e sc a l le x p r e s s m o r e i n f o r m a t i o n t h a r l t y p e sh o w e v e r ，t h es u p p o r to f s t a c k b a s e d f u n e t i o nc a l li sw e a ki nh o a r el o g i cf o rt h e s er e a s o n s t h eg o a lo ft i f f sr e s e a r c hi s s u b s t i t u t i n gl o g i cp r e d i c a t e sf o rt y p e sa sp r o g r a ms p e c i f i c a t i o ns ot h a tt y p es y s t e m 英文摘要 a n dh o a r el o g i ca r ec o m b i n e df o ran e wf r a m e w o r k i nt h i s a m e w o r k ，s a f ec o d e s c a nb ed e v e l o p e d t h i sd i s s e r t a t i o np r o p o s e sa na p p r o a c ho nh i g ha s s u r a n c es o f t w a r ed e v e l o p m e n tu s i n gl o g i c b a s e dc e r t i f y i n gl o w l e v e ll a n g u a g e ，i nw h i c hac e r t i f i e do p e r a t i n g s y s t e mc o m p o n e n ta n dr u n t i m el i b r a r ya r ed e v e l o p e d t h i sa p p r o a c hi so r i g i n a t e d f r o mh o a r es t y l ep r o g r a m r e a s o n i n ga n dc e r t i f y i n ga s s e m b l yp r o g r a m m i n g ( c a p ) o fy a l eu n i v e r s i t y s oat a r g e tm a c h i n ea n di n f e r e n c er u l e sa r er e q u i r e df o rr e a - s o n i n g ，a n ds u r e l yi n f e r e n c er u l e sm u s tb es o u n d ( s a f e ) t h i st h e s i sh a sf o l l o w i n g c o n t r i b l l t i o n ： d e s i g na n df o r m a l i z et h er e a l i s t i cc e r t i f y i n ga s s e m l b y l a n g u a g ef o rx 8 6 一l i k e m a c h i n e ( r c a l 8 6 ) i nc o q a n dp r o v et h es o u n d n e s so fi t ss t a t i cr e a s o n i n g r u l e s t h i sl a n g u a g ea v o i d st h ed e f i c i e n c yo fe x i s t i n gs i m i l a rr e s e a r c h ，s u c h a sc a p ，i no r d e rt ob em o r es u i t a b l ef o rd e v e l o p m e n to fs a f ec o d e f o r m a l i z et h es t a c k b a s e d c e r t i f y i n ga s s e m b l yp r o g r a m m i n g ( s c a p ) i n c o q a n dp r o v ei t ss o u n d n e s s s c a pi sam i p s l i k ea s s e m b l yl a n g u a g e ， a n dh a sas t a c ks t y l ec a l l i n gc o n v e n t i o n d e v e l o pac e r t i f i e do p e r a t i n gs y s t e mc o m p o n e n ti nr c a l 8 6a n dac e r t i f i e d r u n t i m el i b r a r yi ns c a p d e v e l o pac o qm o d u l ef 6 rs e p a r a t i o nl o g i c ，w h i c hi sl o g i cf o rd y n a m i cd a t a s t r u c t u r er e a s o n i n g b e c a u s ec o qi sai n t e r a c t i v et h e o r e m p r o v i n ga s s i s t a n t ， t h i sm o d u l ec a nr e m a r k a b l yd e c r e a s et h en u m b e ro fu s e ri n p u tp r o v i n gt a c t i c s a n di m p r o v et h ee f f i c i e n c yo fp r o o fc o n s t r u c t i o n f o r m a l i z et h em a c h i n ew o r da sb i tv e c t o r ss ot h a tl o g i ca n da r i t h m e t i co d e r a t i o nc a nb ee q u a l l ys u p p o r t e d a st h ea u t h o rk n o w s ，t h e r ea r en os i m i l a r r e s e a r c ho nt h er e a s o n i n go fb i tl e v e lo p e r a t i o nu n t i ln o w a l lt h ef o r m a ld e s c r i p t i o na n dp r o o fi nt h i st h e s i sa r ee n c o d e di nc o q w o r ko f t h i st h e s i ss h o w st h a tc o n s t r u c t i n gp r o o ff o rl o w l e v e lc o d em a n u a l l yc a ng u a r a n t e e m o r es a f e t yp r o p e r t i e sc o m p a r e dw i t ha u t o m a t i ca p p r o a c hs u c ha st y p ec h e c k i n g a n da u t o m a t i ct h e o r e mp r o v i n g ，b u tr e q u i r e sm u c hm o r ec o s tc u r r e n t l y a l t h o u g h i ti sah e a v yb u r d e nf o rp r o g r a m m e r st op r o d u c ec e r t i f i e dc o d e su s i n gt h i sa p p r o a c h ， t h e r ei ss t i l lal a r g ee f f i c i e n c yi m p r o v i n gs p a c e s oi th a sab r i g h tp r o s p e c ti nt h e r 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 nu n d e r g r a n tn o 6 0 4 7 3 0 6 8 昀w 。小； 括l 州盯蛳晓s 寸v 、r 盹，。门k 厶p 日r ? 3 ， 伽队b 岣均弋 背景介绍 第一章背景介绍 、 弟一早目京丌珀 、 在核反应堆，火箭，飞机的控制系统中，运行着大量经过无数次测试 和检查的代码。人们花大量的时间和金钱检查测试这些代码，是因为这些 代码中存在的任何一个漏洞，哪怕在千万次运行过程中都安然无恙，一旦 运行到这个漏洞时，结果都将时灾难性的f 1 1 。但是，人们在软件测试以 及一些软件静态检查工具上花费甚多，却不能保证测试和检查后的软件是 安全的。开发安全的软件基本上有两大类方法，程序分析f 2 ，3 幂l j 程序验 证f 4 ，5 1 。一般来说，程序分析是不可靠的，这意味着哪怕一个程序分析器 向你报告程序不违反某个属性，事实上也可能是违反的。但程序分析在各 种程序检查器和优化器中有着广泛的工程应用。我们评价一个程序分析器 的好坏，是根据分析过的程序的运行时表现以及分析所需的代价。而程序 验证是可靠的，我们能够宣布经过验证的程序不违反某个属性，并且有严 格的证明保证确实不违反。从这里可以看出程序验证的任务就是构造出一 个程序满足给定的规范的证明，每种不同的途径给出程序规范以及证明的 方法略有不同。本章将介绍本研究领域的一些基本概念和各种程序验证方 法及其最新的研究进展。 1 1基本概念 本节介绍程序验证研究领域中的常见概念和一些术语。 1 1 1程序的安全属性 代码安全的研究是为了保证开发出的代码是安全的，那么什么样的代 码是安全的? 也就是说代码的安全属性是什么? 从广义上说，代码的运行 时行为与期待的行为一致的属性就是代码的安全属性。但是完整精确地指 明代码期待的行为对于那些复杂的程序是不实际的，而且很容易出错。所 以，代码的安全属性就由一组安全策略来描述，指明哪些行为是可接受， 1 1 1 基本概念 哪些是不允许的。这样，我们说代码的安全属性得到了保证就意味着代码 的运行时行为都是可以被接受的。有很多种安全策略是必须的，比如内存 访问不越界，无非法指令及操作数等，还有一些安全策略是针对特定应用 的，比如信息流安全，访问控制等。另外还有一些安全策略是与正确性相 关的，比如最大公因子的计算函数某代码点处对变量值的特定要求f 6 1 。安 全策略体现在验证框架的多个方面，比如定型规则，逻辑推理规则，还有 程序的不变式( i n v a r i a n t s ) f 7 1 标注。题目中的高可信( h i g ha s s u r a n c e ) 不仅意 味着简单的类型安全，还包含正确性方面的要求。 那么，如何保证程序的安全属性呢，我们只要能够给出程序满足它的 安全属性的证明 5 】即可。关于这一点，有多种方式可以隐式或显示地给出 这个证明，在后面将详细描述。 1 1 2 信任计算基 信任计算基( t r u s t e dc o m p u t i n gb a s e ，t c b ) s l 是系统中用来推行系 统安全策略的部分，即必须要信任的部分。所有的计算机硬件是包含 在t c b 之内的，因为如果你不信任计算机硬件的正确性，什么也做不了。 在最常见的计算系统里，除计算机硬件外，操作系统内核属于t c b ，因为 无法保证内核是安全的，除非信任它是安全的。同样，控制系统操作的 配置文件，有s e t u i d ，s e t g i d 属性的应用程序，我们没有办法确信它们是安 全的，只有信任它们是安全。代码安全的研究另一个目的就是将计算系统 的t c b 尽可能的减小，因为如果存在一个很大的t c b ，即使我们证明了程 序具有要求的安全属性也是不够的。t c b 的减小使得我们对计算系统的安 全性能够获得最大的自信，因为无需信任许多组件。另外，想要整个计算 系统没有t c b 是不可能的，因为必须需要一个组件去推行安全策略，这个 组件的安全性是必须要被信任的。虽然无法消除t c b ，但是我们可以通过 仔细检查代码或者高强度的测试将精力集中在无法排除出t c b 的那一部分 组件上，使得它们尽可能安全。 综上所述，t c b 的大小也是至关重要的。 1 1 3规范语言的表达能力 无论是类型还是逻辑语言都可以用来描述程序的规范，如果一个形式 化语言能表达的程序安全属性更丰富，那么我们就说这个形式化语言的表 2o 背景介绍 达能力强。例如逻辑命题i 0 就比类型语言的一个类型判断i ：i n t 表达的信 息多，前者的表达能力就强。规范语言的表达能力也是至关重要的，表达 的信息少，则证明的对象就越简单，证明越容易，但能保证的程序属性就 越少。一般来说，一个简单的程序验证框架通常采用弱表达能力的规范语 言，因而可以使用自动的定理证明器，但是对于表达能力强的规范语言描 述的属性，必须借助手动或者半自动的定理证明工具。 1 2c u r r y h o w a r d n 构 目前程序验证方法有两种门类，一个是基于逻辑的方法，一个是基 于类型的方法。逻辑和类型理论两者之间存在紧密的联系，这种联系称 为c u r r y - h o w a r d 对应或者c u r r y - h o w a r d 同构9 ，1 0 1 。它的思想是，一个逻 辑命题p 的证明由p 的具体见证构成。c u r r y $ f l h o w a r d 注意到，这种见证有 很强的计算性，例如，命题pdq 的证明能被看做是给定一个p 的证明，构 造q 的证咀的过程。p 八q 的证明可以看做是p 的证明和q 的证明。逻辑命题 和类型有如下的对应关系： 逻辑编程语言 命题 命题pdq 命题p 八q 命题p 的证明 类型 类型p q 类型p q 类型为p 的项 命题p 是可证明的存在类型为p 的项 根据这个对应关系，一个简单类型化入演算的项对应相应的逻辑命 题的证明。计算( 入演算的消减规则) 相当于应用消去推理规则的证明过 程。c u r r y - h o w a r d 同构不仅限于特定的类型系统及相关的逻辑，相反，它 能被扩展到很多的逻辑和类型系统。以下是类型系统和逻辑系统的对应关 系。 3 13h o a r e 逻辑 类型系统逻辑系统 简单类型化入演算 s y s t e mf ( 带量词的类型) s y s t e mf u 线性类型系统 1 3h o a r e 逻辑 命题逻辑 二阶构造逻辑( 带量词的命题) 高阶逻辑 线性逻辑 程序语言研究对形式逻辑的使用开始于二十世纪六十年代f l o y d 1 1 军r l h o a r e 1 2 1 的论文的发表，这两篇论文被认为是基于逻辑的程序验证 的基石。h o a r e 在他的论文里提出一个形式系统，称作h o a r e 逻辑f 1 2 ，1 3 ， 用来对命令式语言程序的正确性进行推理。在h o a r e 逻辑里，要证明的命 题由著名的h o a r e - - 元组p s q 表示，它的含义是”如果当控制位于程序语 句s 的起始位置时命题p 为真，那么当控制位于s 的结尾时，q 将为真。所 有h o a r e 逻辑风格的验证框架都显式或隐式地包含这个三元组。在h o a r e 逻 辑里包含一组公理，如赋值公理和组合公理等： 公理1 3 1 卜p o x ：= ，) p j 其中z 是变量标识符，是表达式，p o 由将p 中 的所有出现的z 替换成，得到。 公理1 3 2 如果有卜p q 1 ) 兄1 和卜r i q 2 r ，那么有卜p q 1 ；q 2 r 。 利用h o a r e 逻辑可以进行程序的正确性证明。在h o a r e 的文章【1 2 】里就 有a l g o l 6 0 程序在给定前条件和后条件下的正确性证明，对应的h o a r e - - 元式 为： t r u e ( r ：= x ；q ：= o ) ；w h i l ey = rd o ( r ：= r y ；q ：= 1 + q ) - 1 y rax 2 r + y * q h o a r e 逻辑给研究人员一个希望，那就是所有的计算机程序的正确性都 可以用形式化证明严格保证。所以，在后续的十几年间，大量的研究工作 集中于扩展此系统，以便验证更复杂的语言结构，以及寻求更好的方式来 构造，表示，检查形式证明。例如，谓词转移语义( 1 4 并n 最弱前条件 1 5 】的 4 背景介绍 观点，以及用验证条件产生器和自动定理证明器f 1 6 1 进行程序的自动验证 等，h o a r e 逻辑用于j a v a 语言程序上的验证如f 1 7 1 0 然而，证明所有程序的正确性的目标后来被发现是遥不可及的，部分 的原因是描述源语言程序的正确性是困难的，另外一个原因是证明产生和 检查的机制不完善。正女q d e m i l l o 1 8 所说的那样程序正确性证明“绝不会 成功”。随着计算机技术的不断进步和对软件安全的迫切需求，h o a r e 逻辑 又被研究者采用。不象过去那样用它证明程序的正确性，大部分研究的目 标都是用它来证明程序满足一些重要的安全属性。并且更快的计算机也保 证了能开发出更有效率的定理证明器和检查器。 h o a r e 逻辑无疑是一个非常强大的程序验证方法，但是h o a r e 的对栈风 格( 先调用后返回) 的函数调用支持的不好，原因在于函数的返回地址是一 个代码指针，而代码指针的类型是多态的，h o a r e 三元组不能很好地反映这 一点。对栈式函数调用的验证，类型系统具有更好的模块性，模块性反映 在函数接口规范的信息隐藏以及函数的独立验证。 1 4类型系统 为程序设计语言设计一个可靠的类型系统f 1 9 1 ，从而通过这个类型系统 对应的类型检查器检查的程序就能保证是安全了。最简单的类型化语言是 简单类型化入演算，它眭t c h u r c h ( 1 9 4 0 ) 2 0 并 j c u r r y ( 1 9 5 8 ) 9 】提出。简单类型 化入演算的类型系统只包括函数抽象和函数应用。在此简单类型化入演算的 基础上，可以对类型系统进行扩充，增加各种类型构造符以及子定型，递 归类型等特色丰富语言对静态信息的表达能力。类型检查的过程是重构证 明的过程，所以类型化的程序无需携带证明，可以说，类型检查是隐式地 构造证明的方法。 对于命令式语言设计类型系统是困难的，主要在于语句的副作用使用 类型来表达比较困难。j a v a 语言f 2 1 1 有一个功能强大的类型系统，但是它的 形式化以及可靠性证明一直都没有实现，所以j a v a 语言不算是一个安全的 高级语言。为了减小编译器引起的信任计算基问题，人们设计了类型化的 低级语言，以使得高级语言的类型信息能够一直保持到低级语言。类型化 命令语言包括类型化中间语言t i lf 2 2 2 7 ，类型化汇编语言t a lf 2 8 ，2 9 1 ， 类型化机器语言t m l 3 0 等。 由于简单类型对程序属性表达能力的不足，h o n g w e ix i 3 1 3 3 】提出 5 1 4 类型系统 使用依赖类型进行程序验证和数组边界检查消除优化。一般来说，依赖 类型为依赖于语言值表达式的类型，比如i n t ( i ) 类型，这种类型的表达式 都有值i ，所以i n t ( i ) 称做单值类型，i 也称做类型索引表达式。通过这种限 制形式的依赖类型可以捕捉更多的程序不变式，并且有助于维护软件文 档。限制形式的依赖类型清晰地将类型索引表达式和运行时表达式分割 开来。在函数式语言上，x i 使用依赖类型丰富了m l 语言的类型系统，设 计出d m l ( d e p e n d e n tm l ) f 3 4 1 ；在命令式语言中，设计出一种带依赖类型 的类似c 语言语法的语言x a n a d u 3 5 1 。依赖类型和逻辑命题有很大的相似 性，比如一个函数的两个参数m ，n 都是n a t 类型，并且m = n ，写成依 赖类型就是m ：n a t ，几：n a t l m - - 礼1 。我们以如下例子解释依赖类型能 捕获更多的程序不变式，例女l l i s t 是类型构造符，那么( i n t ) l i s t ( n ) 代表长度 为n 的整数列表类型，贝l r i a ：n a t ( i n t ) l i s t ( a ) _ ( i n t ) l i s t ( a ) 描述了一个函 数接受长度为a 的整数表，并返回同样长度的整数表。依赖类型是类型细 化( r e f i n e m e n t ) 的一种方法，但是依赖类型不可以被滥用，因为新的类型 构造符和定型规则的加入会使类型系统变的复杂，造成类型系统的可靠 性3 6 1 变的不确定。 1 4 1类型化高级语言 最简单的类型化高级语言当属简单类型化入演算【9 ，2 0 】，它是一种函数 式编程语言。它的语法和项求值规则如图1 1 所示，a 演算包含了函数抽象 和函数应用。求值规则e a p p l 和b a p p 2 规定了先进行函数的归约，再进 行参数的归约；规则d a p p a b s 表明函数应用可以通过约束变量的替换进 行归约。 通过一组简单的定型规则可以确定一个a 项的良型性。定型规则如 图1 2 所示。定型规则t v a r 表明只有当变量x 出现在定型上下文r 中时，才 能确定x 的类型；定型规则t a b s 描述了如何为一个函数抽象a 项定型；定 型规则t a p p 描述了如何为函数应用) 、项定型。 这组定型规则是可靠的，可靠意味着，良型的项总能归约到值。可靠 性由如下两个定n p r o g r e s s 和p r e s e r v a t i o n 体现【1 9 】。 定理1 4 1 ( p r o g r e s s ) 一个良型的项要么是值，要么可以根据归约规则作一步归约。 6 背景介绍 图1 1 ：简单类型化a 演算的语法和操作语义 x ：t r r 卜x ：t r x ：t 1 卜t 2 ：t 2 fi - a x ：t 1 t 2 ：t 1 _ t 2 1 1 卜t l ：t 1 1 。t 1 2 ri - t 2 ：t l l r 卜t 1t 2 ：t 1 2 ( t v a r ) ( t a b s ) ( t a p p ) 图1 2 ：简单类型化a 演算的定型规则 7 1 4 类型系统 定理1 4 2 ( p r e s e r v a t i o n ) 如果一个良型的项能够作一步归约，则归 约后的项仍然是良型的。 定理1 4 2 表明良型入项的一步归约保持项的良型性，所以归约后的良 型项仍然可以继续归约到另个良型项，直到最后得到一个值。 1 4 2类型化汇编语言 类型化汇编语言t a l ( t y p e da s s e m b l yl a n g u a g e ) 【2 8 ，2 9 】作为编译器的 目标语言，它具有一般的r i s c 的指令集合，并且是强类型的命令式低级 语言。t a l 的类型系统非常标准，它支持元组，多态，存在包，和受限的 函数指针。一个类型保持的编译器可以从类似m lf 3 7 】的语言自动产生良 类型的t a l 代码。同时，t a l 还支持许多常规的低级优化，如全局寄存器 分配，公共子表达式删除等。由于类型安全能够保证一些安全属性如内 存安全，而不能保证其它的属性，如终止性，以及正确性相关的属性，所 以t a l 的类型表达能力是不够的。t a l 抽象的好处是可以自动构造出类型 安全的证明，所以t a l 比携带证明的代码p c c ( p r o o fc a r r y i n gc o d e ) f 3 s 简 洁；因为p c c 必须包含完整的证明。t a l 的研究主要包括两个部分，首先 为传统的汇编语言定义一个类型系统并且证明它的可靠性，然后设计一个 类型保持的编译器将a f 编译到t a l ，藉此证明t a l 的表现力。 t a l 的抽象机器状态包括堆( h ) ，寄存器文件( r ) ，以及一个指令序 列。堆是标签( 1 ) 到堆值( 元组或者代码块) 的映射。寄存器文件是寄存 器( r ) 到机器字的映射。t a l 的语法如图l 一3 所示： 和现实机器不同的是，t a l 的堆值是机器字的元组( t u p l e ) 或者一个 代码块。机器字或者是i n t e g e r ，或者为一个未初始化的垃圾值? 7 ，或者 为字值实例化类型变量丁后的结果叫h ，或者是一个存在包。从这里可以 看出t a l 的抽象层次比较高。t a l 的操作语义表示为一个确定的重写系 统p p 7 ，一般指令的操作语义比较容易给出，h 匕女a d d 从p 的寄存器文 件取源操作数寄存器的值，并使用目的寄存器到结果值的映射更新p 7 的寄 存器文件。u n p a c k 指令将存在包解开，以获取值v 中被抽象的类型7 - ，并使 用丁替换后续指令序列中出现类型变量q 。所以u 1 1 p a c k 指令的操作语义可以 写成： 8 背景介绍 图1 3 ：t a l 语法 ( h ，r ，u n p a c k q ，r d ，u ；，7 ) 一( h ，r r dh 伽】，7 【丁a ) w h e r er ( v ) = p a c k t ，w 】a s7 7 而j m p 指令跳转到的代码块的前条件类型是多态的，所以需要实例化目 的代码块，7 中的自由类型变元。它的操作语义可以写做： ( 日，r ，i m pu ) 一( 日，r ， 影司) w h e r ej f 2 ( 口) = z v a n dh ( 1 ) = c o d e a f ，7 从这里可以看出，t a l 的操作语义在擦除类型信息后就与真实机器非 常相近了。t a l 静态语义的作用是明确什么时候程序是良型的，并且保证 良型的程序不会中止，除非执行到h a l t 指令。p r o g r a m 的良型性由它的三 个部分，堆，寄存器文件，指令序列的良型性确定的。t a l 的静态语义包 括1 3 个良型性判断及相应的规则，这些良型性判断基于证明树的不同层 次，最上层是p r o g r a m 的良型性判断，然后是指令序列的良型性判断，堆与 寄存器的良型性判断，大小值的良型性判断，类型的良型性，堆类型的良 9 1 5 传统的携带证明的代码 型性以及类型和寄存器文件类型的子类型关系判断等。以j m p 指令为例子， 来看它的指令序列的良型性规则是如何的。 皿；r 卜t a lu ：v 】r 7 al - t a lr r 7 ， 皿；f 卜 t a li m pu 、7 这条规则的含义为目标代码块的类型为v 【】r 7 ，就是说这个代码块期待的 寄存器上下文类型为r 7 或者是它的子类型，由于r 是r 7 的子类型，那么在包 含更精确信息的寄存器上下文r 下，i m pu 是良型的。这条规则保证了当机 器的寄存器上下文是r 类型( 正是目标代码块所期待的) 时，跳转到u 是安全 的。 再来看u n p a c k 的静态语义，它的静态语义由下面的规则描述： 垩!二全主三：笔；!萎；_三t旦a兰l二unip竺a三c兰k_a三羔t!di笋i ( q 隹)( s u n p a c k ) ；r， 】，口； r7、 7 这个规则的含义是，u 是一个存在包，它抽象了，中的类型变量q ， 如果带类型变量的代码块是良型的( 在r d 为7 - 类型的情况下) ，那 么u n p a c k a ；r d l ，u ；，是良型的。这条规则保证了p r e s e r v a t i o n 属性，因为一 步执行后的指令序列也是良型的，即规则上部的第二个条件为真。从这个 规则可以看出，可以看做一个多态函数，对它的每次调用都需要实例化它 包含的类型变量q ，如果我们能证明，对任何的a 都是良型的，那么在调用 它的时