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

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

使用模型检验自动化验证路由协议

模型检验可验证路由协议的收敛性,环路问题,包交付失败,由于协议描述的歧义导致的问题,安全性缺陷等.实验一建立关注链路状态数据库同步的OSPF模型,设置攻击者路由器伪造消息,找到攻击成功的反例;实验二建立关注节点加入、失效和相应处理的Chord模型,寻找协议缺陷.两个模型都用显式模型检验工具SPIN和有界模型检验工具CBMC实现验证,实验结果表明SPIN解决此类问题更有优势.

路由协议的自动形式化验证方法研究

路由协议被广泛部署于因特网中用来进行路由信息的交换与路径的选择,确保路由协议正确、安全的运行是计算机网络的基础问题之一。近年来,形式化验证已成功应用于协助路由协议的设计和实现,形式化方法的使用能够找到软件测试过程中难以发现的系统缺陷,从而有效地提高系统的安全性。主要介绍了自动形式化验证的几类主要技术基础:模型检验、定理证明和等价性验证。总结了自动形式化验证路由协议的方法和优缺点以及它们在各个方面的研究进展和使用状况,为相关方向的研究者在使用形式化方法验证路由协议时提供了参考依据。最后总结了该领域的研究状况,并对未来研究热点进行了预测和展望,提出了一些可行的研究方向。