基于模型检验的路由协议验证方法研究

发布时间：2021-03-04 07:48

　　计算机网络多样化的发展催生出大量新的路由协议,这些路由协议的安全性和正确性问题亟待解决。目前,基于形式化的方法、技术、工具已大量应用在路由协议研究上,帮助实现协议的设计和实施。但现实问题是,一方面路由协议的发展变得多样化,协议应用的网络规模从少节点到多节点不等;分层路由和人为规定的选路策略也使得概念简单清晰、性能优良的算法变得复杂;通信链路和节点的不可靠使网络拓扑呈动态变化。另一方面,形式化方法的理论较深,规约、建模语言多样,模型检验、定理证明技术多样,支持形式化验证的工具多样。相比理论上的可行性,形式化方法的工具仍然较弱。因此,网络协议研究人员如果想掌握全部知识似乎不可行,选择合适的形式化验证方法、技术、工具应用在路由协议设计和实现上,也需要花费大量时间和精力。本文提出一种基于模型检验的路由协议正确性和安全性的验证方法,该方法通过对协议的假设和简化抽取出模型,并通过基于反例的抽象精化技术实行验证和模型精化。将该方法应用在三个路由协议的建模和验证上,使用有代表性的模型检验工具SPIN和CBMC验证了包括安全性、正确性和收敛性的性质,通过对验证结果的分析,有效说明了该方法的可行性。 

【文章来源】：南京航空航天大学江苏省 211工程院校

【文章页数】：68 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
注释表
第一章 绪论
    1.1 课题研究背景
    1.2 国内外研究现状
    1.3 论文的选题依据和内容
    1.4 论文的结构安排
第二章 模型检验及工具综述
    2.1 模型检验概述
        2.1.1 显式模型检验
        2.1.2 符号模型检验
        2.1.3 有界模型检验
        2.1.4 抽象技术
    2.2 模型检验工具SPIN
        2.2.1 建模语言Promela
        2.2.2 性质描述-线性时序逻辑
        2.2.3 使用SPIN验证
    2.3 模型检验工具CBMC
        2.3.1 CBMC建模程序内部变换特点
        2.3.2 性质描述
        2.3.3 使用CBMC验证
    2.4 本章小结
第三章 使用模型检验验证路由协议的方法
    3.1 路由协议化简的基本原则
        3.1.1 路由协议简述
        3.1.2 化简原则
    3.2 基于模型检验的路由协议建模和验证
    3.3 本章小结
第四章 使用模型检验验证路由协议的实例分析
    4.1 实例之OSPF
        4.1.1 OSPF基础
        4.1.2 OSPF建模
        4.1.3 OSPF安全性描述
    4.2 实例之Chord
        4.2.1 Chord基础
        4.2.2 Chord建模
        4.2.3 Chord正确性描述
    4.3 实例之BGP
        4.3.1 BGP基础
        4.3.2 BGP建模
        4.3.3 BGP收敛性描述
    4.4 本章小结
第五章 实验结果与分析
    5.1 实验结果
        5.1.1 OSPF验证结果
        5.1.2 Chord验证结果
        5.1.3 BGP验证结果
    5.2 SPIN与CBMC在路由协议验证上的性能对比
    5.3 本章小结
第六章 总结与展望
    6.1 论文总结
    6.2 未来工作展望
参考文献
致谢
在学期间的研究成果及发表的学术论文


【参考文献】：
期刊论文
[1]模型检测中状态爆炸问题研究综述[J]. 侯刚,周宽久,勇嘉伟,任龙涛,王小龙.  计算机科学. 2013(S1)
[2]安全协议20年研究进展[J]. 卿斯汉.  软件学报. 2003(10)



本文编号：3062838