（计算机软件与理论专业论文）基于sat的有界模型检测及其应用研究.pdf

基于s a t 的有界模型检测及其应用研究专业：计算机软件与理论博士生：杨晋吉指导老师：苏开乐教授摘要无论在计算机系统硬件设计方面还是在软件设计方面，随着设计规模越来越复杂和庞大，会产生越来越多的设计缺陷和错误等。用一些传统的方法往往是代价很高，但还难以检测出它们。形式化验证的优点是在一个设计或系统的研制周期的前期进行。在研制周期的早期进行分析和验证，可大大降低返工的成本，提高效率。基于这些原因，有界模型检测( b o u n d e dm o d e lc k c k i l l g 简称b m c )作为一种重要的形式化验证的方法，它的相关技术的研究和应用在当前具有相当重要的价值和意义。有界模型检测是通过把有限状态机( f s m ) 和l t l 逻辑验证规范否定形式编码成s a r 实例，再由各种s a t 工具来求解，以获得反例。该方法相比基于o b d d技术的模型检测，进一步减轻的状态空间爆炸问题，且给出的反例是最短的。因为b m c 较晚出现，它的很多相关的技术不完善、相关的应用也不普遍。本文围绕b m c 的相关技术和应用进行了一定的研究。主要工作如下：b m c 编码技术的优化可生成规模小易于求解的s a t 实例，对提高有界模型检测的效率至关重要，近年其是b m c 研究中一个热点问题。本文结合f s m 状态转移的特性和线性时序逻辑的语义，在现有的编码基础上，对有界模型检测中对验证g ( p ) 和g ( p 寸f ( q ) ) 这两个很重要很常用的模态算子转换公式进行了优化，给出了简洁高效的递推公式；证明了递推公式和原公式的逻辑关系；基于递推公式设计了编码算法。通过实验比较分析，基于递推公式编码算法在生成s a t 实例规模和求解效率方面，都优于现有的两个主流的编码算法。所给出的方法和思想对有界模型检测的其他模态算子编码的优化，有直接的参考价值。s a t 工具是b m c 的后端求解工具。s a t 问题的研究对包括b m c 在内的许多领域都很有意义。局部搜索方法是求解s a t 实例的一类重要的方法。本文提出用初始概率的方法对局部搜索算法中的变量的初始随机指派进行适当的约束，用该方法对目前的一些重要的s a t 问题的局部搜索算法进行改进，通过对不同结构、不同规模的s a t 问题的实例测试表明，改进后的这些局部搜索算法的效率有了较大的提高。提出用b m c 和串空间结合的方法对安全协议进行验证。主要是通过串空间理论先确定不安全协议的丛结构，依此来约束协议运行的的规模和角色行为，然后用b m c 对该丛结构进行建模验证。这种方式结合了模型检测和定理证明的优点，通过几个安全协议的分析和实验，验证了本方法较传统的模型检测方法的验证效- 一- - 一率局。关键词：有界模型检测，可满足性问题，串空间理论，递归公式，概率论文原创性声明本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人或集体发表或撰写过的作品成果。对本文的研究作出重要贡献的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律后果由本人承担。学位论文作者签名：爿磊乒留言日期：扣学年多月日第1 章绪论无论在计算机系统硬件设计方面还是在软件设计方面，随着设计越来越复杂和庞大，会产生越来越多的设计缺陷和错误等。用一些传统的方法往往是代价很高，但还难以检测出它们。而这些问题一旦出现，可能导致产生严重的后果。如1 9 9 4 年底，奔腾处理器被一位数学教授发现在执行某个特定的浮点运算时出现错误，尽管这个芯片设计上的小缺陷，计算机在9 0 亿次除法运算中仅会一次错误；但为此，i n t e l 公司付出近5 亿美元的巨额，用于回收这些有缺陷的奔腾处理器。1 9 9 6 年6 月，欧洲航天局研制的阿里亚娜火箭在发射升空后不到4 0 秒爆炸；事后调查发现，错误发生是由于一个很大的6 4 位浮点数转换出现异常引起的。这个小小错误，使得多年的努力毁于一旦。尤其近年来，计算机网络应用的不断深入和扩大，这深刻影响和改变着我们的生活方式。网络安全问题也变得更是越来越重要，但也越来越复杂。2 0 0 0 年中，英国拥有1 2 0 万名用户的e g g 互联网银行，被专业黑客利用其网络漏洞，被盗走数十万英镑，发生了全球第一起网络银行盗窃案。之后随着电子商务的交易量迅猛增加，由于各种漏洞和缺陷，由此引起的金融案件的数量和金额大量增加。为保证这些计算机硬件设计、软件设计的正确性和计算机网络系统的安全性，传统的方法是模拟和测试。测试是在已开发的实际的系统中，通过输入实验数据，观察输出结果是否正确。若输出结果不正确，要重新设计和开发，因此成本高。模拟一般适用于在验证初期发现大量和明显的设计错误。但无论模拟还是测试都严重依赖输入的实验数据，对许多越来越复杂和庞大的系统，想用1 0 0 的数据覆盖率来进行模拟和测试几乎不可能；若实验数据覆盖率不够，往往隐蔽的错误难以发现。另外测试往往是一项艰苦的工作，很费时间。许多保证网络系统安全的安全协议，即使密码系统的足够安全，但由于协议设计的逻辑错误，会产生很隐蔽的致命缺陷，而用传统的模拟和测试的方法，很难发现。形式化验证是克服模拟和测试的不足，保证系统正确性和安全性的有效手段。形式化验证有关的工具和方法的研究在当前有相当的价值。本章的结构为：第一节介绍形式化验证及相关知识和模型，第二节介绍形式化验证的重要方法之一一模型检测的原理和相关的技术，第三节介绍另一形式化验证的重要方法一定理证明，第4 节介绍本论文的主要贡献和组织。1 1 形式化验证及相关知识形式化验证是通过数学方法和工具来确保一个设计或系统符合一些准确表达的性质 1 】。具体说，具备三点：( 1 ) 构造一个设计或系统的模型，( 2 ) 这个设计或系统运行的环境描述，( 3 ) 期望这个设计或系统的模型能满足一些性质。形式化验证就是寻找违背这些性质的输入序列，或者证明这些性质在某些情况下一直成立。形式化验证的优点是在一个设计或系统的研制周期的前期进行，具备一定的完备性即可证明性质在某些情况下完全正确性。在目前系统复杂度不断增大，模拟和测试难以发现的隐形缺陷和错误不断增加；由于激烈的市场竞争，产品的研制周期不断缩短，而验证过程占整个研制周期的一半以上，为提高研制的速度，在研制周期的早期进行分析和验证，可大大降低返工的成本，提高效率。基于这些原因，形式化验证的技术和方法的研究和应用在当前具有相当重要的价值和意义。形式化验证早期应用于硬件设计的验证，后在安全协议验证和软件程序方面的验证也有了较多的应用。形式化验证的方式主要有模型检测和定理证明。这两种方法各有优势，各有缺点，后面有更详细的介绍。1 1 1 形式化的规范( s p e c i 6 c a t i o n )形式化的规范就是用形式化语言描述系统或模型运行中需要满足的某些性质。这也是形式化验证要验证的性质。形式化语言是数学上有语法和语义定义的语言。通过形式化语言来深入准确的描述系统的行为和性质，往往可以使系统设计者更深入了解系统，能够帮助设计者发现系统的设计缺陷、不一致的问题、模糊的问题、不完备的问题等等。形式化语言有很多种，如时序逻辑【2 】【3 、进程代数【4 】等，在这里我们主要介绍两种形式化验证中常用且和本论文有一定关系的时序逻辑形式化语言：l i n e a rt e m p o r a ll o g i c s ( 简称l t l ) ，c o m p u t a t i o n a lt r e el o g i c s( 简称c t l ) 。c t l ：c t l 公式由命题逻辑公式和时序模态词两部分构成。命题公式用来表示系统的状态，时序模态词表示系统运行将来能够经过的路径。c t l 的时序模念词由一对符号构成。这对符号的第一个符号 a ，e ，其中a表示必然的，e 表示可能的；这对符号的第二个符号 x ，g f ，u ) ，其中x 表示下一2个，g 表示所有的将来，f 表示一些将来，u 表示直到才。设当前状态为s ，p 、q 为原子命题，某些c t l 公式为真的例子如下：a x ( p ) 为真当且仅当在所有状态s 的后继状态中命题p 都为真。a f ( p ) 为真当且仅当从状态s 开始的所有路径中，每条路径至少存在一个状态，命题p 在该状态中为真。a g ( p ) 为真当且仅当从状态s 开始的所有路径，每条路径所有状态，命题p 在这些状态中为真。e f ( p ) 为真当且仅当从状态s 开始的所有路径中，至少存在一条路径，该路径至少存在一个状态，命题p 在该状态中为真。e g ( p ) 为真当且仅当从状态s 开始的所有路径，至少存在一条路径，该路径上所有状态，命题p 在这些状态中为真。l 1 几：l t l 公式由命题逻辑公式和时序模态词两部分构成。命题公式用来表示系统的状态，时序模态词表示系统运行将来经过的路径。其和c t l 公式不同在于考虑将来每一条路径，而c t l 考虑的是将来的分枝情况。l t l 的时序模态词由一个符号构成。这个符号 x ，g f ，u ) ，其中x 表示下一个，g 表示所有的将来，f 表示一些将来，u 表示直到才。设当前状态为s ，p 、q 为原子命题，某些l t l 公式为真的例子如下：x ( p ) 为真当且仅当在从状态s 路径中，每条路径s 的后继状态中命题p 都为真。f ( p ) 为真当且仅当从状态s 开始的所有路径中，每条路径至少存在一个状态，命题p 在该状态中为真。g ( p ) 为真当且仅当从状态s 开始的所有路径，每条路径所有状态，命题p在这些状态中为真。( puq ) 为真当且仅当状态s 开始的所有路径，每条路径都满足：命题q为真之前的所有状态中，p 都为真。c t l 公式和l t l 公式表达能力有交集，但某些情况l t l 能表达c t l 不能表达，如f g ( p ) ；另一些情况c t l 能表达l t l 不能表达，如a g ( e f ( p ) ) 等。以上c t l 和l 1 、l 严格的语法和语义的定义和说明见文献【5 】。形式化验证的性质主要分两类 6 】：s a 诧t y 性质和l i v e n e s s 性质。s a 诧t y 性质：主要是那些威胁的、不好的事情永远不发生。l t l 表示为：g ( ! p )：p 为不好的事情l i v e n e s s 性质：主要是好的、期待的事情终将发生。l t l 表示为：g ( p 坩( q ) ) ：q 为好的事情s a 诧t y 性质和l i v e n e s s 性质更详细更严格的介绍见文献 7 】【8 】，文献【9 】介绍了如何通过验证s a 诧t y 性质来验证l i v e n e s s 性质。1 1 2d o l 、，e y | a o 模型形式化验证分析安全协议，我们首先抽象出它的一个运行环境系统运行安全协议所面临的最大问题是其所处的网络通信环境是有怀恶意破坏的黑客存在如果将协议及其所处的环境视为一个系统，那么在这个系统中，一般而言包括发送和接收消息的诚实的主体和一个攻击者攻击者相当于网络中的主路由器，所有的消息都由他转发协议的合法消息可被攻击者截取、重放和篡改攻击者将所有已知的消息放入其消息集合s 中诚实主体之间交换的任何消息都将被加入到攻击者的s 中，并且，攻击者可对s 中的消息进行级联( c o n c a t e n a t i o n ) 、分离( d e c o n l p o s i t i o n ) 、加密( e n c r y p t i o n ) 和解密( d e c r y p t i o n ) ，所得消息也将加入到其s中一个被动攻击者( p a s s i v ea t t a c k e r ) 可在线窃听敏感信息而一个主动攻击者( a c t i v ea t t a c k e r ) 则可截断获获取数据包，并对其进行任意的修改，甚至可以伪装成通信主体，欺骗诚实主体与其进行非法通信归纳起来，攻击者的行为表现为以下几种形式，如图1 1 所示，即著名的d o l v e y a o 模型 1 0 【1 1 】：两一v图1 1 攻击者几种形式将消息发送到其意定接收者，即作为网络中的一个总的中继的路由器( r o u t e r ) ；篡改消息( f o r g e ) 后转发；4将消息与以前接收的消息合并，形成一个消息集合墨用于后继攻击；改变部分或全部消息的发送地址( r e d i r e c t ) ；重放( r e p l 矗y ) 消息不进行任何密文的分析破解尽管此模型在发现跟实现细节相关的攻击时有缺陷，因为这个模型不考虑基于密文的分析和攻击，但它简化了协议的分析它被证明为最强的黑客模型，因为它能够模拟任何可能的独立于协议的攻击 1 2 我们把d o l e v y a o 模型作为协议运行环境的一个因素有些研究者甚至把这个模型扩充到具有密码分析能力的黑客描述中 1 3 1 2 模型检测技术模型检测是一种重要的形式化验证方法，主要是对系统或模型的运行来创建一个有限自动机的抽象模型m ，对要验证的性质创建形式语言描述的规范说明巾。模型检测就是通过自动运行来判断模型m 是否能满足巾即m ，如图1 2 所示图1 2 模型检测流程图c l 玳e 等人 1 4 【1 5 】最早提出的这种方法，这种方法就是算法自动搜索状态空间，使规范说明由在所搜索的状态中成立。由于系统被抽象为有限自动机，因此，当穷尽搜索状态空间时，理论能保证收敛。但实际由于物理设备的限制，存在状态空问爆炸问题，所以模型检测一个很重要的挑战是设计好的算法和数据结构使的尽可能搜索大的空间，这样验证问题规模可以更大。m c m i l l a n 等人【1 5 【1 6 】使用o b d d 技术 1 7 】可高效率地表示状态转移，很大程度减轻了状态爆炸问题，因此提高的验证的系统规模。基于o b d d 技术的模型检测s m v 取得很大成功，成功验证了很多协议的问题。后来，又有多个模型检测工具基于这种o b d d 技术。模型检测工具s m v 等出现后，使得自动化的形式化验证方法在实际中取得了很大的成功，并越来越被大家接受和重视，成为模拟、仿真的重要补充。但验证的问题规模虽然较前一代的非o b d d 技术的模型检测器e m c 有很大提高，但实际验证中仍然很受限制，其最大问题仍然是状态空间爆炸问题。b o u n d e dm o d e lc h e c k i n g ( b m c ，有界模型检测) 是继模型检测s m v 后的又一重要突破。有界模型检测是b i e r e 等人在1 9 9 9 年提出【1 8 】。有界模型检测不象s m v 那样通过o b d d 表示状态和转移关系，不通过固定点的迭代计算来求解，而是把状态和转移关系、验证的问题公式转换为s a t 实例，通过s a t 求解工具来求解。因此，有界模型检测是把模型检测的问题求解被转化成s a t 问题求解。而s a t 问题虽然己证明是n p c o m p i e t e 问题，尽管s a t 问题求解最坏情况时间的上界仍然是指数的，但是至今没有指数时间的下界分析，而且在实际应用取得了很大的成功。s a t 求解时的状态空间爆炸问题远没有b d d 的严重。i n t e i 的研究报告【6 4 】显示在对p e n t i u m 4 芯片中抽取的典型设计进行验证中，有界模型检验在验证能力和效率上都比基于o b d d 的符号模型检验有优势。综上所述，对模型检验问题的研究虽然取得了重大的进步，但迄今仍然是具有挑战性的研究课题。目前己有一些新算法或改良算法，如利用对称性、偏序化简、组合推理、抽象等。下面我们简单介绍模型检测这种非常重要o b d d 技术，和一些有影响的模型检测工具。另一和有界模型检测密切相关的s a t 技术在后面章节进行更详细的介绍和讨论。1 2 1o b d d 技术：二叉判定图( b i n a r yd e c i s i o nd i a g r a m ) 是一种表示布尔函数的高效方法布尔表达式的表示方法有很多，最常见的是用规定了句法的命题公式表达，如：x v y ，此外还有诸如真值表等表达形式如针对卅的真值表，如图1 3 所示：6xym0o0o11lo1l11图1 3 删真值表每一种表达方式有其各自的优缺点，命题公式表达十分紧凑，但是决定一个命题公式是否可满足以及两个命题公式是否相同是需要指数时间的：在真值表的表达方式下，判断这两种都十分简单，只需要布尔变量数的线性时间，但是储存整个真值表则需要花费大量的指数级的空间在这种两难的情况下，b d d 无疑是一种较好的选择b d d 的一个简单情形是二叉判定树b d t ( b i i l a r yd e c i s i o nt r e e ) ，二叉判定树也被用于表示布尔函数，它的非终端( 叶) 节点是布尔变量乒，而它的终端( 叶)节点则是布尔值1 或o 由于包含了一些冗余，二叉判定树未能为布尔函数提供紧凑的表示，事实上，它和真值表的大小是一样的但是二叉判定树有很多冗余，如果去除这些冗余，自然能得到很大的简化b r y a n t 1 7 】给出了如何得到布尔函数的规范表示的方法，该方法是在二叉判定树上加上两个限制，得到二又判定图第一个限制是，从树的根节点到终端节点的每一条路径上，布尔变量的出现顺序必须一致第二个限制是，在图中不能有同构的子树或冗余的顶点基于以上分析，得到三种转换规则，用于简化b d d ：1 删除重复的终端节点：对于同样为o ( 或1 ) 值的终端节点，只保留其中的一个，删除其它的o ( 或1 ) 节点，并让原来指向被删除的o ( 或1 ) 节点的弧指向唯一剩下的0 ( 或1 ) 节点2 删除重复的非终端节点：如果b d d 中两个节点 和垅是结构相同的两个子b d d的顶点，那么删除其中一个，并让原本指向这一节点的弧指向另一个节点3 删除满足下列条件的其中一个节点：如果对于两个非终端节点“和v ，有阳“甜)= 阳“v ) ，d 以甜) = ，0 以v ) 并且厅0 咖( z ，) = 地咖( v ) ，那么去掉“( 或v ) ，并让原来指向“( 或v ) 的弧指向1 ，( 或“) 这里砌v ) 表示节点v 所指的变量，d 以d 和衄珈( v ) 分别表示v 所指的左右节点对一个b d d 不断使用上述规则进行简化，直到无法再简化为止，这样就得到了b d d 的规范形式b r y a n t 给出了自底向上化简b d d 的过程，该过程对于原b d d 的大7小来说，是线性时间的由上述方法得到的图称为有序二叉判定图o b d d ( o r d e r e db i n a r yd e c i s i o nd i a g r a m s ) ，它是布尔函数的一种规范表示形式下面给出了一个用0 b d d 表示布尔函数的例子f = ( 1 八2 ) v 3 。图1 4 所示为肭二义树结构，图1 5 所示为珀勺o b d d 树结构，由此可看出o b d d 的存储效率高。图1 - 4二叉树结构图1 5o b d d 树结构变量的排列次序对0 b d d 的结构影响很大，用o b d d 表示布尔函数的例子f =( x 1 人y 2 ) v ( 2 八y 2 ) v ( x 3 八y 3 ) ，在图1 6 和图1 7 的两图中表示同一函数的o b d d结构，但变量排列次序不一样，存储效率大不一样。8图1 6变量优化排序后o b d d图1 7 变量优化排序前o b d do b d d 为布尔公式提供了一种标准的表示方式，这种表示方式通常比合取范式或析取范式更紧凑，而且也有非常有效的方法对它们进行操作( 线型时间的) 因此使得计算大规模的布尔公式提供了良好的数据结构最近十几年来，0 b d d在符号化模型检测领域和人工智能领域等等，都取得了非常好的结果但是我们也必须看到o b d d 的局限性，虽然o b d d 在一定程度上缓解了状态爆炸问题，但它仍然没法避免状态爆炸，当布尔公式变得比较大时，如上百个变量，需要的存储空问就会变的很大，o b d d 显得有点力不从心了，而且b w a n t 也指出，对于有些公式，无论变量顺序怎样，其0 b d d 都是指数爆炸的，没有优化的空间 1 7 所以随着计算规模的进一步扩大，人们需要新的符号化工具2 0 世纪9 0 年代后期，o b d d的作用逐渐衰落，而此时s a t 工具却异军突起，成为取代o b d d 的主力1 2 2 一些著名的模型检测工具的介绍：1 s m v ：s m v 是卡耐基梅隆大学的m c m i l l a n 等在1 9 9 2 年研制的一个通用的模型检测工具。它是现在使用最广泛的模型检测工具之一。也是最早使用ob d d 技术来隐形表示状态和状态转移关系，通过固定点迭代【1 9 计算，最后求出问题的解。由于o b d d 技术使用，节省了存储空间，使可搜索状态空间大大增加，较第一代显式9表示状态及状态转移的模型检测器e m c 2 0 】，在性能、效率方面提高明显。s m v使用的系统描述语言能通过相等关系来表示状态转移，根据系统需要，可由描述语言把整个系统f s m 分为多个子模块( 更小的f s m ) ，每个子模块内部完成部分状态转移、变量赋值工作。要验证的系统的规范说明用c t l 描述。之后，m c m i l l a n等人对s m v 的性能、验证能力不断完善和提高。2 n u s m v ：n u s m v 【2 1 】是意大利i t c i r s t 的c i i l l a t t i 等人为主按照开放源码的工业标准【2 2 】，对s m v 模型检测工具进行了重新设计、实现和扩充。相比s m v ，n u s m v主要的特点有：1 提供了一个交互界面。2 采用模块设计，不同功能由不同模块实现，是一个结构良好、开放的、易扩充的、文档化的模型检测工具平台。3 把基于b d d 技术的s m v 和基于s a t 技术的b m c 有机集成在一个框架中，这样，在验证问题中，可充分利用两种技术的优点。4 验证的规范说明支持c t l描述和l t l 描述。n u s 的整体结构见图1 8 所示，其中各部分介绍如下：核心部分：内存的动态分配，基本数据结构处理( 如h a s h 表等) 。该模块包含了o b d d 一个效率很高的版本c u d d 库。语法分析部分：检测由n u s m v 的模型描述语言建立的模型进行语法分析，为模型建立起供内部处理的一个语法树。编译部分：见图1 9 ，如果用b d d 技术进行模型检测，把语法树编译成b d d结构的f s m ；如果用s a t 技术进行模型检测，最终把语法树编译成r b c 结构的f s m 。模型检测部分：见图1 9 ，如果是b d d 技术进行模型检测，对b d d 结构的f s m用运固定点计算迭代求解；如果用s a t 技术进行模型检测，把r b c 结构的f s m编码成s a r 实例，通过内置的s a t 工具s i m 或外部的s a r 工具z c h a 鼠m i n i s a t等求解。交互部分：早期的n u s m v 的交直界面由文本界面和图形界面两部分，后来，由于兼容和移植问题，现在版本只有文本界面。1 0琳s t a n t 橇。n o ne 蚤j c 0 0 1 n a鼹，lc 0 b p 璩r螂珧l a ；y 雠似l 锄2l a n 横i 囊i f”_ _ i 齄cc 矗抽扣雠噶，to i 嘎扣瓣畦抛撕k # 融o1 w 盘蕾l 知p l 。1 hm图1 8n u s m v 的整体结构图1 9n u s m v 的内部本文的许多工作是在n u s m v 工具中完成，另外一些算法细节在后面的章节介绍。l l3 s p i n ：s p i n 2 3 是美国b e l l 实验室主要面向软件验证的一个o nt h ef l y 的模型检测工具。该工具1 9 8 0 研制，研制时问比较早，后续版本不断改进。它也是目前比较有影响的一个模型检测工具。s p i n 的建模语言是p r o m e l a ，该语言提供创建通信通道的功能，很便于对分布式系统进行建模验证。验证的规范说明是l t l 。s p i n的模型检测算法不是基于f s m ，而是基于另一重要思想一自动理论技术( a u t o m a t a t h e o r e t i c ) 2 4 】。在验证部分中，采用了一种类似于o b d d 技术的偏序约简技术( p a n i a lo r d e rr e d u c t i o nt e c h n i q u e s ) 来提高存储效率。提供了三种使用模式，模式1当模拟器来使用；模式2 进行穷尽验证，这当作模型检测器来验证问题，给出反例等；模式3 当作一个证明系统来证明一个大模型的验证问题的有效性。在最近的版本中，支持嵌入c 语言代码做模型描述的一部分。同时支持深度优先和宽度有限两种搜索方法。也提供了一个良好的图形交互界面。4 r u l e b a s er u l e b a s e 2 5 】是美国i b m 的b e e r 等人1 9 9 6 开发的一个面向工业界的一个模型检测器。建模描述语言是s m v 的建模语言。提供了一个图形用户界面。验证的规范说明是c t l 等。支持联合的和序列的等价检测。5 _ i i d r 英国牛津大学的l o w e 6 】年首先提出使用通信进程代数( c s p ) 2 6 的模型检测器f d r 来进行安全协议的分析这种方法成功地首次检验到n e e d h a m - s c l l r o e d e r 公钥协议的一种攻击，因而在学术界引起广泛的第一章安全协议验证绪论1 7 反响和兴趣，从而启发研究人员用通用的模型检测器( 如s m v 1 6 】，m a u d e f 2 7 】) ，来进行安全协议分析这种方法的思想，是把安全协议抽象成一个进程通信系统坛而通信系统的安全规范& 如安全协议应满足的对应性( c o r r e s p o n d e n c e ) ，秘密性( s e c r e c y ) ，转化为对应的c s p 语言进行描述最后输入给f d r 来检测魄否满足s 当协议不满足规范时，还可以输出反例，发现新的攻击l o w e 在这点意义上可以说开创了安全协议验证的一个新方向由于c s p 语言的复杂性，用户比较难把握为了提供给用户一个更加友好的界面，l o w e 开发了c a s p e r 转换器 2 8 ，提供一种友好的语言脚本，可以方便地自动转化成c s p语言它大大地方便了用户使用l o w e 的方法来进行安全协议的分析6 b r u t u s c m u 的c l a r k e 等人开发的b m t u s 【2 9 】，是一种专门针对安全协议验证来开发相应的模型检测工具b m t u s 也是一种基于穷举搜索的模型检测分析器，他提供了1 2一种专门针对描述安全协议验证的前台语言他的主要思想，是把安全协议模型化为信息的组合和交换信息完全由密钥( k e y s ) ，主体名字( p r m c i p a lm m e s ) ，随机数( n o n c e s ) ，数字证书( d i g “a lc e n i f i c a t e s ) 等等组成b m t u s 的前台规范( s p e c i f i c a t i o n ) 语言，使用一阶逻辑加上一个过去时态算子，来表达安全协议的对应性( c o r r e s p o n d e n c e ) ，秘密性( s e c r e c y ) ，匿名性( a n o n y m i t y ) 及非抵赖性( n o n - r e p u d i a t i o n ) 等等b m t u s 后台的核心算法是基于状态空间的穷举搜索协议开始时，执行主体都处于初始的状态，每执行一步协议，则主体的状态改变一次所有执行主体的可能的状态空间，就是他们所有可能状态的异步合成( s y n c l l r o n o u s c o m p o s i t i o n ) 状态空间虽然囊括和考虑了协议执行时的所有可能的情况，但是它是组合爆炸的，因此c 1 a r k 引入了一系列规约技术( r e d u c t i o n ) ，包括偏序规约( p a r t i a lo r d e rr e d u c t i o n ) 和对称规约( s y m m e t 巧r e d u c t i o n ) ，大大减少了冗余的状态，使b m t u s 可以检测工业级的电子商务协议，如i i o 协议族等7 n r l 协议分析器除了b 1 1 j t u s ，美国海军研究院( n a v a lr e s e a r c hl a b o r a t o 巧) 也开发了自己的专门的安全协议模型检测器，n p a ( n r lp r o t o c o la n a l y z e r ) 【3 0 】n p a 是用p r o l o g 开发的模型检测器，他是基于证伪的( f a l s i 6 c a t i o n ) ，用户首先给出一个不安全的状态，即一种潜在的攻击，n p a 然后进行反向搜索，看是否能可以从协议的初始状态可达，若有，则协议不是安全的，找到的路径就是一个攻击所有的状态转换规则用p r ol o g 来表达并且显式地定义黑客的行为n p a 里协议的描述由以下组成，( a ) 系统状态：包括黑客事先知道的信息，执行主体，已发生的时间序列( b ) 协议规则：每个执行主体的具体动作，及每个动作执行后主体和黑客状态的变化，即黑客能得到的信息黑客的行为用d o l e v y a o 模型来描述( c ) 重写规则：即原子消息的合成分解与加解密的代数描述由于使用p r o l o g ，n p a 实质上是半定理证明和半模型检测的，但他的主要思想是模型检测的他也使用了一些状态规约的技巧n p a 己成功地运用到了分析许多安全协议的漏洞中 3 1 8 s a i m cs a t m cf 3 2 1 是a v i s p a ( a u t o m a t e dv a l i d a t i o no fi n t e m e ts e c u 血yp r o t o c o l sa i l da p p l i c a t i o n s ) 工程的一部分( h t t p ：w w w a v i s p a - p r o j e c t o r g ) 他的思想其实很简单，是借助于有界模型检测( b o u n d e dm o d e lc h e c k i n g ) 的理论，把一个协议执行过程编码成一个命题公式，再把黑客在后步内的攻击编码成另一个公式q ，然后利用s a t 求解器强大的计算能力进行搜索求解( 下一章会讨论s a t 问题) 若 锄唧s a t ，则满足的赋值模型对应于协议的黑客在陟内的一个攻击；若 锄唧u n s a t ，则协议在陟内不存在攻击由于利用了s a t 求解器的计算能力，这个工具在搜索砂内的攻击的效率很高，但是他的缺点也很明显，就是只能搜索砂内的攻击，而在真正的分析协议中，没有人会预先知道潜在的攻击是在几步内可以完成9 a t h e n aa t h e n a 3 3 】，是c m u 的s o n g 等人开发的，是个很特别的模型检测工具，因为他是基于无穷会话的( u n b o u n d e ds e s s i o n s ) ，他们在协议存在攻击的情况下可以输出一个攻击。不存在的话则可以证明其安全性但是a t h e n a 都必须先对协议进行某些假设后才输入处理，否则没法停机因为理论上早已证明，安全协议的安全问题是不可判定的 3 4 a t h e m 是一种基于串空问模型s s m ( s t r a n ds p a c em o d e l ) 的一阶逻辑模型检测工具，这种串空间模型s s m 巧妙地使用串”来定义协议的状态转换，避免了像b n n u s 那样因为状态的异步合成( s y n c l l r o n o u sc o m p o s i t i o n ) 而导致的状态爆炸a t h e n a 融合了模型检测和定理证明的优化技术，使得其有相当高的执行效率目前在国内有一些研究团体进行了模型检测工具的研制和应用，如中山大学和北京大学的苏开乐等s p v 【3 7 【1 4 l 】，北京航空航天大学怀进鹏等s p a 【3 5 】，中科软软件所张文辉等b m v 【8 2 8 0 ，国防科技大学李梦君等s p v t 【3 6 】等，都是很有特点的工具。1 3 定理证明方法定理证明是另一种重要的历史更为悠久的形式化验证方法，它是把系统和要验证或期望的性质都表示为某个形式系统的公式。这个形式系统是由一个公理集合和一个推导规则的集合构成。定理证明就是从公理出发，通过一系列的推导规则，证明要验证的性质公式。证明的过程主要用公理、规则、定义、中间的一些引理来完成。形式化验证中定理证明应用较早例子见文献【3 8 ，这种方法很多情况可由手工来完成，后来，为减轻人工的负担，将一部分的推导工作由机器自动完成，出现了定理证明器( t h e o r e mp r o v e r ) 。定理证明器在软件、硬件的验证方面应用也在不断增多。1 4和模型检测相比，定理证明器在验证性质时不用象模型检测那样穷举搜索所有状态 1 5 1 。定理证明器主要是搜索语法域的一个证明，这大大小于模型检测在语义域的搜索空间。但定理证明器验证比较大的系统时，给出的证明一般会非常大，很难理解，需要非常专业知识和技术分析才能掌握。定理证明可以处理无限的状态空间。为证明无限状态空间的问题，非常依赖于诸如归纳技巧等。即使定理证明器也需要和人进行许多交互工作，因此，定理证明处理过程一般很慢且容易出错。但在发现验证性质公式的证明过程中，人们往往可对系统或模型有非常有价值的深入了解或者获得证明。1 3 1 定理证明一些重要方法或定理证明器做一个简单介绍l - b a n ：b u r r o w s ，a b a d i 和n e e d h a m 在文献 3 9 中提出的b a n 逻辑，是安全协议分析的一个里程碑，是用逻辑进行协议验证开端，后继者用逻辑手段分析安全协议的工作许多都以它为基础b a n 逻辑是一种关于主体信仰，以及用于从已有信仰推知新的信仰的推理规则的逻辑这种逻辑通过对认证协议的运行进行形式化分析，来研究认证双方通过相互发送和接收消息，能否从最初的信仰逐渐发展到协议运行最终要达到的信仰其目的是在一个抽象层次上分析分布式网络系统中认证协议的安全问题如果在协议执行结束时，未能建立起关于诸如共享通信密钥、对方身份等的信任时，则表明这一协议有安全缺陷b a n 逻辑的规则十分简洁和直观，易于使用，因此得到广泛的认可，并成为逻辑形式化分析系统的标准b a n 定义了一套逻辑语言，形式化地描述通信过程中主体信念的变化，把主体名，密钥，n o n c e s 等等定义为原子命题，然后定义公理系统和推理规则，b a n 的基本公式为：b a n 的基本公式及语义p = zp 相信x ，x 表达的事实是真的；尸司x ，p 看了x ，p 收到并看到x 这个命题；p 觇p 曾经说了x ，p 曾经发了x 这个消息；尸xp 对x 进行了判断，p 相信x 的真实性；雾c 的，x 是新鲜的( f r e s h n e s s ) ，表示x 在以往通信会话( 1 1 j n ) 中从未用过；p 山9 ，p 与q 使用密钥k 进行通信；x 表示x 使用密钥k 进行加密b a n 的推导规则直观地反映了逻辑公式构造的语义我们把“若m 垃，出成立则】，成立”记为1 5荃! ；垄圣；兰；茎翌y下面是b a n 一些特定的推理规则：j 消息解读规则：p p 毒q ，p 司甄p q 卜x2 消息新鲜性规则：尸 ： ( x ) 夕 # ( x ，y ) 3 n o n c e 验证规则： # ( x ) ，p q 卜x p q x4 判定规则：p q 净x ，p q x 。pbx：用户首先把一个协议抽象成b a n 表达的命题形式，然后进行推理，若最终能推出尸 = q 弦和q = 尸 = 咒即通信双方对某一事实可以通过这个安全协议达成共识，形成相互信任( m u t u a lb e l i e f s ) b a n 虽然成功验证了一些例子，但是学者们经过研究发现，b a n 逻辑在理想化步骤( i d e a l i z a t i o n s ) 等方面存在着不可逾越的障碍，而且其语义不明晰，因此后来有不少改进版本，主要表现在以下几个方面 4 0 ：对b a n 逻辑自身进行功能和语义扩充导致了b a n 类逻辑的产生，如g n y 【4 1 】逻辑，a t 逻辑 4 2 ，s v o 4 3 逻辑等；为具体的协议设计特定的形式化分析工具，如分析电子商务协议的k a 订a r 逻辑 2 9 以及分析与时问相关的协议的c s 逻辑 4 4 等；突破b a n 及b a n 类逻辑对协议主体的假设的局限性而提出的k g 4 5 逻辑，以及突破主体信仰与知识的单调性而提出的n o n m o n o t o m i c 4 6 逻辑针对b a n 逻辑的缺陷和不足，s y v e r s o n 和0 0 r s c h o t 从另一角度提出了s v o逻辑 4 3 它的出现标志着b a n 及b a n 类逻辑的成熟s v o 逻辑吸收了b a n 、g n y和a t 等逻辑系统的优点，具有十分简洁的推理规则和公理在形式化语义方面，s v 0 逻辑对一些概念作了重新定义，从而取消了a t 4 2 逻辑系统中的一些限制。2 p v s1 6p v s 4 7 1 是0 、r e 等人创建的一种有丰富类型的高阶逻辑系统，它包含依赖类型和谓词类型。适用用软件、硬件的形式化验证。这种逻辑的类型检查是不可判定的，需要定理证明器辅助，人的干预有有助于产生类型的正确条件。定理和定义被集成在参数化的定理中，这些参数可起约束作用。p v s 中的证明是使用向后证明的方式。和原始的高阶逻辑推导相比，p v s 的推导的规则在比较高的层次操作，包括s k o l e m 化、实例化、定理应用、相等重写以及复杂的命题重写。高层次的证明策略类似于h o l 系统，它可通过专用的策略语言从基本的推导规则中建立起来。p v s f 4 8 1 集成了一个判定工具用于等价推导、线性计算和排列等，它主要是一个类型检测器；p v s 还集成了另一个基于b d d 技术的处理命题逻辑的工具，它是一个基于有限状态的u 验证的一个模型检测器。3 p a 曲o n 归纳法p a u l s o n 在文献 4 9 中，提出了一个基于协议消息和事件的攻击结构方法标注的证明法，称为p a u l s o n 归纳法p a u l s o n 将协议归纳定义为所有可能事件路径的集合这种方法通过一个随通信过程不断增长的消息集合h ，在这个集合上应用归纳法，因为尸( f ) ，jp ( f + 1 ) ，所以p ( 门) 对所有自然数胛成立它通过定义了三个集合p a n s ，a n a l z 和s y n t h ，来与d 0 1 e v y a o 模型对应，一个黑客的攻击就可以表示为s y n t h ( a n a l zh ) 然后利用高阶逻辑的定理证明器i s a b e l l a 自动证明处理但是这个过程不是全自动的，需要用户的干预过程，并且由于高阶逻辑的复杂性，证明的效率也会受到影响但是这种方法还是成功验证了一些协议的安全性4 串空间模型( s t r a n ds p a c e s )19 9 8 年，t h a y e r 、h e r z o g 和g u t t m a n 在文献 5 0 中提出了一种新的概念串空间模型( s t r a n ds p a c e s ) 它是一种新型有效的协议形式化分析方法串空间是一种基于图论的分析方法，他把安全协议的通信过程抽象成一种过程关系图，定义了两种偏序关系新口t ，其中前者表示通信协议消息发送接受的时间先后关系，后者定义消息的收发关系，在串空间模型中，用d o l e v y a o 模型显式地定义黑客的行为，并用串进行描述当用户分析安全协议时，首先抽象成图，然后进行偏序关系上的归纳法，分析协议在黑客情况下是否满足安全协议的对应性和秘密性虽然串空间模型用提供了另一种全新的角度去描述和分析安全协议中的通信过程关系，成功地分析了大量的协议，但他本身比较复杂，用户比较难掌握和运用，因此有一定的局限性不过可喜的是s o n g 【3 3 】等人，使用串空问模型作为理论基础1 7开发了a t h e m 这个安全协议的自动验证器，a t h e n a 是一个极其高效的针对安全协议的模型检测器，他妙在使用”串”在表达一个状态，而不是传统的用时间点”因而状态空间大大减少，成功的验证了一些很大的工业上的协议。在后面第5 章、第6 章，我们对串空间的原理有更详细的介绍，并且运用串空间理论和b m c 相结合方法，对一些安全协议进行了验证分析。5 s p i 演算( s p ic a l c u l u s )s p i 演算是p i 演算的扩展p i 演算作为并发计算的基础，是r o b i nm i l n e r 在2 0 世纪9 0 年代初基于c c s 【5 1 】等进程演算模型提出的用于描述并发系统和分布式系统的形式化语言，具有很强的表达能力p i 演算的独到之处在于引入了通道( c h a n n e l ) 的概念：通道可以被创建和传递，从而使得p i 演算可以描述拓扑结构动态改变的通信系统；通道的作用域规则使得通道作用域之外的进程无法访问该通道，在一定程度上保证了通信的安全性然而，p i 演算并未提供用于描述协议中加，解密的结构，因而无法表示分布式通信系统中常用的密码学操作。为了便于描述和分析各类依赖于密码学和通信信道的安全协议，a b a d 洱口g o r d o n 在p i 演算的基础上通过增加支持描述密码操作的原语，提出了s p i 演算 5 2 s p i 演算保留了p i 演算的部分语法结构，同时又增加了用于描述各种密码学操作的语法结构使得它成为分析安全协议的强有力的数学工具，因为它为描述和验证协议的安全规范如认证性( a u t h e n t i c “y ) 和秘密性( s e c r e c y ) 提供了数学语言和证明方法6 可信任代理和不可信任代理的方法该方法是b 0 1 i g n a n o 于1 9 9 7 提出的 5