-
题名边界网关协议安全性的模型检验方法研究
被引量:3
- 1
-
-
作者
黄吴丹
陈哲
-
机构
南京航空航天大学计算机科学与技术学院
软件新技术与产业化协同创新中心
-
出处
《小型微型计算机系统》
CSCD
北大核心
2017年第6期1187-1191,共5页
-
基金
国家自然科学基金项目(61100034)资助
国家自然科学基金委员会-中国民航局民航联合研究基金项目(U1533130)资助
+1 种基金
教育部留学回国人员科研启动基金项目(2013)资助
中央高校基本科研业务费专项资金项目(NS2016092)资助
-
文摘
作为一种域间路由协议,边界网关协议在因特网上被广泛部署用来进行自治系统之间可达信息的交换.与一般的路由协议不同,它采用了策略来对路由信息的转发进行控制,从而保证链路的安全性.但是由于协议的复杂性,导致其中存在许多的安全漏洞.首先提出一种用来描述协议的抽象方法,然后使用这种方法对具体的网络进行简化,使其更易于分析.在简化后的抽象描述方法基础上,使用Promela建立协议的模型.之后提出了三种基本性质以及两种攻击方式,并且使用SPIN模型检测器对这些性质进行自动验证.通过分析无攻击和有攻击两种情况下的实验数据,我们发现这些攻击对路径的正确选择产生了影响.
-
关键词
抽象描述
边界网关协议
安全性问题
形式化验证
模型检验
-
Keywords
abstract description
border gateway protocol
security issues
formal verification
model checking
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名使用模型检验自动化验证路由协议
被引量:2
- 2
-
-
作者
马银雪
陈哲
黄志球
黄吴丹
-
机构
南京航空航天大学计算机科学与技术学院
-
出处
《小型微型计算机系统》
CSCD
北大核心
2015年第11期2462-2466,共5页
-
基金
国家自然科学基金项目(61100034)资助
中国博士后科学基金项目(20110491411
+1 种基金
2012T50498)资助
江苏省博士后科研计划项目(1101092C)资助
-
文摘
模型检验可验证路由协议的收敛性,环路问题,包交付失败,由于协议描述的歧义导致的问题,安全性缺陷等.实验一建立关注链路状态数据库同步的OSPF模型,设置攻击者路由器伪造消息,找到攻击成功的反例;实验二建立关注节点加入、失效和相应处理的Chord模型,寻找协议缺陷.两个模型都用显式模型检验工具SPIN和有界模型检验工具CBMC实现验证,实验结果表明SPIN解决此类问题更有优势.
-
关键词
模型检验
路由协议验证
形式化方法
SPIN
CBMC
-
Keywords
model checking
verification of routing protocols
formal methods
SPIN
CBMC
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名路由协议的自动形式化验证方法研究
- 3
-
-
作者
黄吴丹
严俊琦
-
机构
南京航空航天大学计算机科学与技术学院
-
出处
《计算机技术与发展》
2017年第12期1-6,共6页
-
基金
国家自然科学基金资助项目(61100034)
国家自然科学基金委员会-中国民航局民航联合研究基金(U1533130)
+1 种基金
教育部留学回国人员科研启动基金(2013)
中央高校基本科研业务费专项资金(NS2016092)
-
文摘
路由协议被广泛部署于因特网中用来进行路由信息的交换与路径的选择,确保路由协议正确、安全的运行是计算机网络的基础问题之一。近年来,形式化验证已成功应用于协助路由协议的设计和实现,形式化方法的使用能够找到软件测试过程中难以发现的系统缺陷,从而有效地提高系统的安全性。主要介绍了自动形式化验证的几类主要技术基础:模型检验、定理证明和等价性验证。总结了自动形式化验证路由协议的方法和优缺点以及它们在各个方面的研究进展和使用状况,为相关方向的研究者在使用形式化方法验证路由协议时提供了参考依据。最后总结了该领域的研究状况,并对未来研究热点进行了预测和展望,提出了一些可行的研究方向。
-
关键词
路由协议
形式化验证
模型检验
定理证明
-
Keywords
routing protocol
formal verification
model checking
theorem proving
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-