摘要
作为一种域间路由协议,边界网关协议在因特网上被广泛部署用来进行自治系统之间可达信息的交换.与一般的路由协议不同,它采用了策略来对路由信息的转发进行控制,从而保证链路的安全性.但是由于协议的复杂性,导致其中存在许多的安全漏洞.首先提出一种用来描述协议的抽象方法,然后使用这种方法对具体的网络进行简化,使其更易于分析.在简化后的抽象描述方法基础上,使用Promela建立协议的模型.之后提出了三种基本性质以及两种攻击方式,并且使用SPIN模型检测器对这些性质进行自动验证.通过分析无攻击和有攻击两种情况下的实验数据,我们发现这些攻击对路径的正确选择产生了影响.
As an inter-domain routing protocol, the border gateway protocol is now widely deployed on the Internet to exchange reachability information between autonomous systems. It is different from other protocols because of its policies configured to control the transmission of route information to keep links secure. Due to the complexity of the protocol, many vulnerabilities have been found. In this paper, we introduce an abstract description approach to describe the protocol. Then we represent the concrete network with an ab- stract system which can be easily analyzed. We construct a model of the protocol with Promela based on the abstract system. Three basic properties are identified next and we also propose two attacks which may violate these properties. The properties will be automaticaUy verified with the SPIN model checker and we will analyse the results of the experiment. The experiment presents that these attacks result in invalid routes.
出处
《小型微型计算机系统》
CSCD
北大核心
2017年第6期1187-1191,共5页
Journal of Chinese Computer Systems
基金
国家自然科学基金项目(61100034)资助
国家自然科学基金委员会-中国民航局民航联合研究基金项目(U1533130)资助
教育部留学回国人员科研启动基金项目(2013)资助
中央高校基本科研业务费专项资金项目(NS2016092)资助
关键词
抽象描述
边界网关协议
安全性问题
形式化验证
模型检验
abstract description
border gateway protocol
security issues
formal verification
model checking
