數(shù)據(jù)鏈路層協(xié)議的分析與檢測(cè).pdf

1、隨著計(jì)算機(jī)網(wǎng)絡(luò)技術(shù)的發(fā)展與應(yīng)用,網(wǎng)絡(luò)協(xié)議日益復(fù)雜,協(xié)議開發(fā)過程中任何一點(diǎn)錯(cuò)誤都將給分布式系統(tǒng)的穩(wěn)定性、可靠性、堅(jiān)固性、安全性、容錯(cuò)性以及異種系統(tǒng)之間的互通性帶來巨大的危害。因此網(wǎng)絡(luò)協(xié)議的安全性分析和檢測(cè)就顯的極為重要，并且成為當(dāng)今計(jì)算機(jī)安全領(lǐng)域中研究的重大課題。
　　網(wǎng)絡(luò)協(xié)議一般分為不同層次進(jìn)行開發(fā)，每一層負(fù)責(zé)不同的通信功能。數(shù)據(jù)鏈路層是一切數(shù)據(jù)通信網(wǎng)絡(luò)最基礎(chǔ)的架構(gòu)，也是一切高層協(xié)議賴以實(shí)現(xiàn)的基礎(chǔ)。因此數(shù)據(jù)鏈路層協(xié)議的安全性對(duì)整個(gè)

2、網(wǎng)絡(luò)通信起的至關(guān)重要的作用。
　　采用形式化方法(formalmethds)之一的模型檢測(cè)技術(shù)對(duì)網(wǎng)絡(luò)協(xié)議進(jìn)行形式化驗(yàn)證和分析，是構(gòu)建一個(gè)可靠協(xié)議的重要途徑。國外研究者Lesilie Lamport提出了一種新邏輯，行為時(shí)序邏輯（TLA）理論體系，運(yùn)用這種邏輯對(duì)協(xié)議進(jìn)行建模，在一度程度上可以減少由于狀態(tài)空間爆炸帶來的壓力。用TLA描述和推理并發(fā)系統(tǒng)，結(jié)合了標(biāo)準(zhǔn)時(shí)序邏輯和動(dòng)作邏輯的特點(diǎn)，具有較強(qiáng)的描述和推理能力?；赥LA的系統(tǒng)描述語

3、言TLA+以模塊的形式構(gòu)造規(guī)約，并通過擴(kuò)展和實(shí)例化等方法把多個(gè)模塊組合以形成更為復(fù)雜的規(guī)約。用這種方法取得的模塊式規(guī)約可以通過TLA的檢測(cè)工具TLC來檢測(cè)，檢驗(yàn)?zāi)繕?biāo)屬性是否符合規(guī)約并舉出反例。因此，不論在理論上還是在實(shí)際應(yīng)用中，這種模型檢測(cè)技術(shù)都具有一定的研究?jī)r(jià)值。
　　本文在在詳細(xì)介紹數(shù)據(jù)鏈路層基本協(xié)議及其工作原理的基礎(chǔ)上，分析了行為時(shí)序邏輯基本理論，運(yùn)用基于行為時(shí)序邏輯TLA的規(guī)約語言TLA+與模型檢測(cè)工具TLC對(duì)協(xié)議進(jìn)行分析

4、與檢測(cè)，所作的主要工作與創(chuàng)新之處如下：
　　對(duì)數(shù)據(jù)鏈路層中的停止等待ARQ協(xié)議,連續(xù)ARQ協(xié)議的算法以及滑動(dòng)窗口協(xié)議作了深入分析。根據(jù)ARP協(xié)議工作原理，找出ARP協(xié)議弱點(diǎn)，結(jié)合ARP攻擊的主要方式給出應(yīng)對(duì)措施。
　　根據(jù)ARP報(bào)文格式和Libnet構(gòu)造數(shù)據(jù)包的流程即初始化libnet_init()——構(gòu)造ARP協(xié)議塊——構(gòu)造以太網(wǎng)協(xié)議塊——發(fā)送數(shù)據(jù)包——銷毀libnet_destroy的過程構(gòu)造ARP應(yīng)答數(shù)據(jù)包。在構(gòu)造AR

5、P應(yīng)答數(shù)據(jù)包時(shí)將源主機(jī)的MAC地址填充成其他主機(jī)的MAC地址即可以實(shí)現(xiàn)ARP欺騙。
　　對(duì)Leslie Lamport提出的行為時(shí)序邏輯（Temporal Logic of Action）作較為全面的研究,對(duì)TLA中基本概念如變量、狀態(tài)函數(shù)、使能謂詞，以及TLAII中的活性，公平性等概念進(jìn)行深入研究。在對(duì)公平性的研究中得出強(qiáng)公平性可以推出弱公平性的結(jié)論。
　　分析行為時(shí)序邏輯理論，利用一個(gè)擁有三個(gè)字段的記錄構(gòu)造網(wǎng)絡(luò)通信通道c

6、han，三個(gè)字段中有一個(gè)字段代表通道中傳送的內(nèi)容，另兩個(gè)字段的值是0或1，它們用于保證通道在使用過程中傳輸?shù)耐叫浴Ｔ诎l(fā)送者和接收者之間加入一個(gè)緩沖區(qū)，然后在發(fā)送者與緩沖區(qū)以及緩沖區(qū)與接收者之間分別加入一個(gè)通道chan就可以實(shí)現(xiàn)消息的異步傳輸。在通道設(shè)計(jì)的過程中的每一步，文中都給出了具體的實(shí)例及使用方法。
　　研究基于行為時(shí)序邏輯TLA的描述語言TLA+和模型檢測(cè)工具TLC的檢測(cè)原理及建模要求。將待規(guī)約的系統(tǒng)或協(xié)議表示成TLA+的

7、標(biāo)準(zhǔn)形式而后用TLC進(jìn)行檢測(cè)。在規(guī)約中加入THEOREM Spec=>Property，就可以檢驗(yàn)屬性Property是否滿足模型Spec所描述的系統(tǒng)。若不滿足則會(huì)給出一條路徑，這條路徑也就是屬性不滿足系統(tǒng)的一個(gè)反例。
　　根據(jù)停止等待ARQ協(xié)議的算法，用TLA+對(duì)ARQ協(xié)議進(jìn)行建模。用TLC驗(yàn)證了ARQ協(xié)議應(yīng)該滿足的兩條基本屬性，其中一條屬性如：A給B發(fā)送出數(shù)據(jù)幀后,B最終一定能收到A發(fā)來的數(shù)據(jù)幀，得到的結(jié)果是正確、錯(cuò)誤或重復(fù)的