【摘要】：隨著計算機(jī)網(wǎng)絡(luò)和通信技術(shù)的高速發(fā)展,網(wǎng)絡(luò)設(shè)備的信息配置和硬件備份以及互聯(lián)網(wǎng)操作系統(tǒng)(Internet Operating Systems,IOS)的軟件備份和快速恢復(fù)是現(xiàn)今網(wǎng)絡(luò)系統(tǒng)正常運(yùn)行的基本條件。由于簡單文件傳輸協(xié)議(Trivial File Transfer Protocol,TFTP)設(shè)計簡單,通過代碼可以比較容易地實現(xiàn)文件傳輸?shù)男Ч?大部分的網(wǎng)絡(luò)設(shè)備配置和備份功能的底層實現(xiàn)都是基于TFTP協(xié)議的。簡單文件傳輸協(xié)議是一種簡單的文件傳輸協(xié)議,它允許客戶端從遠(yuǎn)程主機(jī)獲取文件或者將文件放入遠(yuǎn)程主機(jī)中,它主要用于網(wǎng)絡(luò)設(shè)備啟動引導(dǎo)時引導(dǎo)文件的獲取。從簡單文件傳輸協(xié)議提出至今,形式化領(lǐng)域中對該協(xié)議的研究工作寥寥無幾,缺少形式化模型的支持使得TFTP協(xié)議的安全性問題經(jīng)常被忽略,使用TFTP協(xié)議進(jìn)行計算機(jī)病毒傳播的事件時有發(fā)生。本文使用進(jìn)程代數(shù)中的通信順序進(jìn)程(Communicating Sequential Processes,CSP)對TFTP協(xié)議進(jìn)行建模與分析。首先對TFTP協(xié)議中通信的消息數(shù)據(jù)進(jìn)行建模,對不同類型的消息使用不同的模型。然后將TFTP協(xié)議抽象成為服務(wù)端、客戶端和資源組件三個模塊,分別描述成為CSP中的進(jìn)程。每個模塊使用相應(yīng)的通道,對接收消息和發(fā)送消息的行為進(jìn)行刻畫。同時,在模型中加入侵入者,侵入者是可以根據(jù)已知的事實偽裝或者攔截消息的進(jìn)程。通過將協(xié)議中的三個模塊和侵入者并發(fā),形成一個完整的協(xié)議系統(tǒng)。本文還使用規(guī)范的方式把TFTP協(xié)議的性質(zhì)描述為規(guī)范集合,然后通過模型檢測工具PAT(Process Analysis Toolkit)對其進(jìn)行了驗證。最后,本文通過一個具體的案例來說明我們所建模型的正確性和合理性,并說明文件傳輸功能會受到協(xié)議安全性的影響。運(yùn)用形式化方法對TFTP協(xié)議進(jìn)行建模與分析,能夠增強(qiáng)工業(yè)界對TFTP協(xié)議的認(rèn)識和理解,同時對其性質(zhì)的驗證能夠引起工業(yè)界對TFTP協(xié)議的安全性考量。
【圖文】：

們使用PAT工具對建立的模型進(jìn)行死鎖性驗證，PAT的死鎖性驗證是通過驗證系統(tǒng)的所有狀態(tài)，，檢查系統(tǒng)是否進(jìn)入死鎖來驗證系統(tǒng)的死鎖性，我們對TFTP協(xié)議驗證得到死鎖性驗證通過，如圖4.1 所示為驗證結(jié)果。圖 4.1: 死鎖性驗證57

抗偽裝性驗證
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2018
【分類號】：TP393.04

【參考文獻(xiàn)】

相關(guān)期刊論文 前7條

1 項俊龍;陳傳峰;;安全協(xié)議形式化驗證方法綜述[J];信息安全與通信保密;2013年05期

2 董葉;陳小平;;TFTP協(xié)議在LM3S6965上的移植和應(yīng)用[J];通信技術(shù);2011年08期

3 賈仰理;張振領(lǐng);李舟軍;;構(gòu)件行為協(xié)議實時性擴(kuò)展及相容性驗證[J];計算機(jī)科學(xué);2010年10期

4 李小波;王健;;基于ARM的TFTP協(xié)議的實現(xiàn)[J];工業(yè)儀表與自動化裝置;2009年06期

5 李虔華;臧習(xí)飛;;TFTP協(xié)議在嵌入式系統(tǒng)中的應(yīng)用[J];電腦與電信;2008年02期

6 許先斌;熊慧君;李洲;楊芬;劉煒;;基于ARM9的嵌入式Linux開發(fā)流程的研究[J];微計算機(jī)信息;2006年11期

7 鄭紅軍;張乃孝;;軟件開發(fā)中的形式化方法[J];計算機(jī)科學(xué);1997年06期

相關(guān)碩士學(xué)位論文 前3條

1 程歆元;船載VSAT遠(yuǎn)程監(jiān)控系統(tǒng)研究與開發(fā)[D];浙江海洋大學(xué);2017年

2 陳華;基于通信順序進(jìn)程的安全協(xié)議形式化研究[D];華中科技大學(xué);2007年

3 苗志鋒;基于有限狀態(tài)機(jī)的IP協(xié)議研究[D];蘭州理工大學(xué);2005年

本文編號：2619969