（计算机软件与理论专业论文）基于计算机辅助证明的安全性保证方法研究.pdf

信息工程大学硕士学位论文 摘要 随着计算机和网络的广泛应用，很多貌似安全和正确的协议或软件呈现出严重的安 全问题，这些问题来自设计和实现等多个方面。因此，迫切需要合适的、系统化的方法 来保证协议和软件的安全。本文深入研究了协议和软件的安全性保证方法，提出了基于 计算机辅助证明的研究方案，并对其可行性和有效性进行了理论和实验验证。本文所做 的工作如下： 对形式化方法和计算机辅助证明工具进行了较为全面的分析比较，指出了各自的优 点和局限性；选取了基于高阶逻辑的交互式辅助证明工具c o q 作为本文研究工作的平 台，在对c o q 的元语言归纳构造演算深入研究的基础上，剖析了c o q 的强大功能， 为基于c o q 开展安全性保证工作提供了理论依据和技术保证；深入分析了各种协议验证 方法，分别针对停止等待协议和0 t w a y r e e s 认证协议建立了形式化模型，对相关概念和 性质给出了形式化描述，并进行了严格的计算机辅助验证。验证结果表明停止等待协议 在设计上是正确无误的以及0 t w a y r e e s 认证协议存在类型缺陷；针对程序正确性问题， 本文通过对h o a r e 逻辑、程序提取等技术的研究，利用c o q 进行了大量的函数式和命令 式程序的验证，探索出了一条系统地进行程序安全性保证工作的方法。 文中的形式化和证明都经过严格的计算机验证，验证过程和结果表明，基于计算机 辅助证明可以系统、有效地开展协议和软件安全性保证工作。 关键字：安全性保证，机器辅助证明，c o q ，归纳构造演算，形式化方法，协议验证，程 序验证 第v i 页 信息工程大学硕士学位论文 a b s t r a c t a l o n g 谢t l lt l l ec o m p r c h e l l s i v ea p p l i c a t i o no fc o m p u t e 璐觚d 珊舸r km 雏yp m t o c o l s 锄d s o r w a r ew h i c hs e 锄t 0b es a f ea n dc o r r e c ts b d w r i o i l ss e c l l r i t yp r o b l 锄s t h e p r o b l e m sa b r o u g h td u r i l 玛t l l e i rp r o c e s so fd e s i g na n di m p l e m e n t s o m ep r o p c ra n ds y s t e m 砒i cm e t l l o d s a r _ en e e d e du r g n yt 0 蜘g t l l e ns u c hs e c 嘣够t 1 1 i s 曲部i s 百v 鄂ad e e pi 1 1 v e s t i g a t i o n0 nt 1 1 e m 幽d so f c u f i t y 觞s u r a n c e ，p f o p o sar e s o l u t i o np i a i lb a s e do nc o m p u t * 嬲s i s t e dp r o o f n e nw ee v a l l l a 惦i t sf e a s i b i l i t y 锄dv a l i d 时i nb o mt h e o r e t i c a la l l dp r a c t i c a lw a y s f i r s t l y ，t l l i st h e s i sm a k e sa na n a l y s i s 锄dc o m p a r i s o no ft h ec u 小m tf 0 姗a l 脒l 血o d s 锄d c o m p u t e r 弱s i s t e dp m o ft 0 0 l s ，p o i n t so u tt l l ea d v 锄t a g e s 锄dd i s a d v a m a g e ss 印锄t e l y t h e nw e c h o o s et l l ei i l d u c t i v ep r o o fa s s i s t a l l t c o qw i l i c hi sb 硒e do nh i g h e ro r d e rl o g i c 嬲t l l e p l a t f o mo fo l | rs m d y w ca i l a l y s et l l ep o w e 例f i l i l c t i o no fc o qb a s c do nm ei n 蛔) m i n v e s t i g a t i o no fc o q sm e t al 锄g i l a g e - c a l c u l 璐o fi n d u c t i v ec o n s 仃u c t i o 璐np r o v i d e st l l e t h e o r e t i c a lf o u n d a t i o na n dt e c h n i c a ls l l p p o nf o fc o qb a s e d 卵c u t ) ，a s s u m n c 已a 矗e f1 1 1 巩w e e s t a b l i s hd i f f b r e mf o m l a lm o d e l sf 研s t o p w a i tp r o t o c o l 船do t w a y r e e sa u t l l e n t i c a t i o np r o t o c o l ， f o 眦a l i z ct l i er e l a t i v cc o n c e p t s 觚dp r o p e r t i e s ，锄dm a k cas m c tc o m p u t e r - 硒s i 鼬c dp r o o f f o r b o t h o f t l l e m t h er ；c s u l ts h o w st l l a tt l l es t o p - w a i tp r o t o c o l i sf 撕l t l e s s 访d e s i g n 趾dt l l e r ei s 白，p en a w i no t w a y r e e sp r o t o c 0 1 a t l a s t ，t l l et 1 1 e s i sg i v e sa 咖d yo nh o a r el o g i c 粕dt e c l l r l o l o 西e ss u c h 硒 p r o g r a i ne x 订a c t i o nf o rv e r i f i c a t i o no f m ec o r r e c t n e s so f p m 黟锄s w ee x p l o r cas y s t e m a t i cw a y t 0o 虢rs e c 嘶t y 船s u 瑚c ef o rp r o g m m s 疆e rv c r i 聊n gm 锄y 劬c t i o i l a l 柚d i m p e r a t i v ep r o 鲫璐 b y c o q t h ef o m l a l i z a t i o i l s 柚d p r o o f sa r cv e r i f i e ds 岫c t l yb yc o m p u t e r _ a s s i s t e dp r o v 既n e p r o c e s s e sa n d r e s u l t so ft 1 1 e s ev c r i 五c a t i 0 船s h o wm a tm e t h o db 鹊e do nc o m p u t e r - 鹞s i s t e dp r o o f c 锄p r o v i d es e c 谢t y 嬲s u n a n c ef o rp r o t o c 0 1 sa n ds o f t w a r es y s t e m a t i c a l l y 锄de 仃e c t i v c l y k e yw o r d s ：s e c i l r i t y a s s u r a n c c ，c o m p u t * a s s i s t e dp r o v i i l g ，c o q ，c a l c u l i l so f i n d u c t i v e c o n s 仇l c t i o n ， f o n a lm e t h o d ， p f o t o c o lv e r i f l c “o n ， p r o g r 姗v e r i f i c a t i o n 第v i i 页 信息工程大学硕士学位论文 表l 辅助证明工具的比较 表目录 表2 直觉主义逻辑和古典逻辑的比较。1 l 表3 直觉主义命题逻辑的自然演绎风格表述 表4 简单类型n 演算的自然演绎风格表示1 4 表5 直觉主义命题逻辑与简单类型 演算的对应a 1 4 表6 直觉主义命题逻辑与简单类型 - 演算的对应b 1 5 表7c o q 8 o 之后版本的类型属性1 7 表9 安全协议安全性保证的形式化方法。3 3 第1 v 页 信息工程大学硕士学位论文 图l c i c 的类型结构 图2 c i c 的类型规则 图目录 图3 辅助推理系统的逻辑结构 图4 协议验证流程 图5 停止等待协议的i ，o 自动机模型 图6o 研a y r e e s 协议的示意图 图7 相同消息的两种理解 图8 程序提取示意图 图9w h y 的工作流程 图1 0c a d u c e 啪工作流程图 第v 页 博侈筋拍弱弘“铝 原创性声明 本人声明所提交的学位论文是本人在导师指导下进行的研究工作及取得的研究成果。 尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表和撰写 过的研究成果，也不包含为获得信息工程大学或其他教育机构的学位或证书而使用过的材 料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示谢 意。 学位论文题目：基i 土簟垫圭蔓塑堡塑塑窒全i ! 堡堡查基互塾 学位论文作者签名：三：! = 垒煎：日期：厶刁年7 月 日 作者指导教师签名： 。 乏蓥碰 日期：蜥7 月j日 学位论文版权使用授权书 本人完全了解信息工程大学有关保留、使用学位论文的规定。本人授权信息工程大学 可以保留并向国家有关部门或机构送交论文的复印件和电子文档，允许论文被查阅和借 阅；可以将学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或 扫描等复制手段保存、汇编学位论文。 ( 保密学位论文在解密后适用本授权书。) 学位论文题目：塞重主i 篝堑! 壹麴堡亟煎塞堡坚】垃主亟耷鱼 学位论文作者签名：二兰垒璺竭：日期：卿年7 月日 作者指导教师签名： z 笼建剐 日期：二门年7 月日 信息工程大学硕士学位论文 第一章绪论 本章首先介绍了课题的研究背景，接着在指出了非形式化方法不足的基础上，介绍 了基于计算机辅助证明的安全性保证方法，最后是本文的贡献和论文组织情况。 1 1 研究背景 计算机网络，特别是i m 锄c t 的出现和发展促进了计算机应用发生了质的变化，其应 用范围已远远超出了科学计算，成为无所不在的工具。现实世界中的各种组织和系统、 各种商务和交易在互联网这个虚拟世界中建立并迅速发展，不仅提高了人们的办公效率 和生活质量，还将人们对安全问题的关注程度提高到一个前所未有的高度。很多貌似安 全和正确的协议或程序呈现出严重的安全问题，这些问题来自设计和实现等多个方面。 因此，迫切需要合适的、系统化的方法来保证协议和软件的安全。 为此，本文基于某科学计划项目，对协议和程序的安全性保证方法展开研究工作。 1 2 研究现状 当一个协议或软件设计完毕，最初是使用非形式化的测试或仿真方法对其进行分 析，例如尝试已知的实际攻击方法进行测试，以检验协议或软件是否安全。但这类方法 存在两个明显的缺陷：一是非形式化方法无法系统而全面客观地进行严格的分析；二是 这类方法只能检测己知的攻击，对于许多未知的攻击无能为力。因此，一些被认为是安 全的协议或软件在设计使用很长一段时间后，却被发现存在严重的安全漏洞。 为了能够有效而全面、客观地进行分析，人们转向形式化方法的研究。简单来说， 形式化方法是一种用于描述系统性质的数学方法，它主要用于发现一个系统中的歧义 性、不一致性与不完备性。人们将协议或软件及其运行环境进行形式化描述，利用一定 的规则推理或者空间搜索对其进行严密而全面的分析和证明。经过形式化证明能够除去 原来系统说明中含糊和主观的成分。形式化证明可以人工完成，但最好还是使用辅助证 明工具。使用机器辅助证明有两个重要的原因：一是这些证明冗长但不够深入，所以计 算机程序适合接管部分工作。另一个原因是在冗长的证明中，大部分人都有可能出错， 计算机则可以面面俱到，能够发现那些被人们忽视的哪怕是很小的错误。于是机器辅助 证明技术越来越受到人们的重视。 计算机辅助证明是对“数学推理”的形式化，是利用计算机来形式化描述并证明定 理的技术和方法。它一方面提供形式化描述的形式语言，另一方面又提供证明定理的推 理工具，从而将一个包含公理、推理规则的推理系统抽象成一个符号系统，最终实现在 系统内以机械化的方式来构造定理的证明【1 1 。借助于计算机，让它帮助我们进行许多高级 推理工作，从而避免手工证明导致的一些低级的错误，提高安全性保证工作的可靠性， 同时使人们从繁重的推理工作中解放出来，而专注于富于创造性的工作，由人工来完成 第l 页 信息工程大学硕士学位论文 智能型的工作。 如今人们不仅可以利用它来证明许多数学领域的定理，而且开始把它应用于协议验 证、程序验证等新领域。其驱动力来自两个方面【2 j ： 1 计算机和网络的高速发展，使各种软、硬件和协议等变得越来越复杂，传统的安 全性保证方法越来越难以胜任； 2 一些新的理论研究成果及其实际应用使得计算机辅助证明的技术和方法越来越显 示出实用价值。 目前，欧美等发达国家已将这些方法和技术投入工业应用，将其应用到航空航天、 银行、电信、核电站等对安全性要求比较高的部门，有效地提高了这些部门相关系统的 安全性，产生了非常好的效果。 国内在这一领域的研究起步虽然晚，但也取得了丰硕的成果。例如吴文俊院士所带 领的科研组，已经在几何机器定理证明领域做出了突出的成鲥3 1 。中科院、清华大学、中 国科技大学、国防科技大学等多家院校都有相关课题组在开展这方面的研究。如国防科 技大学正在开展基于构件的高可信系统形式验证研究、微处理器高层功能验证测试 程序自动生成的理论与方法、h i 砌ds y s t e m s 的形式规范和验证技术等自然科学 基金和8 6 3 计划项目。李梦君、李舟军等基于0 b j e c tc a m l 设计并实现了安全协议验证工 具原型s p v 4 1 。兰州大学李廉教授带领的课题组对使用多种计算机辅助工具开展对硬 件、并行系统等的验证工作。 1 3 本文的贡献 本文主要贡献如下； 1 在深入研究了协议和软件的安全性保证方法的基础上，提出了基于计算机辅助证 明的技术和方法可以系统、有效地提供安全性保证的观点，并对该观点的可行性 和有效性进行了理论和实验验证； 2 对形式化方法和计算机辅助证明工具进行了较为全面的分析比较，这样不仅有利 于全面总结各种安全性保证方法，更有利于揭示安全性保证工作的研究方向，为 进一步的研究提出新的思路； 3 提出了规格说明一建立模型一形式化一提取属性一计算机辅助证明的系统化的协 议安全性保证方法。利用此方法证明了停止等待协议的正确性和o t w a y r e e s 安 全认证协议存在类型漏洞，证明了此方法还具有发现漏洞的能力； 4 针对程序正确性问题，结合h o a r e 逻辑，利用c o q 进行了大量的函数式和命令式 程序的验证，探索出了一条系统地进行程序安全性保证工作的方法。提出程序提 取机制可以作为一种开发安全程序的方法的观点，在对程序提取机制进行了深入 研究的基础上，通过实例证明了这一观点。从而证明了基于计算机辅助证明的方 法可以有效地开展程序的安全性保证工作； 第2 页 信息工程大学硕士学位论文 5 已将形式化描述和证明过的安全属性提取为相应的程序模块加入到课题的原型系 统s p a l d e r 中，这些包可以被应用到今后的安全性保证工作当中，减少对 相同属性的重复提取工作，提高工作效率。 1 4 本文的组织结构 本文后续章节安排如下： 第二章是对形式化方法和计算机辅助证明工具较全面的分析和比较，指出了形式化 方法的好处和不足，以及对辅助证明工具的比较结果。为基于计算机辅助证明的安全性 保证工作中形式化方法和辅助证明工具的选取提供了参考标准； 第三章深入研究了c o q 系统的元语言归纳构造演算，在此基础上分析了c o q 的 强大功能，为基于c o q 系统开展安全性保证工作提供了理论依据和技术保证： 第四章分为两个部分，第一部分针对网络协议，剖析了网络协议的安全性保证问题 的提出和相关工作。提出了基于c o q 的系统化的辅助证明步骤，对停止等待协议进行了 形式化和计算机辅助证明，给出了验证过程和结果：第二部分针对安全协议，剖析了安 全协议的安全性保证问题的提出和相关工作，对o 觚a y r e e s 认证协议的安全缺陷攻击过 程进行了形式化和计算机辅助证明，给出了验证过程和结果； 第五章研究程序的安全性保证问题。简要介绍了程序安全性保证的发展情况，对主 流的安全性保证方法进行了分类和比较。阐述了如何使用c o q 对命令式语言和函数式语 言进行验证，结合实例给出了验证过程和结果。对程序提取技术进行了深入研究，通过 实例分析指出程序提取机制可以作为一种开发安全程序的方法。 最后是结束语，对全文进行了总结，指出了目前在研究中还存在的一些问题和不 足，并给出了下一步可能的研究课题和相应的一些设想。 第3 页 信息工程大学硕士学位论文 第二章形式化方法和辅助证明工具的研究 形式化方法和辅助证明工具是计算机辅助证明技术的基础，本章主要对形式化方法 和辅助证明工具进行分析和比较，给出了比较结果。为基于计算机辅助证明的安全性保 证工作中形式化方法和辅助证明工具的选取提供了参考标准，是本文研究工作的基础。 2 1 形式化方法 计算机系统本身，它的硬件、软件都可描述为一种形式系统，程序设计语言更是不 折不扣的形式语言系统。要研究计算机、开发种种程序设计语言，没有形式化方面的知 识和能力是难以取得出色成果的。另一方面，应用计算机求解实际问题，首要的任务便 是形式化。离开对问题正确的形式化描述，没有理性的机器是无法理解和解答这些问题 的。人们必须用计算机懂得的形式语言告诉它“做什么”和“怎么做”，而计算机理解这 些语言的过程，又正是按照人赋予它的形式化规程，将它们归约为自己的基本操作1 5 j 。 2 0 世纪6 0 年代后期，针对当时所谓“软件危机”，人们提出种种解决方法，归纳起 来有两类：一是采用工程方法来组织、管理软件的开发过程；二是深入探讨程序和程序 开发过程的规律，建立严密的理论来指导软件开发实践。前者促使了“软件工程”的出 现和发展，后者则推动了对形式化方法的深入研究【6 ”。 形式化方法可以分为形式化描述方法和形式化验证方法两大类。形式化描述是基 础，形式化验证是目的。 2 1 1 形式化描述 形式化描述方法是指在描述、设计和构建计算机系统和软件的过程中所使用的基于 形式逻辑和离散数学的方法和技术【8 】。它是对“做什么”的数学描述，是用具有精确语义 的形式语言书写的功能描述，是设计和编制协议和软件的出发点，也是验证协议和软件 是否正确的依据。 形式化描述一方面是对系统或程序的描述，另一方面是对性质的描述。经过长期的 发展，已经产生了大量的形式化描述方法。如：有限状态机、进程代数、n 演算、1 1 演 算、特殊的程序语言以及程序语言的子集等。这些形式化描述方法可以根据其基于的数 学理论被划分为两类：基于集合论的方法和基于类型论的方法。 1 基于集合论的方法 集合论是数学的基础，其基本知识己被运用于数学各个领域。集合论从集合的直观 概念出发，研究集合的运算、序数、各种集合的性质，并用集合定义各种数学对象，使 得全部顺序都可以在该理论范围展开。集合论的概念、性质和方法不仅是数学中大多数 分支的基础，而且作为离散结构的一个有力描述工具已被广泛应用到计算机科学、逻辑 学、信息科学、运筹学等多个现代科学领域中。由于集合论的语言适合于描述和研究离 第4 页 信息工程大学硕士学位论文 散对象及其关系，所以它也是计算机科学与工程的理论基础。它在程序设计、形式语 言、关系数据库、操作系统等计算机学科中都有重要的应用。基于集合论的方法有很多 已经比较有名，比如z 方法、b 方法等。 z 方法以经典集合论和一阶逻辑为基础，提供了一种称为模式的结构，以此来描述一 个规格说明的状态空间和操作。z 规格说明由一系列模式组成每个模式定义一个抽象对 象或操作，并用谓词判定描述给出新的对象或操作的语义约束。z 模式说明可以组合成新 的z 模式新的z 模式继承其成分模式的一切属性和约束。这样，软件系统的z 模式规 格说明可以按一定的层次结构给出。模式的使用为规格说明提供了一种演算通过这种 演算，无论多么大型系统的规格说明都可以通过一个个小的部分来构成。这是一种很有 集合论特色的有效的形式化方法m o 】。 b 方法建立在z e n n e l o f r a l l l 【e l 集合论的基础上，它包含种从规格说明到精化再到 实现的结构化机制。它使用一种精确的方法来描述软件系统的需求和设计。这种描述方 法称为a m n ( a b s t r a c tm a c h i n cn o t a t i o n ) 。a m n 是基于状态的归约和设计语言，通过广 义代换语言g s l ( g e n e r a l i s e ds u b s t i t u t i o nl a n g i l a g e ) 提供其形式语义。b 方法有很多优 点，比如：使用比较简单、模块化以及有大量的工具支持等【i o 】。 2 基于类型论的方法 类型论源于罗素为避免朴素集合论的悖论而引入的“分类”思想。后来人们发现了 很多它在计算机科学方面的应用，它比集合论更符合计算机的表示，尤其是c 唧 h o 靴耐同构理论的出现和发展，使人们认识到类型论可以为计算机科学中的计算和推理 这两种基本概念提供统一的处理方法。人们可以在个形式框架下同时完成编程、理解 和推理三项任务。此外，类型论还提供一种很好的抽象机制同时支持规范的开发、程序 的编写和证明的构造。因此，它可以消除程序设计语言和程序规范语言之间的差距【l 。 而且，大部分基于类型论的形式化描述方法都支持高阶逻辑，其功能更强大。因此，类 型论相比集合论，在支持计算机辅助推理，形式化数学和程序验证等领域更有前途。 基于类型论的方法比较著名的是m 枷n 1 醒直觉主义类型论【1 2 】。 m a n i n 1 6 f 直觉主义类型论最初的目标是为构造数学提供个形式系统，但它对计算 机科学领域的作用很快显现出来。从直觉主义的观点来看，定义一个构造集合理论完全 等同于定义一个逻辑演算或是一个用于求解问题的规范语言。一个集合中有元素相当于 一个命题有证明或是一个问题有求解它的程序。m a n i n 1 计直觉主义类型论也是一个函数 性编程语言，它拥有丰富的类型结构并能从规范中获取正确的程序。 本文所采用的归纳构造演算也是基于类型论的，关于归纳构造演算的内容将在第三 章详细介绍。 2 1 2 形式化验证 形式验证是指在已做出的形式化描述的基础上使用严格的数学方法来推理验证设计 第5 页 信息工程大学硕士学位论文 或实现是否符合其全部或部分规范。利用基于计算机的形式化验证工具，验证过程能在 一定程度上自动地完成，在这方面有三个较为成功的技术，它们分别是定理证明技术与 模型检测技术和类型检测技术。 1 定理证明技术 定理证明技术将系统及其特性使用某种数学逻辑进行表达。描述这个系统的逻辑系 统包括一个公理集合与一个推理规则集合。证明的过程就是从系统的公理出发，依据推 理规则或是某些定义以及中间引理来推导有关的系统性质。证明所需要的步骤依赖于系 统的公理和推理规则，在某种程度上也依赖于其派生定义和中间引理【1 3 1 。定理证明的优 点在于可以使用类似于结构化的推导过程来证明具有无限状态的系统；缺点是由于大多 数定理证明系统是交互式的，因此其自动化程度较低。 2 模型检测技术 模型检测技术利用有限状态机为系统建立模型，在此基础上检测该模型是否具备应 有的性质。检测的过程实质上是一个穷尽搜索状态空间的过程，以此来判断一些特殊的 状态是否可达，或者是否可以生成一条特殊的状态转移路径。其优点是定义好状态集合 和转移函数集合，验证过程可以自动进行；缺点是由于模型检测技术只能应用于有限状 态系统，限制了它可以检测的系统的规模。 3 类型检测技术 类型检测技术可以说是最新的用于安全性的辅助推理技术。在类型检测技术中，消 息与信道都被赋予不同的类型，那么存在安全缺陷就等价于出现类型不匹配。其优点是 类型机制的严格性保证了被验证对象一经验证，就具有非常高的可靠性；缺点是类型机 制过于苛刻，限制了它的灵活性。 2 1 3 形式化方法的优点 好的形式化方法起到的作用是多方面的【1 4 】。 首先是更精确、严密。现有的描述方法一般是非形式化的，例如自然语言，一个词 可以表达多种不同的意思，并且一个意思也可以用几个不同的词来表达，因此表达的语 义不明确。形式化描述以逻辑精确性为特色，除去了在非形式化描述中不可避免的含糊 不清的描述，这种精确性为开发人员与用户对需求的一致性理解，及需求的正确执行提 供了更大的可能性。 其次是易于机器实现。形式化方法建立在严格的逻辑和数学基础之上，它所基于的 数学模型非常适合模拟离散系统，例如计算机。许多工作都能部分自动或半自动地完 成，对于一些简单的系统，形式化的描述有可能直接转换成可执行程序，这可以简化手 工劳动、降低分析方面的费用、节约资源和减少出错的可能性。 另外，形式化方法可以用于程序的验证，以保证程序的正确性。形式化方法可用于 测试用例的自动生成，这可以节约许多时闻并在一定程度上保证测试用例的覆盖率。 第6 页 信息工程大学硕士学位论文 2 1 4 形式化方法的局限性 形式化方法能非常有效地提高安全性和可靠性，但完全的安全是不可能的。它主要 有两个基本的局耐1 4 】： 1 形式化描述可能是不完备的或是错误的 书写形式化说明要求专心致志，否则形式化说明中可能存在未发现的错误，或者存 在对正确描述的需求的错误解释或形式化，不过目前有些系统可以通过类型检查部分地 解决这方面的问题。 2 证明也可能含有错误 形式化方法的主要手段是利用各种数学理论的证明程序来辅助证明研究对象达到了 设计的目的，但是却难以保证这些证明程序本身的正确性，即使这些程序是正确的，也 不能完全保证运行这些程序的硬件的正确性。 我们不能完全保证设计的正确性，只能利用计算机辅助证明技术的严格性进一步发 现设计错误以增强正确性，堵塞可能的漏洞。因此，辅助证明工具的选取就显得十分重 要。 2 2 辅助证明工具 为了在逻辑系统中有效地实现推理，出现了多种证明方法，如自然推理、序列演 算、归结原理等。相应地也出现了多种多样的机器辅助证明系统。它们有各自的特点和 应用领域。对于辅助证明工具的选择必须针对应用领域，发挥它们的特长。这些形式化 方法工具不仅支持初始开发和说明分析，而且减少了随后修改和扩展时再分析所需的时 间。 2 2 1 辅助证明工具研究 典型的辅助证明工具有三个主要部分：逻辑系统、规范描述语言和辅助证明的计算 机程序。 1 逻辑系统 逻辑是辅助证明工具的理论基础，此处的逻辑主要是指古典或直觉主义命题逻辑和 谓词逻辑，还有非经典的各种时态逻辑等。许多辅助证明系统都采用较少的原语作为自 己的逻辑基础，然后再在这个基础上进行扩展，这样可以保持逻辑的严谨和一致性。当 谓词逻辑中加入了全称量词、存在量词、变量、谓词和将这些组成公式的法则时，就成 为一阶逻辑。当量词所约束的变元可以是函数变量和谓词变量时，就称为高阶逻辑。 2 规范描述语言 辅助证明工具的规范描述语言是辅助证明工具用来表达其逻辑的语言。规范描述语 言也被称为系统的目标语言。这种语言大多使用基于集合论或类型论的概念和传统的带 有量词的一阶逻辑的符号系统。 第7 页 信息工程大学硕士学位论文 3 辅助证明的计算机程序 在理想情况下，人们利用规范描述语言表示设想的定理，并输入到辅助证明工具， 辅助证明工具将会决定它是正确的还是错误的，并且给出每一步的证明过程。 辅助证明工具可以按照所采用的逻辑、自动化程度、规模和应用领域等进行分类。 根据自动化程度可以分为交互式和自动式。事实上，辅助证明工具还远没有达到完全自 动的程度。对于许多问题的证明还需要人为的干预，引导其一步步地完成证明。因此大 部分辅助证明工具是交互式的，由用户和机器合作，机器完成那些繁杂的工作，人们用 自己的经验和智慧指导机器进行工作。于是一个辅助证明工具必须具备自动保存和搜索 定义、公理、定理、推理规则的程序以及辅助证明过程的各种实用程序。多数系统提供 各种证明策略供用户选择，不同的证明策略能解决的目标的大小和难度各不相同，策略 的证明能力决定了系统的自动化程度。 2 2 26 种辅助证明工具的比较 上文已经论述了基于类型论的形式化方法在支持计算机辅助推理，形式化数学和程 序验证等领域更有前途，因此，本文选取了六种当前比较流行的基于类型论的辅助证明 工具，它们分别是法国的c o q 、英国的l e g o 、i s a b c l k 、h o l ，以及美国n u p r l 和p v s ， 经过多年的不断研究和完善，这些工具己经被成功应用到软、硬件的形式化验证、协议 验证、嵌入式系统的验证等，但由于侧重点不同，其功能也不尽相同。下面分别对这6 个系统进行一下分析和比较： 1 c o q c o q 是法国国家计算机科学与自动控制研究所( 烈r j a ) 研制的基于高阶逻辑的辅助 证明系统，通过它，我们可以定义函数或谓词；声明数学定理和形式化规范；交互式地 构造证明并检查证明是否正确等，目前它已经在数学定理证明、协议验证、程序验证等 许多领域得到应用。在信息安全性质的证明方面具有很好的应用前景。2 0 0 5 年4 月，美 国科学家就用这一工具证明了上个世纪七十年代提出的对四色定理的证明是严谨而正确 的【1 6 1 。 2 l e g o 英国爱丁堡大学研制的l e g o 是一个基于类型理论的系统，它能够提供构造性的证明 帮助。英国达勒姆大学研制的p l a s t i c 系统是一个基于类型理论框架l f 的系统，它更强调 子类型化( s u b t y p i n g ) 和强制( c o e r c i o n ) 的实现，以上两个系统都有很强的信息安全领 域应用潜力i l ”。 3 i s a b e l l e 由英国剑桥大学和德国慕尼黑大学联合研制的i s a b e l l e 系统提供了一个逻辑理论框 架，在此框架下可以定义并且实现很多不同的理论和系统。目前，它已被应用于数学形 式化、逻辑研究、计算机软硬件以及安全协议的验证等多个领域。i s a b e l l e 包含许多有重 第8 页 信息工程大学硕士学位论文 要参考价值的证明信息，例如含有证明方法的证明步骤，反映当前证明形式和效果的证 明状态。这些信息都有助于用户开发新的证明文档【l ”。 4 h o l h o l 是由剑桥大学开发的，基于l c f 体系结构( l 0 画cf o rc o m p u t a b l ef l l n c t i o n ) 的 高阶定理证明系统。h o l 通过元语言m l ( m e 诅- l a n g i l a g e ) 与用户交互，由用户选择推理 规则，h o l 应用这些规则。h o l 内置5 个公理和8 条最基本的推理规则。每一步的证明 步骤都是由用户选择推理规则。凭借m l 内置的策略，h o l 能够实现各种反向推理。基 于这些优点并凭借高阶逻辑强大的逻辑表达能力，h o l 成为验证复杂系统的有力工具。 h o l 系统自从1 9 8 4 年至今，已经不断地改进，先后出现了h o l 8 8 ，h o l 9 0 ，h o l l i g h t ，h o lk a n a n a s h s1 ，h o lk a l l a i l a k i s2 等版本。其应用极为广泛，已经验证了多种 硬件电路的通讯协议，包括英国的军用微处理器p e r 和其它各种微处理器。在世界上已 经形成了一个庞大的h o l 用户群。应当说h o l 系统是最成熟的用于硬件验证的定理证 明器之一【1 9 1 。 5 n u p r l n u p d 是美国c o m e l l 大学研制的一个为问题求解提供计算机支持的系统。n u p d 包含 一种程序设计语言，更精确地说，那是一个实现数学的系统。一个重要的特征是它是基 于构造性逻辑的系统，因此断言和证明的计算意义更加明显，这就为计算机提供辅助推 理提供了理论上的支持。也为系统安全性质的形式化证明提供了理论支持，在此系统中 如果引入的公理没有问题，就不可能给出错误的证明。当用户使用n u p d 时，他们需要建 立事实，定义和定理库，同时他们也可以创建m l 程序库，从而产生新的定理的证明。 目前在数学领域已经有很多n u p r l 的应用【2 0 】。 6 p v s 美国斯坦福研究所s i u 研制的p v s ( p r o t o t y p ev e = r i f i c a t i o ns y s t e m ) 系统，为形式规范和 验证提供了计算机辅助支持，它包括一种基于古典高阶逻辑的规范语言，一组预定义的 理论，一个定理证明器，以及一些应用实例。p v s 的应用包括自动的硬件验证，容错和 实时系统的安全保障等，一些公开的涉及军事方面的应用主要集中在航天飞机的飞行控 制等领域。它在信息安全和攻击方面的应用的潜力很大【2 lj 。 当然，辅助证明工具远远不止以上6 种，它们被应用于不同的领域，发挥着不同的 作用，我们很难评价它们的高低优劣，只能针对我们的需要进行选择。n 日m e g e n 大学的 w i c d i i k 曾经做过这方面的比较，他联系了1 7 种辅助证明系统的开发人员，让他们都对 “2 是无理数”这一命题进行证明，根据对方反馈的结果，他对这1 7 种辅助证明系统 进行了多方面进行比较。本文是对安全性保证方法的研究，在辅助证明工具的选择上， 我们关注的是系统的逻辑一致性、描述能力、推理能力等。 对上述6 种辅助证明工具进行了比较，结果显示在表l 中。 综合比较之后，我们选择了c o q 系统作为我们的辅助证明工具。对构造逻辑的支持 第9 页 信息工程大学硕士学位论文 以及非常小的内核程序都保证了它的在逻辑上的一致性与严格性，高阶类型理论和强大 的标准库使其具有很强的描述能力，良好的可扩展性方便我们在其上定制感兴趣的内 容，提高工作效率。 表l 辅助证明工具的比较 对构造逻核心证用户可系统提供 逻辑基础 辑的支持明程序扩展性的标准库 c 0 q高阶类型理论支持 小好大 妇 高阶逻辑支持小差小 h o l 高阶逻辑不支持小好大 i s a b e l l e 高阶逻辑不支持小好大 n u p r l 高阶类型理论支持大中大 p v s 高阶逻辑不支持 大中大 2 3 结论 本章对形式化方法和辅助证明工具进行了研究，它们是计算机辅助证明的基础，通 过分析和比较，确定了c o q 作为我们研究工作的辅助证明工具。 第l o 页 信息工程大学硕士学位论文 第三章c o q 的元语言与功能分析 c o q 的功能是由它的元语言( m e t al a i l g u a g e ) 归纳构造演算( c i c ) 决定的。本 章在对归纳构造演算深入研究的基础上，剖析了c o q 的强大功能，为基于c o q 系统开展 安全性保证工作提供了理论依据和技术保证。 3 1 理论背景 归纳构造演算的出现是数学、逻辑学以及计算机科学等多个领域发展交织的结果。 为了更好地理解它，我们从直觉主义逻辑谈起。 3 1 1 直觉主义逻辑 逻辑是理论计算机科学十分重要的基础之一，而其中又以直觉主义逻辑对计算机科 学的影响最为显著，它的思想比古典逻辑更加切合计算的观点口2 ，矧。直觉主义逻辑，创始 人是布劳威尔。在这一派学者的主张中，最重要的观点之一是反对排中律。例如，他们 认为像“pv 廿”之类的公式不能承认为永真。与此同时，他们主张对任何数学定理的证 明必须是构造性的，否则就不能承认。 所谓构造性是指：与古典逻辑只关心公式的真值不同，构造性逻辑关注的是实际的 证明对象本身，能具体地给出某一对象或者能给出某一对象的计算方法。即当我们把能 证实“存在一个x 满足性质a ”的证明称为构造性的，是指能从这个证明中具体地给出满 足性质a 的一个z ；或者能从此证明中得到一个机械的方法，使其经有限步骤后即能确定 满足性质a 的这个工来阱】。 表2 直觉主义逻辑和古典逻辑的比较 经典逻辑直觉主义逻辑 语义t a b k i 语义b m u w 盯- h e y t i n g - k o l m o g o 刚直觉解释 语 义 命题的定义就是把该命题的证明写下来。只 命题解释命题为真或者为假有存在命题的证明对象，命题才为真命 基 题的“真”等价于命题的“可证明性” 础 语义模式模型论证明论 - 1 是原子逻辑运算符，卅是原 _ 1 不是原子逻辑运算符，卅不是原子公 - 1 的原子性 子公式式，用彳j 上表示 排中律4 v 叫是重言式不接受排中律彳v “ 一( 1 a 1 口) j ( 4 v 口) 不接受，“j 4 排中律 ，v x ? ，p ( x ) = ，血尸( x ) - 1 ( 以 1 曰) j 4 v 曰 _ 1 4 ：，4 是重言式 ，v x p ( jj x 尸( x ) 第l l 页 信息工程大学硕士学位论文 3 1 1 1 直觉主义逻辑和经典逻辑的区别 具体地说，直觉主义逻辑和经典逻辑在以下几个方面有着显著的不同。 1 语义基础不同； 2 一不是原子运算符 3 不接受排中律 错误l 未找到引用源。【2 5 1 给出了直觉主义逻辑与经典逻辑的不同之处： 3 1 1 2 直觉主义逻辑的语法表示 直觉主义命题逻辑的语法可以被归纳定义为： 矿：= 上i 尸矿i ( 矿一矽) i ( 矿v ) i ( ) ( 1 ) 其中，p 矿表示任意的命题变元( p r o p o s i t i o n a lv a r i a b l e s ) ，其上的操作包括蕴含、析取、 合取以及取非操作。 接下来我们采用自然演绎风格对直觉主义逻辑进行形式化。 3 1 1 3 直觉主义命题逻辑的自然演绎风格表述 表3 给出了直觉主义逻辑的自然演绎风格的表述： 表3 直觉主义命题逻辑的自然演绎风格表述 公理规则 而( 触) 合取的引入规则 船( r 卜a b 、7 合取的消除规则 等r 卜a 半c 卜- b 、 析取的引入规则 r 卜a v b 志r 卜- a v b 、7 析取的消除规则 叶b 等；，卧c ( v e ) r 卜c 、 蕴含的引入规则 r 卜- a 斗b 、 蕴含的消除规则 卧a ；皂叶a ( 一e ) r 卜- b 、7 取非的消除规则祟( 旧 r 卜- a 、一一7 第1 2 页 信息工程大学硕士学位论文 3 1 2 简单类型九演算 为了把简单类型九演算阐述清楚，我们先简单介绍一下九演算【1 4 j 。 3 1 2 1n 演算 c b u r c h 在1 9 3 6 年提出的九演算系统是最早的计算模型之一。九演算所依据的是一种 完全不同于逻辑的思想。它可以表示序偶、表、树和高阶函数的计算。它是函数式语言 的理论基础，是函数式程序设计语言的纯理论部分的范式。大多数函数式语言都是在九演 算的基础上加了一些修饰而形成的。 n 演算是一种关于函数的简单形式理论。比如h 时3 可以表示函数f ( 曲= 什3 。一般 来说，若f 为表达式，则h f 表示函数俐= f 。它里面的项称为九项，是递归地从变量 石，y ，z ，和其它九一项中构造出来的。九演算有两种基本运算：应用( 印p l i c a t i o n ) 和抽象 ( a b s t r a c t ) 。令f ，“代表任意的九项，则九演算可以表示为： 顾：= x i 五lr j f 甜 变量 抽象 应用 ( 2 ) 在抽象运算中，记号九被引入。在舡f 中，我们称石为约束变量，f 为函数体，在f 中的每 个x 都被抽象所约束。相对地，如果一个变量j ，没有被约束，即如果它没有被包含在某种 抽象砂”中，它就是自由的。 表达式( f 表示对象f 作用于“，o 功既可被理解为计算o 的过程，也可被理解为 此过程的输出。九演算是无类型系统，从而自作用如oo 是合法的，于是它可以模拟递 归。 归约是计算的前提，九演算有两条归约规则，分别是n 归约和b 归约。 a 归约将一个抽象中的约束变量重新命名： ( 肌r ) j 。( 旯弦f 【) ，卅) ( 3 ) p 归约是最重要的，它通过将实际参数替换进函数体来变换一个函数应用： ( ( 触，) “) = ，df