基于CSP的TFTP协议形式化建模与分析

发布时间：2020-04-08 23:34

【摘要】：随着计算机网络和通信技术的高速发展,网络设备的信息配置和硬件备份以及互联网操作系统(Internet Operating Systems,IOS)的软件备份和快速恢复是现今网络系统正常运行的基本条件。由于简单文件传输协议(Trivial File Transfer Protocol,TFTP)设计简单,通过代码可以比较容易地实现文件传输的效果,大部分的网络设备配置和备份功能的底层实现都是基于TFTP协议的。简单文件传输协议是一种简单的文件传输协议,它允许客户端从远程主机获取文件或者将文件放入远程主机中,它主要用于网络设备启动引导时引导文件的获取。从简单文件传输协议提出至今,形式化领域中对该协议的研究工作寥寥无几,缺少形式化模型的支持使得TFTP协议的安全性问题经常被忽略,使用TFTP协议进行计算机病毒传播的事件时有发生。本文使用进程代数中的通信顺序进程(Communicating Sequential Processes,CSP)对TFTP协议进行建模与分析。首先对TFTP协议中通信的消息数据进行建模,对不同类型的消息使用不同的模型。然后将TFTP协议抽象成为服务端、客户端和资源组件三个模块,分别描述成为CSP中的进程。每个模块使用相应的通道,对接收消息和发送消息的行为进行刻画。同时,在模型中加入侵入者,侵入者是可以根据已知的事实伪装或者拦截消息的进程。通过将协议中的三个模块和侵入者并发,形成一个完整的协议系统。本文还使用规范的方式把TFTP协议的性质描述为规范集合,然后通过模型检测工具PAT(Process Analysis Toolkit)对其进行了验证。最后,本文通过一个具体的案例来说明我们所建模型的正确性和合理性,并说明文件传输功能会受到协议安全性的影响。运用形式化方法对TFTP协议进行建模与分析,能够增强工业界对TFTP协议的认识和理解,同时对其性质的验证能够引起工业界对TFTP协议的安全性考量。
【图文】：

们使用PAT工具对建立的模型进行死锁性验证，PAT的死锁性验证是通过验证系统的所有状态，，检查系统是否进入死锁来验证系统的死锁性，我们对TFTP协议验证得到死锁性验证通过，如图4.1 所示为验证结果。图 4.1: 死锁性验证57

抗伪装性验证
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2018
【分类号】：TP393.04

【参考文献】

相关期刊论文 前7条

1 项俊龙;陈传峰;;安全协议形式化验证方法综述[J];信息安全与通信保密;2013年05期

2 董叶;陈小平;;TFTP协议在LM3S6965上的移植和应用[J];通信技术;2011年08期

3 贾仰理;张振领;李舟军;;构件行为协议实时性扩展及相容性验证[J];计算机科学;2010年10期

4 李小波;王健;;基于ARM的TFTP协议的实现[J];工业仪表与自动化装置;2009年06期

5 李虔华;臧习飞;;TFTP协议在嵌入式系统中的应用[J];电脑与电信;2008年02期

6 许先斌;熊慧君;李洲;杨芬;刘炜;;基于ARM9的嵌入式Linux开发流程的研究[J];微计算机信息;2006年11期

7 郑红军;张乃孝;;软件开发中的形式化方法[J];计算机科学;1997年06期

相关硕士学位论文 前3条

1 程歆元;船载VSAT远程监控系统研究与开发[D];浙江海洋大学;2017年

2 陈华;基于通信顺序进程的安全协议形式化研究[D];华中科技大学;2007年

3 苗志锋;基于有限状态机的IP协议研究[D];兰州理工大学;2005年

本文编号：2619969