《基于有向图的网络协议建模》由会员分享，可在线阅读，更多相关《基于有向图的网络协议建模（34页珍藏版）》请在金锄头文库上搜索。
1、摘 要网络协议是互联网通信的基本构架，不完备或错误的协议往往给攻击者提供了攻击的机会。因为协议本身的高并发性以及所处环境的复杂性，网络协议的设计是非常困难的。我们可以通过对协议设计完毕后进行安全建模，并进行自动化验证，来找到协议设计存在的安全隐患。在本文中，我们用两种方法分别对BGP协议进行建模。方法一基于规则推理，对协议进行完全分析，得到协议资源和具有某种推导关系的行为，基本资源可以作为协议行为的参数，通过用AND和OR来表示协议行为的推导关系。将此方法应用到BGP协议，最终在BGP协议的攻击规则图上得到了29条攻击路径。方法二用CSP对协议建模，用CSP来表示协议之间各个进程的并发作用，模
2、型包括协议本身、攻击者，以及所要满足的安全约束。并用FDR检验所建立的模型是否满足约束。用该方法来对BGP进行建模验证，检验结果为，该模型满足其中一个约束，而另一个没有被满足的约束得到了一个反例序列。本文提出了两种对协议进行分析以及建模的方法，一种是基于规则的，一种是用形式化的方法来进行建模。通过这两种方法，我们可以用建立的模型来准确的描述网络协议，使得更好的理解网络协议，并通过对协议的有效分析与验证，得到协议的攻击方法与协议的缺陷。关键词：CSP；网络协议；规则；安全建模；BGP协议ABSTRACTNetwork protocol is the basic framework of Inte
3、rnet communications, however, the incomplete or incorrect protocol often provides attackers some opportunities. Because of the high concurrency of a network protocol and the complexity of the environment where it works, it is difficult to design a network protocol with a reliable safety. We can find
4、 out a network potentials safety hazard through security modeling and automated verification. In this paper, well use two methods to model on the BGP protocol. The first method bases on the rule-based reasoning approach to analyze the protocol and get protocol resources as well as behaviors which ha
5、ve some kinds of derived relations. The basic resources serve as the parameters of the protocols behaviors and indicates the derived relations by “AND” and “OR”. Applying this method to BGP protocol, we successfully get 29 attack paths on the attacking rules diagram. The second method is to model wi
6、th CSP. Well use CSP to indicate the concurrency effect of every process among the protocols. This model contains not only the protocols but also the attackers and the security constraints which need to be satisfied. At the same time, we use FDR to test this model to exam whether it meets the constr
7、aints. In this way, we testify the BGP and the result is that one of the two constraints is satisfied while the other is unsatisfied from which we get a counter-example sequence.We propose two methods-one is rule-based, the other is formalized-to model and analyze the protocol. By using the model, w
8、e are able to precisely describe the network protocol, and then deepen the comprehension of it. By analyzing the protocol efficiently and testing, we obtain the types of attacks and the protocols defects.Key words：CSP；Network Protocol；Rule；Security Protocol；BGP；目 录第一章 绪论11.1.研究目的及意义11.2.国内外发展11.3.主要
9、工作和贡献21.4.论文组织结构3第二章 相关概念介绍42.1.网络协议42.2.通讯顺序进程42.3.FDR5第三章 基于有向图的网络协议建模63.1.网络协议攻击发现和分析架构63.2.网络协议建模73.3.攻击路径分析过程83.4.针对BGP的建模和攻击分析案例93.4.1.BGP协议资源分析103.4.2.BGP协议行为分析113.4.3.BGP协议危害与行为规则分析123.4.4.规则图以及攻击路径分析133.4.5.攻击路径的规范描述163.5.基于规则库的网络协议的攻击发现18第四章 基于CSP的网络协议建模194.1.形式化建模分析194.2.BGP协议的分析与建模案例194.
10、2.1.整体模型介绍204.2.2.BGP协议分析214.2.3.BGP协议模型介绍224.2.4.FDR检测结果27第五章 总结与展望295.1.总结295.2.展望29参考文献304第一章 绪论1.1. 研究目的及意义随着Internet的不断发展，人们对互联网的依赖已经变得越来越重要。互联网作为信息技术革命的一个重要环节，已经深深的影响着每个人的工作，学习和生活。互联网更多的涉及到了金钱利益，隐私，版权专利，是绝大多数机关企业单位正常运维的关键砝码。但同时互联网也存在风险，攻击者找到系统的缺陷和漏洞，对系统进行攻击，从而进行破坏、牟利的行为，造成损失。网络协议是互联网通信的基本构架，网络
11、协议的安全性直接影响互联网的安全。网络协议作为数据交换的准则被广泛的实现和应用在网络设备中，而这些设备对网络协议的实现很大程度制约网络环境的安全系数。所以协议实现的安全性得到保证才能使得用户不会受到攻击。网络协议的开发过程也包括设计、分析、实现、测试与维护等阶段，设计一个安全的协议非常困难，主要原因在于：协议本身所具有的微妙性，还有协议所存在环境的复杂性，攻击者模型的复杂性以及协议的高并发性。通过在设计阶段对网络协议进行形式化的建模，可以实现网络协议的形式化规格，从而对协议模型进行分析，可以界定协议的边界，可以准确描述协议的行为，定义安全协议的特性，并可以验证网络协议是否满足其说明。因此通过对
12、网络协议的安全建模及其形式化，能够更好的理解网络协议，进而可以找到网络协议所存在的安全隐患，通过对这些安全问题进行修补，提出缓和方案，最终能提高网络协议的安全性能。1.2. 国内外发展当前主要都是对于安全协议进行形式化研究，而专门对于网络协议进行的研究比较少，不过他们对于协议形式化描述的方法大同小异。1982年，Dolev和Yao用算法的手段分析了两类特殊的协议的安全性，随后Dolev、Even和Karp的分析方法与之一脉相承，都是用多项式时间的算法对于某些特定类型的安全协议进行判定。不过这些方法只能针对特殊的协议，Dolev与Yao结果的意义开启了用形式化方法分析安全协议的先河。在安全协议的
13、领域，如果把Dolev-Yao的工作视为形式化方法的标志性工作的话，那Burrows，Abadi和Needham的工作就是形式化方法的代表作和里程碑。他们利用知识和信念逻辑，描述和推理认证协议。这个逻辑系统被称为BAN逻辑。这种方法用一集公式表示协议主体的信念或者知识，用一集推理规则从原有公式得到新的信念公式，这个逻辑可以指出一些协议的漏洞。BAN逻辑之后，许多形式化方法被应用于安全协议的分析上。因为受到BAN逻辑的启发，许多人开始寻找或者开发一些安全协议的验证工具，以及一些成熟的形式化方法寻找应用领域。因此上个世纪90年代安全协议的形式化研究出现了空前的繁荣景象。模型检测技术被应用到安全协议
14、的形式化研究中，值得提出的是Lowe利用FDR（Failures-Divergence Refinement）发现Needham-Schroeder协议的一个漏洞。再之后类型检测方法、基于定理证明的方法以及基于计算复杂性的形式化方法发展起来。如今网络协议的建模现如今主要有四种技术：有限状态自动机、Petri网、时态逻辑和通信进程演算。有限状态自动机的建模方式是目前最流行的，基本思想协议是中的组件状态及其状态转换进行分析，在此基础上进行安全的分析和验证。通过对FSM模型的扩展，加入特定属性来完成协议信息的补充以达到特性的建模目的。以扩展FSM的模型描述网路协议，并通过FSM的化简算法降低模型的复
15、杂度，最后通过这种模型生成测试用例，来指导对网络协议实现的测试。Petri网是一种描述分布式系统的数学建模语言，通常以位置和迁移形式来表述系统所具有的状态及状态之间的迁移条件。Petri网的概念最早是由德国人的Carl Adam Petri与1962年在其博士论文自动机通信中提出来的，它是一种适合于开发、异步、分布式系统描述与分析的图形数学工具。近几年利用时间Petri网对网络协议的建模方法也层出不穷，通过时间Petri网对网络协议进行建模，并对模型进行验证确保协议的实现正确可靠。基于时态逻辑的网络协议建模是模态逻辑的扩展，它涉及含有时间信息的时间、状态及其关系的命题、谓词和演算。1977年Pnueli在计算机科学中提出线性时态逻辑后，线性时态逻辑被广泛的应用在有限状态系统的行为描述上。但是因为线性时态逻辑主要体现被描述系统的时序状态，所以一般配合FSM或Petri网进行建模。通信进程演算是计算机通信系统的基本理论模型，它是许多形式化语言的基础。CCS( Calculus of Communication System )的基本成分是事件与进程，而进程是通过顺序、选择和并行三个基本算子来定义的。通信进程演算最初是由英国学者R. Milner提出的，最初用来描述通信开发系
