论文部分内容阅读
作为一种域间路由协议,边界网关协议在因特网上被广泛部署用来进行自治系统之间可达信息的交换.与一般的路由协议不同,它采用了策略来对路由信息的转发进行控制,从而保证链路的安全性.但是由于协议的复杂性,导致其中存在许多的安全漏洞.首先提出一种用来描述协议的抽象方法,然后使用这种方法对具体的网络进行简化,使其更易于分析.在简化后的抽象描述方法基础上,使用Promela建立协议的模型.之后提出了三种基本性质以及两种攻击方式,并且使用SPIN模型检测器对这些性质进行自动验证.通过分析无攻击和有攻击两种情况下的实验数据,我们发现这些攻击对路径的正确选择产生了影响.
As an interdomain routing protocol, border gateway protocol is widely deployed on the Internet to exchange information between autonomous systems.Different from the common routing protocols, it uses a strategy to control the forwarding of routing information, Thereby ensuring the security of the link.But due to the complexity of the protocol, there are many security vulnerabilities in it.First, an abstract method to describe the protocol is proposed, and then this method is used to simplify the specific network to make it more Easy to analyze.Based on the simplified abstract description method, Promela is used to establish the protocol model.Then, three basic properties and two attack methods are proposed, and the SPIN model detector is used to verify these properties automatically.By analyzing the non-attack We also found that these attacks have an impact on the correct choice of path.