边界网关协议安全性的模型检验方法研究

摘要：

作为一种域问路由协议,边界网关协议在因特网上被广泛部署用来进行自治系统之间可达信息的交换.与一般的路由协议不同,它采用了策略来对路由信息的转发进行控制,从而保证链路的安全性.但是由于协议的复杂性,导致其中存在许多的安全漏洞.首先提出一种用来描述协议的抽象方法,然后使用这种方法对具体的网络进行简化,使其更易于分析.在简化后的抽象描述方法基础上,使用Promela建立协议的模型.之后提出了三种基本性质以及两种攻击方式,并且使用SPIN模型检测器对这些性质进行自动验证.通过分析无攻击和有攻击两种情况下的实验数据,我们发现这些攻击对路径的正确选择产生了影响.

关键词：抽象描述、边界网关协议、安全性问题、形式化验证、模型检验

所属期刊栏目：38

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金项目61100034;国家自然科学基金委员会-中国民航局民航联合研究基金项目U1533130;教育部留学回国人员科研启动基金项目2013;中央高校基本科研业务费专项资金项目NS2016092

在线出版日期：2017-08-04（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：1187-1191