（计算机软件与理论专业论文）用于指针逻辑的自动定理证明器的设计与实现.pdf

摘要 摘要 对高可信软件需求的增加使得指针程序的验证成为近十几年的研究热点， 自动定理证明作为形式化方法之一，在软件验证和程序分析工具当中发挥着及 其重要的作用。然而，自动定理证明本身是一个非常难于解决的问题，尤其是待 解决的问题中存在着指针以及涉及到指针的递归定义的谓词的情况下。 考虑到以上问题，我们在一个出具证明编译器框架中设计并实现了一个自 动定理证明器和一个起辅助作用的证明检查器，来帮助完成指针程序的验证。 实验结果证明，我们的实现不但具有创新性而且具有实际可行性。 在本文中，我们首先介绍了项目的研究背景和理论基础，然后提出了一种为 指针逻辑来设计自动定理证明器的新技术，这项技术主要是基于变换和替代，我 们已经在一个被称为a p l 的工具中实现了该技术。指针逻辑作为h o a r e 逻辑的 扩展，可以对指针程序进行精确的分析。此外，本文还介绍了a p l 自动定理证 明器的详细设计和实现，描述了一些关键算法，比如指针逻辑决策过程，整型 线性算术决策过程，证明检查算法等等。a p l 定理证明器是完全自动的，并且a p l 所产生的证明可以被有效的记录和检查。在出具证明编译器p l c c2 中，我们调 用了a p l 自动定理证明器，并对一些具有代表性的程序进行了测试。实验结果 表明，a p l 完全可以自动地证明使用类c 语言编写的关于单链表，双链表和二叉 树的指针程序。 本文的主要特色和贡献为： 1 提出了一种为指针逻辑设计自动定理证明器的新方法。该方法是为了解 决基于指针信息集合表示的验证条件的证明问题而设计的。在实现时我们使用 了替代，变换，指针分析等基本技术，在指针信息集合上完成各种推理和证明。 并且我们使用这种方法为指针逻辑实现了一个完全自动的定理证明器。这在已 存在的比较流行的定理证明器中是不曾实现过的。 2 设计了指针逻辑的断言语言和相应的断言演算。该断言语言能够以简洁 易懂的形式描述指针逻辑的最显著的特点，主要使用指针信息集合的形式表示 待验证的指针程序在各程序点上的状态。断言语言和断言演算是定理证明器和 证明检查器设计和实现的基础。 3 设计了一个证明检查算法，并在一个证明检查器中实现了该算法。该算 法不同于已有的证明检查算法之处在于，它主要是使用模式匹配的方法对以指 针信息集合表示为主的证明进行快速有效的检查，来保证证明的正确性。 4 实现了一个用于指针逻辑的自动定理证明器。该实现主要包含指针逻辑 和整型线性算术两大理论的决策过程，独创的验证条件检查器，证明生成、保 存和检查模块等。可以完全自动地证明出具证明编译器p l c c 所产生的关于单链 表，双链表和二叉树等程序实例的验证条件。a p l 自动定理证明器的实现，使 得出具证明编译器p l c c2 不再需要依赖交互式证明工具c o q ，能证明更多的、 规模更大的程序实例，整个工具的功能因此变得更加强大。 关键词：软件安全程序验证指针程序指针逻辑验证条件自动定理证明 器证明检查器证明检查算法出具证明编译器p l c c a b s t r a c t - - - 一一一l a b s t r a c t t h ei n c r e a s i n gd e m a n d sf o rh i g h - a s s u r a n c es o f h v a r em a k et h ev e r i f i c a t i o no f p o i n t e rp r o g r a m sah o tr e s e a r c hp o i n to v e rt h ep a s tf e wy e a r s a u t o m a t e dt h e o r e m p r o v i n gi sam e t h o do ft h ef b 咖m e t h o d s ，a n di tp l a y sa u li m p o n a n tr o l ei nm a n y s o f t w a r ev e r i f i c a t i o na n dp r o g r a ma n a l y s i s t o o l s h o w e v e r ， a u t o m a t e dt 1 1 e o r e m p r o v i n gi sad i 街c u l tp r o b l e m ，p a r t i c u i a r i yi nt h ep r e s e n c eo fp o i n t e r sa n dr e c u r s i v e i y d e f i n e dp r e d i c a t e si n v o l v i n gp o i n t e r s t 萏k i n ga j lt h ep r o b i 锄sm e n t i o n e da b o v ei n t oa c c o u n t ，w eh 8 v ed e s i g n e da n d l i n p l e m e n t e da na u t o m a t e dt h e o r e mp r o v e ra n da na u x i l i a 巧p r o o fc h e c k e ri nt h e f r a m e w o r ko fac e r t i 匆i n gc o m p i l e r ， t h ep r o v e ra n dc h e c k c ra r eu s e dt 0 h e l p a c c o m p l i s h i n gt h ev e r i 6 c a t i o no fp r o g r a m s t h ee x p e r i m e n t a lr e s u l t ss h o w so u ，r i m p l e m e n t a t i o nn o to n l yn e wb u ta l s op r a c t i c a l i n t h i sp a p e r ，w ef i r s ti n t r o d u c et h er e s e a r c hb a c k g r o u n da n dt h e o 珂f o u n d a t i o n o ft i l ep r o j e c t t h e nw ep r e s e n tan e w t e c h n i q u ef o rd e s i g n i n gt h e o r c mp r o v e rw h i c h m a i n l yb a s e do nt r a n s f o n n a t i o na n ds u b s t i t u t i o nf o rp o i n t e rl o g i c ，a n dw eh a v e i m p l e m e n t e dt h i st e c h n i q u ei nat 0 0 1c a l j e da p l a sa ne x t e n s i o no fh o a r el o 西c ， p o i n t e rl o g i cc a nb eu s e df o r a c c u r a t ep o i n t e ra n a l y s i so fp o i n t e rp r o g m m s f u r t h e n n o r e ，t h i sp a p e ri n t r o d u c e ss o m ed e t a i l si nd e s i g n i n ga n di m p l e m e n t i n go ft h e a p la u t o m a t e dt h e o r e mp r o v e rf o rp o i n t e rl o g i c ，a n dd e s c r i b e ss o m e a l g o r i m m s f o r e x 锄p l e ，t h ed e c i s i o np r o c e d u r e sf b rp o i n t e rl o g i c ，t h ed e c i s i o np r o c e d u r e sf o rl i n e a r i n t e g e ra r i t h m e t i c ，t h ep r o o fc h e c k i n ga l g o r i t h ma n ds 0o n t h ea p l t h e o r e mp r o v e r i s 如l l ya u t o m a t e da n dp r o o f - sc a nb er e c o r d e da n dc h e c k e de m c i e n t l y w bi n v o k e dt h e a p l 也e o r e mp r o v e ri nt h ec e r t i 匆i n gc o m p i l e rp l c ca n dt e s t e ds o m er e p r e s e n t a t i v e p r o g r a m s t h ee x p e r i m e n t a lr e s u l t ss h o wo u ri m p l e m e n t a t i o nc a n 如l l ya u t o m a t i c a i i y p r o v et h ev e r i f l c a t i o nc o n d i t i o n sf o rp o i n t e rp r o g r a m si nc 1 i k el a n g u a g ea n dp r o d u c e m a c h i n e 。c h e c k a b l ep r o o f s t h ep r o g r a m sf o rt e s t i n ga r em a i n l ya b o u ts i n g l y 】j n k e d l i s t s ，d o u b l y 一1 i n k e dl i s t sa n db i n a 巧t r e e s t h em a i nc o n 仃i b u t i o n sa n df e a t u r e so ft h i st h e s i sa r e ： 1 i tp r c s e n t san e wm e t h o df o rd e s i g n i n ga u t o m a t e dt h e o r e mp r o v e r sf o rp o i n t e r l o g i c - t h i sm e t h o di sd e s i g n e df o rp r o v i n gt h ev e r i 6 c a t i o nc o n d i t i o n su s i n gp o i n t e r i n f o m a t i o ns e ta si t sb a s i cf o r m w h e ni m p i e m e n t i n g ，w eu s e ds o m e t e c h n i q u e s ，s u c h a ss u b s t i t u t e i o n ，t r a n s f o n n a t i o na n dp o i n t e r a n a l y s i s ，a n da c c o m p “s hr e a s o n i n ga n d m p r o v i n go nt h ep o i n t e ri n f o m a t i o ns e t w eh a v ei m p l e m e n t e da na u t o m a t e dt h e o r e m p r o v e ru s i n gt h i sm e t h o d ，a n dw e a r et h ef i r s tt 0d os o 2 i td e s i g n st h ea s s e r t i o n1 a n g u a g ea n da s s e r t i o nc a l c u l u sf o rp o i n t e rl o g i c t h e a s s e r t i o nl a n g u a g ec a nd e s c r i b et h em o s td i s t i n c tc h a r a c t e r so ft h ep o i n t e rl o g i ci na c o m p a c ta n dp e l l u c i d 、v a y t h el a n g u a g eu s e t h ep o i n t e ri n f o m a t i o ns e tt op r e s e n tt h e s t a t eo ft h ep r o g r a mb e i n gv e r i f i e do ne a c hp o i n t t h ea s s e r t i o nl a n g u a g ea n dt h e c o r r e s p o n d i n ga s s e r t i o nc a l c u l u sa r et h eb a s i sf o rd e s i g n i n ga n di m p l e m e n t i n gt h e p r o v e ra n dc h e c k e r 3 i td e s i g n sap r o o fc h e c k i n ga l g o r i t h m ，a n dh a si m p l e m e n t e dt h i sa l g o r i t h mi n ap r o o fc h e c k e r t h ed i f f e r e n c eb e t w e e nt h i sa l g o r i t h ma n do t h e re x i s t i n go n e si s ，i t u s ep a t t e mm a t c h i n gt of i n i s hp r o o fc h e c k i n ge f f c i e n t l yf o rt h ep r o o fu s i n gp o i n t e r i n f o m l a t i o ns e ta si t sm a i nf o m ，t 0a s s u r et h ec o r r e c t n e s so ft h ep r o o 4 i t i m p l e m e n t s a na u t o m a t e dt h e o r e mp r o v e rf o rp o i n t e rl o g i c t h e i m p l e m e n t a i o nm a i n l yc o n t a i n st h ed e c i s i o np r o c e d u r eo f p o i n t e rl o g i c ，t h ed e c i s i 0 9 p r o c e d u r eo f l i n e a ri n t e g e ra r i t h m e t i c ，au n i q u ev e r i 丘c a t i o nc o n d i t i o nc h e c k e r ，p r o o f g e n e r a t i o n ，p r o o fr e c o r d i n g ，a n dp r o o fc h e c k i n ga n ds oo n i tc a na u t o m a t i c a l l yp r o v e t h ev e r i f i c a t i o nc o n d i t i o n sg e n e r a t e db yt h ep l c cc e n i 母i n gc o m p l i e rf o rp r o g r a m s a b o u ts i n g l y l i n k e dl i s t ，d o u b l y - l i n k e dl i s ta n dt r e e s t h ei m p l e m e n t a t i o no fa p l t h e o r e mp r o v e rm a k e st h ep l c cn oi o n g e rn e e dt od e p e n do nt h ep r o o fa s s i s t a n tc o q ， a n dc a np r o o fm o r ec o m p i i c a t e dp r o g r a m s ；t h ec a p a b i i i t yo ft h ew h o l et 0 0 1h a sb e e n i m p r o v e d k e yw o r d s ：s o 厅w a r cs a f e t y ，p r o g r a mv e r i f i c a t i o n ，p o i n t e rp r o g r a m s ，p o i n t e rl o g i c ， y e r i f i c a t i o nc o n d i t i o n ，a u t o m a t e dt h e o r e mp r o v e r ，p r o o fc h e c k e r ，p r o o f c h e c k i n ga l g o r i t h m ，c e n i 矽i n gc o m p i l e rp l c c 中国科学技术大学学位论文原创性声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工作所取得的 成果。除己特别加以标注和致谢的地方外，论文中不包含任何他人已经发表或 撰写过的研究成果。与我一同工作的同志对本研究所做的贡献均已在论文中作 了明确的说明。 作者签名：签字日期：兰塑圭：壁 中国科学技术大学学位论文授权使用声明 作为申请学位的条件之一，学位论文著作权拥有者授权中国科学技术大学 拥有学位论文的部分使用权，即：学校有权按有关规定向国家有关部门或机构 送交论文的复印件和电子版，允许论文被查阅和借阅，可以将学位论文编入有 关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论 文。本人提交的电子文档的内容和纸质论文的内容相一致。 保密的学位论文在解密后也遵守此规定。 匦开口保密(年) 作者签名：至亟塑 签字日期：丝垡：查：兰星 新硌医盎雪 辩醐：芈 第l 章绪论 1 1背景研究 第1 章绪论 在众多的机器驱动的人类活动中，人们越来越关心软件的开发，测试，使用。 尤其是在那些对安全性，可靠性要求高的应用中，比如手机和电脑的操作系统， 航空航天设备，医疗设备，各类军事设备的控制系统，汽车的自动导航系统等等， 对软件的安全性要求就更加严格。尽管致力于开发规模更大也更复杂软件系统的 计算科学和软件工程在不断的进步发展，但是错误的、存在安全问题的软件随处 可见，并且这些软件有时会导致非常严重的问题和相当巨大的经济损失。因此， 通过使用形式化方法，为软件来设计可靠的、高效的形式化程序验证工具一直以 来就是一艰巨的任务。 软件的安全性( s a f e t y ) 主要指的是软件在运行的时候不会引起危险和灾难。 黑客通常就是利用数组越界访问，缓冲区溢出等安全性方面的错误来入侵和破坏 用户的系统的。另外一个容易混淆的软件的安全性( s e c u r i t y ) 概念则指的是对 数据信息的保密性，完整性，可用性，真实性提供保障的能力。我们所做的研究 主要是针对软件的s a f e t y ，因此后文中提到的软件安全性指的都是软件的 s a f e t y 。 我们的研究所关注的是通过使用形式化的方法，具体而言就是使用自动定理 证明器的方法来验证指针程序的安全性。在本节的其他小节中，我们将分别对一 些基本的概念，如形式化方法，指针程序验证，自动定理证明等做简单的介绍。 1 1 1 形式化方法 形式化方法( f o r m a lm e t h o d s ) 1 是计算机科学和软件工程领域中一种基于 数学的特殊技术，主要是用于软件和硬件系统的规范( s p e c i f i c a t i o n ) 、开发 ( d e v e l o p m e n t ) 和验证( v e r i f i c a t i o n ) 。在美国国家航空航天局( n a s a ) 的形式 化方法网站上，有一个对形式化方法的定义：“形式化方法 指的是用于软件和 硬件系统规范，设计和验证的数学严格( 眦t h e m a t i c a l l y “g o r o u s ) 的技术和工 具。“数学严格意味着形式化方法中所使用的规范是用某种数学逻辑书写的合 式语句( w e l 卜f o 瑚e ds t a t e m e n t s ) ，并且验证是使用该种逻辑所进行的严格的 推理。形式化方法的价值在于，它们提供了一种符号化检查一个设计( 硬件或者 软件) 的整个状态空间，对于所有可能的输入，确保其正确性或安全属性的方法 和手段。适当的使用形式化方法的好处是可以提高设计的可靠性和健壮性。然而 使用形式化方法所带来的代价也很高，所以，只有在开发对s a f e t y 和s e c u r i t y 有很高要求的高度集成的系统时，才使用形式化方法。 规范( s p e c i f i c a t i o n ) ，用于描述一个系统以及系统所具有的属性。规范本 身是一种语言，该语言具有数学定义的语法和语义。系统属性可以是函数的行为， 内部结构，安全策略等。使用规范，可以使得我们更深入的理解所描述的系统。 通过规范过程本身，还可以发现设计上的缺陷，不一致性，二义性和不完整性。 规范是一种在顾客与设计人员，设计人员与实现人员，实现人员与测试人员之间 沟通的有用工具。规范可以作为源代码的附加文档，但是是一种更高级别的描述。 验证( v e r i f i c a t i o n ) ，比规范更进了一步，用来分析一个系统是否满足所要 求的属性。模型检查( m o d e lc h e c k i n g ) 和定理证明( t h e o r e mp r o v i n g ) 是验 证领域中两种比较成熟的方法。模型检查技术为系统建立个有限模型，然后检 查所要求的属性在这个模型内能否成立。粗略来讲，该检查就是对状态空间的穷 尽搜索，搜索的过程能终止是因为模型是有限的。定理证明技术把系统和系统所 要求的属性表示成某种数学逻辑的公式。该数学逻辑由一组公理和一组推理规则 - 组成。定理证明就是通过公理和推理规则找出某个属性的证明的过程。 1 1 2 指针程序验证 指针程序验证是目前程序验证方领域中的一个热门研究方向。指针程序验证 通常要检查指针程序的安全属性包括：不存在段错误( s e g m e n t a t i o nf a u l t ) 和 内存泄漏( m e m o r y1 e a k ) 。当去访问一个已经释放的内存单元的时候就会发生段 错误，而当一个内存单元由于没有任何一个指针指向它而无法再被访问的时候就 发生了内存泄漏。如果一个软件在使用中存在段错误或者是内存泄漏，那么将导 致软件错误。当使用指针编程的时候，编程人员容易犯以下错误，比如：通过空 指针( n u l lp o i n t e r ) 或者悬空指针( d a n 9 1 i n gp o i n t e r ) 进行存取对象的操作， 或者把空指针或者悬空指针作为f r e e 函数调用的实参。而悬空指针引用 ( d e r e f e r e n c i n gd a n 9 1 i n gp o i n t e r ) ，以及内存泄露( m e m o r yl e a k ) 等潜在的缺 陷会对程序造成极大的安全性隐患。 指针程序验证，顾名思义，关心的是程序的规范的验证，而这里所提到的程 序的特点是显式使用指针。也正是由于程序中有了指针的存在，因此在验证指针 程序的时候，除了要用到程序验证方面的常规技术外，不可避免的要涉及到指针 分析( p o i n t e ra n a l y s i s ) ，别名分析( a l i a sa n a l y s i s ) 等和指针相关的分析 技术，以及特殊的指针程序验证技术。在指针程序的分析中，主要的难点是别名 ( a l i a s i n g ) ：两个语法结构不同的指针表达式可以指向相同的内存单元。 2 第1 章绪论 在指针分析，别名分析和指针程序验证方面有许多的研究工作。比如分离逻 辑( s e p a r a t i o n1 0 9 i c ) 2 ，3 ；形状分析( s h a p ea n a l y s i s ) 4 ，5 ；指针断言 逻辑( p o i n t e ra s s e r t i o n1 0 9 i c ) 6 ，7 。其中分离逻辑是对霍尔逻辑的扩展， 主要用于低级命令式语言程序的推理。分离逻辑主要特点是通过在断言中引入分 离合取( s e p a r a t i n gc o n j u n c t i o n ) 连接词和分离蕴含( s e p a r a t i n g i m p l i c a t i o n ) 实现局部推理；使用抽象数据结构上归纳定义的谓词来描述存在共 享的结构。而形状分析是一种静态程序分析技术，形态分析的目的是在每个程序 点可以对分配的数据结构的形态特征进行刻画，从本质上来讲，形态分析算法取 决于堆单元的属性集合。指针断言逻辑的方法使用指针断言逻辑表示的局部规范 来标注程序，程序和局部规范写成一元二阶逻辑公式( m o n a d i cs e c o n d o r d e r 1 0 9 i c ) 的形式，公式的有效性使用m o n a 工具来检查，该方法可以验证能够用图类 型( g r a p ht y p e s ) 8 来表示的数据结构，其缺点是经常需要显式地给出详细的循 环不变量，所以不能验证规模较大的程序。 基于已有的这些研究，我们的工作是使用指针逻辑的方法，在一个出具证明 编译器中验证指针程序的属性，该编译器以加了注释的指针程序作为输入，经过 编译器前端的验证条件产生器来产生待验证的逻辑公式( 即验证条件) ，而后， 这些验证条件作为自动定理证明器的输入，经过证明后，产生相应的证明，并返 回正确或者错误作为定理证明器的输出。如果定理证明器返回的是正确和相应的 证明，那么说明程序满足相应的安全规范，是正确的；如果定理证明器返回的是 错误并且不存在相应的证明，那么说明程序存在着错误和安全隐患。 1 1 3 定理证明器 定理证明器的使用者主要是计算机领域的专家，其应用主要包括硬件，软件 和协议的验证。按照自动的程度分类，定理证明器大致可以划分为：自动定理证 明器 9 ，半自动定理证明器，交互式定理证明器。其中，自动定理证明器是完 全自动的完成证明，不需要人工干预；半自动定理证明器有时需要人工给出提示 来完成证：交互式定理证明器则是完全是人机交互来完成证明过程。对于命题逻 辑( p r o p o s i t i o n a l1 0 9 i c ) 来说，可以为其设计完全自动的定理证明器；对于 一阶逻辑( f i r s t o r d e rl o g i c ) ，可以设计自动的定理证明器，但是不一定会终 止；对于高阶逻辑( h i g h e r o r d e rl o g i c ) ，有部分自动，但主要是交互地证明。 那么什么是定理证明器呢? 定理证明器本身是一个计算机程序，该程序可以 证明数学定理。那么为什么需要定理证明器呢? 理由可以概括为三个：第一，可 以彻底的分析系统程序；第二，提早发现设计和规范中的错误；第三，更高的 可靠性( 数学的，机器可检查的证明) 。目前，已知的定理证明器中经常采用的 技术有：一阶归结( f i r s t o r d e rr e s o l u t i o n ) ，项重写，模型消除，数学归纳 ( m a t h e m a t i c a li n d u c t i o n ) ，二元决策图( b i n a r yd e c i s i o nd i a g r 锄s ) ，合 一( u n i f i c a t i o n ) ，高阶合一等等。按照功能来划分的话，定理证明器的基本组 成大致可以分为词法分析，语法分析，语义分析，类型检查，美化打印，策略， 策略算子，量词消除，决策过程，证明搜索，证明产生，证明保存，异常处理， 错误信息处理，用户交互等模块。已有的比较著名的定理证明器，如n u p r l 1 0 ， i s a b e l l e 1 1 ，1 2 ，p v s 1 3 ，c o q 1 4 ，a c l 2 1 5 ，h o l 1 6 ，1 7 等等，历史悠 久，在领域内使用广泛。 h o l 系统是被设计用来使用高阶逻辑来进行交互式定理证明的( 所以才有首 字母缩写h o l ) 。为了实现这个目的，形式逻辑和一个通用目的编程语言接口，在 通用目的编程语言中逻辑的项和定理可以被表示，证明策略被表示并被应用，进 而逻辑理论就可以开发了。h o l 所使用的高阶逻辑的版本是带有类型化l a m b d a 演 算的项的谓词演算。这最初是开发用于数学基础的。开始，h o l 的主要应用领域 确定为用于硬件设计的规范和验证。尽管如此，这个逻辑并不限制对硬件的应用。 h o l 已经被应用于许多领域。h o l 使用的机械化形式证明方法应归功于r o b i n m i l n e r ，r o b i nm i l n e r 也带领团队设计和实现了m l 语言 1 8 。r o b i nm i l n e r 他们 的工作是围绕一个叫做l c f ( l o g i cf o rc o m p u t a b l ef u n c t i o n s ) 1 9 ，2 0 的系 统的。l c f 的目的是用来交互的自动推理高阶递归定义的函数。通过使用m l 的类 型结构，逻辑到元语言的接口成了显式的，这样做的目的是其他逻辑最终可以替 代最初的逻辑。h o l 系统是l c f 的直接的后代，这可以从它的结构以及它和m l 的结 合看出来，甚至是它的部分应用也可以看出来。所以，h o l 也满足最初的计划： 把l c f 方法应用于其他逻辑。最初的l c f 是在2 0 世纪7 0 年代早期在爱丁堡实现的， 所以现在被称为“e d i n b u r g hl c f 。它的代码被g 6 r a r dh u e t 从s t a n f o r dl i s p 移植为f r a n zl i s p ，并被用于一个法国研究项目“f o r m e l ，h u e t 的l c f 的f r a n z l i s p 版本在剑桥被l a r r yp a u l s o n 进一步的发展，变成了大家所知道的 “c a m b r i d g el c f ”。舯l 系统就是在“c a m b r i d g el c f ”的早期版本之上实现的， 最终爱丁堡和剑桥l c f 的许多特点被h o l 继承下来。比如，高阶逻辑的公理化就不 是经典的c h u r c h 的那个，而是l c f 影响下的一个相等的公式表示。语言m l 现在已 经变成了一个编程语言，经管它最初是被设计成为l c f 的证明管理语言。m l 是一 个函数式语言，并以它的类型推导机制著称，它的类型推导机制可以在不增加用 户负担的情况下保证类型安全。类型，尤其是抽象类型，是在安全可靠的方式下， 把一个逻辑的定理同其他的任意的公式区别开来的基础。现在已经为m l 建立了二 个标准，现在大多数的在p a u l s o n 的书中出现的剑桥l c f 版本都是基于这个 s t a n d a r dm l 。h o l 的最初版本包含m l 的一个m l 的初期版本，比如增强的合理化的 4 第1 章绪论 版本，h o l 8 8 。h o l 8 8 是在( 1 9 8 8 年发布的) 最初的h o l 系统使用了几年之后发布 的。在2 0 世纪9 0 年代初，h o l 9 0 ，基于s t a n d a r dm l 而不是l i s p 的h o l 实现被k o n r a d s 1 i n d 在卡尔加里大学完成了。使用s t a n d a r dm l 的h o l 的商业版本被i c l 安全系统 实现了，这个现在被称为p r o o f p o w e r 的系统，在安全性至关重要的领域中，是一 个用于商业验证工程的高度可靠的系统。 i s a b e l l e 是剑桥大学的l a w r e n c ec p a u l s o n 和慕尼黑科技大学的t o b i a s n i p k o w 合作开发的一个流行的通用定理证明环境。i s a b e l l e 是一个通用的证明 辅助工具，它允许用形式的语言来表示数学公式，并提供了工具用逻辑演算来证 明这些公式。i s a b e l l e 的主要应用是数学证明的形式化尤其是形式化验证，形 式化验证包括证明计算机硬件或软件的正确性和证明计算机语言和协议的属性。 和其他类似的工具相比，i s a b e l l e 的最显著的特色是它的灵活性。大多数的证 明辅助工具仅围绕一个单独的形式演算建立的，比如高阶逻辑。i s a b e l l e 有能 力接受许多的形式演算。i s a b e l l e 的已发布版本支持高阶逻辑，也支持公理化 的集合理论以及一些其他的形式，看i s a b e l l e 的逻辑部分可以知道更多的细节。 此外i s a b e l l e 是个开源的自由发布软件。i s a b e l l e 提供了出色的符号支持：使 用正规的数学符号可以引入新的概念，基于传统的证明风格，证明可以写成结构 化的符号，或者更直接的写成命令的序列。定义和证明可能包括t e x 的内容，通 过该内容i s a b e l l e 就可以自动的产生已排版的文档。i s a b e l l e 证明系统的主要 的局限性是：定理的证明需要用户是这方面的专家而且证明起来需要很大的努 力。i s a b e l l e 集成了一些其他的工具，通过把证明过程的某些部分自动化来提 高用户的生产率。特别的，i s a b e l l e 的经典的推理器可以执行一长串的推理步 骤来证明公式。简化器可以推理等式。线性算术是自动证明的。i s a b e l l e 提供 了一个很大的形式化验证过的数学定理库，包括初等数论( 例如，高斯定律) ， 集合论等。同时还提供了大量的研究过程中产生的实例。可以从两方面来看 i s a b e l l e ，一方面它可以作为一般的框架对演绎系统进行快速的原型设计：另一 方面，许多已存在的逻辑，如i s a b e l l e h o l 提供了一个定理证明环境用于大小 相当的应用。i s a b e l l e 的发行版本里包含大量的目标逻辑和其他的例子( 可以 参看i s a b e l l e 定理库) 。其中，i s a b e l l e h o l 是经典高阶逻辑的版本，它模拟 了h o l 系统的相应实现；i s a b e l l e h o l c f 是把用于可计算函数的s c o t t 逻辑加 入到了h o l 中；i s a b e l l e f o l 提供了基本的经典和直觉一阶逻辑，它是多态的； i s a b e l l e z f 在h o l 的顶端提供了z e r m e l o f r a e n k e l 集合论的公式表示。 i s a b e l l e h o l 是目前开发的最好的目标逻辑，包含了一个内容广泛的数学库和 各种各样的用于高级定义性概念的包，这样的概念如( 共) 归纳集合和类型，递归 等等。发行版本中也包含了一些大型的应用，比如加密协议( h o l a u t h ) 和通信 协议( h o l c f i o a ) 的正确性证明。 p v s 定理证明器提供了一系列的功能强大的基本的推理过程，这些过程可以 被用户交互的使用在一系列的演算框架中。基本的推理包括命题和量词规则，线 性算术的归纳，重写和决策过程。这些基本的推理的大的证明的实现被优化了。 例如，命题的简化使用了b d d s ，自动重写使用了c a c h e 来提高效率。用户自定 义的过程可以和这些基本的推理结合起来产生高级的证明策略。证明可以产生依 附于附加的公式的可编辑的脚本，然后在运行。这就允许许多相同的定理可以被 高效的证明。而且还允许证明被经济的调整以适应需求或设计的变化。有利于易 读的证明的开发。p v s 包含一个基于b 叻决策过程用于r e l a t i o n a lm u - c a l c u l u s ； 因此实验性的把定理证明和c t l 模型检查结合起来。p v s 使用g n u 或者xe m a c s 为它的规范语言和证明器提供一个集成的接口，命令可以使用下拉菜单选择或者 使用扩展的e i i l a c s 命令。并有大量的帮助，状态报告和浏览工具，而且还能使用 l a t e x 产生排版的规范，证明树和理论层次可以使用t c l t k 图形化的显示出来。 p v s 的主要目的是用于需求和设计层次的规范的形式化，以及复杂和困难问题的 分析。p v s 已经被用于容错的飞行控制系统的算法和体系结构，以及硬件与实时 系统设计中的问题。些涉及p v s 的合作项目正在与n a s a 和一些其他的航空公 司进行。应用包括一个用于航行器飞行控制的微处理器，容错的体系结构的诊断 和调度算法，航天飞机的飞行控制系统的部分需求规范。p v s 现在已经在北美， 欧洲和亚洲的数百个地方被安装。当前的工作主要是研究高度自动化的硬件验证 ( 包括模型检查器的集成) 和并行及实时系统的p v s 方法。 1 1 4 证明检查器 按照自动的程度来划分，证明检查器可以归为两类：一类是自动的，一类是 交互式的。下面我们提到的证明检查器，指的均为自动证明检查器。交互式的证 明检查器通常用于交互式定理证明系统，不是我们研究的重点。 对于用户来说，证明检查器是一个计算机程序，它读取一个证明文件，检查 文件中存储的证明，然后报告成功或者失败，如果返回的是成功，说明证明是正 确的，如果返回的是失败，则说明证明是错误的。证明检查器通常是一个自动的 证明检查过程，它不同于自动定理证明，它只是机械的检查已存在的证明是否正 确，而不是试着去发现新的证明或者定理，因此，证明检查器和定理证明器比较 起来，任务比后者简单很多，远远没有后者复杂。有一些证明检查器的核心代码 加起来甚至少于一千行。由于证明检查器以证明作为其处理的对象也就是输入， 因此它的实现很大程度上取决于输入的证明所采用的形式。比如，对于以类型信 息为主的证明，证明检查器的实现可能就是进行类型检查就可以了；而对于证明 6 第l 章绪论 是以一系列推导组成的情况，证明检查器则需要验证每一步推导是否正确。 设计并实现一个证明检查器，在程序验证中是至关重要的。这是因为使用定 理证明器产生出来的证明的规模通常都很巨大，很难人工地去检查证明的正确 性，而且有些时候，由于某些定理或验证条件的证明过大，用人力去验证有些不 切实际：此外，定理证明器的设计和实现通常都非常复杂，因此定理证明器本身 的正确性很难去验证，有了证明检查器，可以把证明检查器这部分的代码排除在 被信任计算基础( t c b ，t r u s t e dc o m p u t i n gb a s e ) 2 1 之外。其中，一个计算 机系统的t c b 指的是对其安全性至关重要的所有硬件，固件( f i r m w a r e ) ，和软件 组成的集合。软件安全所关注的就是如何减小系统的t c b ，t c b 越小，则系统的安 全性就越高。 1 1 5 模型检查 在过去的二十年中，模型检查 2 2 ，2 3 ，2 4 ，2 5 已经发展成为一种用于验 证有限状态系统的关键技术。模型检查通常被看做是一种程序验证方法，但是与 传统的基于仿真( s i 舢l a t i o n ) 、测试( t e s t i n g ) 和演绎( d e d u c t i o n ) 的验证 方法相比，模型检查在某些方面是很特殊的。首先，模型检查的目标并不是完全 通用的，最初，就被限制在只用于有限状态系统，尽管这个限制不是绝对的，模 型检查仍然是只用于那些状态有较短且易操纵的描述的系统。模型检查的第二个 特殊之处在于它是完全算法化的，计算复杂度很低。最初模型检查就被设计成自 动的机器实现，因此，它不需要程序员的干预，而且在检查一个属性失败的时候 可以提供显式的信息。最后，由于模型检查可以简单并重复的使用，因此即使是 对正在开发的系统的属性不是很熟悉的用户也可以用它来检查很多属性并得到 反馈信息。在模型检查的众多多优势里，值得一提的是，模型检查是自动的，并 在错误发生时能够提供反例( c o u n t e r e 船m p l e ) 。模型检查作为一种用于有限状 态并发系统的自动验证技术，可用于硬件，并发协议和进程控制系统等工业领域， 已取得了巨大的成功。 当使用模型检查方法验证一个系统时，需要为系统设计相应的模型化语言 ( m o d e