網(wǎng)絡(luò)協(xié)議畢業(yè)設(shè)計(jì)

1、<p><b>　　摘 要</b></p><p>　　網(wǎng)絡(luò)協(xié)議是互聯(lián)網(wǎng)通信的基本構(gòu)架，不完備或錯(cuò)誤的協(xié)議往往給攻擊者提供了攻擊的機(jī)會(huì)。因?yàn)閰f(xié)議本身的高并發(fā)性以及所處環(huán)境的復(fù)雜性，網(wǎng)絡(luò)協(xié)議的設(shè)計(jì)是非常困難的。我們可以通過對(duì)協(xié)議設(shè)計(jì)完畢后進(jìn)行安全建模，并進(jìn)行自動(dòng)化驗(yàn)證，來找到協(xié)議設(shè)計(jì)存在的安全隱患。</p><p>　　在本文中，我們用兩種方法分別對(duì)BGP協(xié)

2、議進(jìn)行建模。方法一基于規(guī)則推理，對(duì)協(xié)議進(jìn)行完全分析，得到協(xié)議資源和具有某種推導(dǎo)關(guān)系的行為，基本資源可以作為協(xié)議行為的參數(shù)，通過用AND和OR來表示協(xié)議行為的推導(dǎo)關(guān)系。將此方法應(yīng)用到BGP協(xié)議，最終在BGP協(xié)議的攻擊規(guī)則圖上得到了29條攻擊路徑。方法二用CSP對(duì)協(xié)議建模，用CSP來表示協(xié)議之間各個(gè)進(jìn)程的并發(fā)作用，模型包括協(xié)議本身、攻擊者，以及所要滿足的安全約束。并用FDR檢驗(yàn)所建立的模型是否滿足約束。用該方法來對(duì)BGP進(jìn)行建模驗(yàn)證，檢驗(yàn)結(jié)

3、果為，該模型滿足其中一個(gè)約束，而另一個(gè)沒有被滿足的約束得到了一個(gè)反例序列。</p><p>　　本文提出了兩種對(duì)協(xié)議進(jìn)行分析以及建模的方法，一種是基于規(guī)則的，一種是用形式化的方法來進(jìn)行建模。通過這兩種方法，我們可以用建立的模型來準(zhǔn)確的描述網(wǎng)絡(luò)協(xié)議，使得更好的理解網(wǎng)絡(luò)協(xié)議，并通過對(duì)協(xié)議的有效分析與驗(yàn)證，得到協(xié)議的攻擊方法與協(xié)議的缺陷。</p><p>　　關(guān)鍵詞：CSP；網(wǎng)絡(luò)協(xié)議；規(guī)則；安全

4、建模；BGP協(xié)議</p><p><b>　　ABSTRACT</b></p><p>　　Network protocol is the basic framework of Internet communications, however, the incomplete or incorrect protocol often provides attackers

5、some opportunities. Because of the high concurrency of a network protocol and the complexity of the environment where it works, it is difficult to design a network protocol with a reliable safety. We can find out a netwo

6、rk potential’s safety hazard through security modeling and automated verification. </p><p>　　In this paper, we’ll use two methods to model on the BGP protocol. The first method bases on the rule-based reason

7、ing approach to analyze the protocol and get protocol resources as well as behaviors which have some kinds of derived relations. The basic resources serve as the parameters of the protocol’s behaviors and indicates the d

8、erived relations by “AND” and “OR”. Applying this method to BGP protocol, we successfully get 29 attack paths on the attacking rules diagram. The second method is to </p><p>　　We propose two methods---one is

9、 rule-based, the other is formalized---to model and analyze the protocol. By using the model, we are able to precisely describe the network protocol, and then deepen the comprehension of it. By analyzing the protocol eff

10、iciently and testing, we obtain the types of attacks and the protocol’s defects.</p><p>　　Key words：CSP；Network Protocol；Rule；Security Protocol；BGP；</p><p><b>　　目 錄</b></p>

11、<p><b>　　第一章 緒論1</b></p><p>　　1.1.研究目的及意義1</p><p>　　1.2.國(guó)內(nèi)外發(fā)展1</p><p>　　1.3.主要工作和貢獻(xiàn)2</p><p>　　1.4.論文組織結(jié)構(gòu)3</p><p>　　第二章 相關(guān)概念介紹4&l

12、t;/p><p>　　2.1.網(wǎng)絡(luò)協(xié)議4</p><p>　　2.2.通訊順序進(jìn)程4</p><p>　　2.3.FDR5</p><p>　　第三章 基于有向圖的網(wǎng)絡(luò)協(xié)議建模6</p><p>　　3.1.網(wǎng)絡(luò)協(xié)議攻擊發(fā)現(xiàn)和分析架構(gòu)6</p><p>　　3.2.網(wǎng)絡(luò)協(xié)議建模

13、7</p><p>　　3.3.攻擊路徑分析過程8</p><p>　　3.4.針對(duì)BGP的建模和攻擊分析案例9</p><p>　　3.4.1.BGP協(xié)議資源分析10</p><p>　　3.4.2.BGP協(xié)議行為分析11</p><p>　　3.4.3.BGP協(xié)議危害與行為規(guī)則分析12</

14、p><p>　　3.4.4.規(guī)則圖以及攻擊路徑分析13</p><p>　　3.4.5.攻擊路徑的規(guī)范描述16</p><p>　　3.5.基于規(guī)則庫的網(wǎng)絡(luò)協(xié)議的攻擊發(fā)現(xiàn)18</p><p>　　第四章 基于CSP的網(wǎng)絡(luò)協(xié)議建模19</p><p>　　4.1.形式化建模分析19</p>&

15、lt;p>　　4.2.BGP協(xié)議的分析與建模案例19</p><p>　　4.2.1.整體模型介紹20</p><p>　　4.2.2.BGP協(xié)議分析21</p><p>　　4.2.3.BGP協(xié)議模型介紹22</p><p>　　4.2.4.FDR檢測(cè)結(jié)果27</p><p>　　第五章 總

16、結(jié)與展望29</p><p>　　5.1.總結(jié)29</p><p>　　5.2.展望29</p><p><b>　　參考文獻(xiàn)30</b></p><p><b>　　緒論</b></p><p><b>　　研究目的及意義</b></

17、p><p>　　隨著Internet的不斷發(fā)展，人們對(duì)互聯(lián)網(wǎng)的依賴已經(jīng)變得越來越重要?；ヂ?lián)網(wǎng)作為信息技術(shù)革命的一個(gè)重要環(huán)節(jié)，已經(jīng)深深的影響著每個(gè)人的工作，學(xué)習(xí)和生活?；ヂ?lián)網(wǎng)更多的涉及到了金錢利益，隱私，版權(quán)專利，是絕大多數(shù)機(jī)關(guān)企業(yè)單位正常運(yùn)維的關(guān)鍵砝碼。但同時(shí)互聯(lián)網(wǎng)也存在風(fēng)險(xiǎn)，攻擊者找到系統(tǒng)的缺陷和漏洞，對(duì)系統(tǒng)進(jìn)行攻擊，從而進(jìn)行破壞、牟利的行為，造成損失。</p><p>　　網(wǎng)絡(luò)協(xié)議是互聯(lián)網(wǎng)

18、通信的基本構(gòu)架，網(wǎng)絡(luò)協(xié)議的安全性直接影響互聯(lián)網(wǎng)的安全。網(wǎng)絡(luò)協(xié)議作為數(shù)據(jù)交換的準(zhǔn)則被廣泛的實(shí)現(xiàn)和應(yīng)用在網(wǎng)絡(luò)設(shè)備中，而這些設(shè)備對(duì)網(wǎng)絡(luò)協(xié)議的實(shí)現(xiàn)很大程度制約網(wǎng)絡(luò)環(huán)境的安全系數(shù)。所以協(xié)議實(shí)現(xiàn)的安全性得到保證才能使得用戶不會(huì)受到攻擊。</p><p>　　網(wǎng)絡(luò)協(xié)議的開發(fā)過程也包括設(shè)計(jì)、分析、實(shí)現(xiàn)、測(cè)試與維護(hù)等階段，設(shè)計(jì)一個(gè)安全的協(xié)議非常困難，主要原因在于：協(xié)議本身所具有的微妙性，還有協(xié)議所存在環(huán)境的復(fù)雜性，攻擊者模型的復(fù)雜

19、性以及協(xié)議的高并發(fā)性。</p><p>　　通過在設(shè)計(jì)階段對(duì)網(wǎng)絡(luò)協(xié)議進(jìn)行形式化的建模，可以實(shí)現(xiàn)網(wǎng)絡(luò)協(xié)議的形式化規(guī)格，從而對(duì)協(xié)議模型進(jìn)行分析，可以界定協(xié)議的邊界，可以準(zhǔn)確描述協(xié)議的行為，定義安全協(xié)議的特性，并可以驗(yàn)證網(wǎng)絡(luò)協(xié)議是否滿足其說明。因此通過對(duì)網(wǎng)絡(luò)協(xié)議的安全建模及其形式化，能夠更好的理解網(wǎng)絡(luò)協(xié)議，進(jìn)而可以找到網(wǎng)絡(luò)協(xié)議所存在的安全隱患，通過對(duì)這些安全問題進(jìn)行修補(bǔ)，提出緩和方案，最終能提高網(wǎng)絡(luò)協(xié)議的安全性能。&l

20、t;/p><p><b>　　國(guó)內(nèi)外發(fā)展</b></p><p>　　當(dāng)前主要都是對(duì)于安全協(xié)議進(jìn)行形式化研究，而專門對(duì)于網(wǎng)絡(luò)協(xié)議進(jìn)行的研究比較少，不過他們對(duì)于協(xié)議形式化描述的方法大同小異。</p><p>　　1982年，Dolev和Yao用算法的手段分析了兩類特殊的協(xié)議的安全性，，隨后Dolev、Even和Karp的分析方法與之一脈相承，都是用多

21、項(xiàng)式時(shí)間的算法對(duì)于某些特定類型的安全協(xié)議進(jìn)行判定。不過這些方法只能針對(duì)特殊的協(xié)議，Dolev與Yao結(jié)果的意義開啟了用形式化方法分析安全協(xié)議的先河。</p><p>　　在安全協(xié)議的領(lǐng)域，如果把Dolev-Yao的工作視為形式化方法的標(biāo)志性工作的話，那Burrows，Abadi和Needham的工作就是形式化方法的代表作和里程碑。他們利用知識(shí)和信念邏輯，描述和推理認(rèn)證協(xié)議。這個(gè)邏輯系統(tǒng)被稱為BAN邏輯。這種方法用

22、一集公式表示協(xié)議主體的信念或者知識(shí)，用一集推理規(guī)則從原有公式得到新的信念公式，這個(gè)邏輯可以指出一些協(xié)議的漏洞。</p><p>　　BAN邏輯之后，許多形式化方法被應(yīng)用于安全協(xié)議的分析上。因?yàn)槭艿紹AN邏輯的啟發(fā)，許多人開始尋找或者開發(fā)一些安全協(xié)議的驗(yàn)證工具，以及一些成熟的形式化方法尋找應(yīng)用領(lǐng)域。因此上個(gè)世紀(jì)90年代安全協(xié)議的形式化研究出現(xiàn)了空前的繁榮景象。模型檢測(cè)技術(shù)被應(yīng)用到安全協(xié)議的形式化研究中，值得提出的是

23、Lowe利用FDR（Failures-Divergence Refinement）發(fā)現(xiàn)Needham-Schroeder協(xié)議的一個(gè)漏洞。再之后類型檢測(cè)方法、基于定理證明的方法以及基于計(jì)算復(fù)雜性的形式化方法發(fā)展起來。</p><p>　　如今網(wǎng)絡(luò)協(xié)議的建?，F(xiàn)如今主要有四種技術(shù)：有限狀態(tài)自動(dòng)機(jī)、Petri網(wǎng)、時(shí)態(tài)邏輯和通信進(jìn)程演算。</p><p>　　有限狀態(tài)自動(dòng)機(jī)的建模方式是目前最流行的，

24、基本思想?yún)f(xié)議是中的組件狀態(tài)及其狀態(tài)轉(zhuǎn)換進(jìn)行分析，在此基礎(chǔ)上進(jìn)行安全的分析和驗(yàn)證。通過對(duì)FSM模型的擴(kuò)展，加入特定屬性來完成協(xié)議信息的補(bǔ)充以達(dá)到特性的建模目的。以擴(kuò)展FSM的模型描述網(wǎng)路協(xié)議，并通過FSM的化簡(jiǎn)算法降低模型的復(fù)雜度，最后通過這種模型生成測(cè)試用例，來指導(dǎo)對(duì)網(wǎng)絡(luò)協(xié)議實(shí)現(xiàn)的測(cè)試。</p><p>　　Petri網(wǎng)是一種描述分布式系統(tǒng)的數(shù)學(xué)建模語言，通常以位置和遷移形式來表述系統(tǒng)所具有的狀態(tài)及狀態(tài)之間的遷移

25、條件。Petri網(wǎng)的概念最早是由德國(guó)人的Carl Adam Petri與1962年在其博士論文《自動(dòng)機(jī)通信》中提出來的，它是一種適合于開發(fā)、異步、分布式系統(tǒng)描述與分析的圖形數(shù)學(xué)工具。近幾年利用時(shí)間Petri網(wǎng)對(duì)網(wǎng)絡(luò)協(xié)議的建模方法也層出不窮，通過時(shí)間Petri網(wǎng)對(duì)網(wǎng)絡(luò)協(xié)議進(jìn)行建模，并對(duì)模型進(jìn)行驗(yàn)證確保協(xié)議的實(shí)現(xiàn)正確可靠。</p><p>　　基于時(shí)態(tài)邏輯的網(wǎng)絡(luò)協(xié)議建模是模態(tài)邏輯的擴(kuò)展，它涉及含有時(shí)間信息的時(shí)間、狀態(tài)

26、及其關(guān)系的命題、謂詞和演算。1977年P(guān)nueli在計(jì)算機(jī)科學(xué)中提出線性時(shí)態(tài)邏輯后，線性時(shí)態(tài)邏輯被廣泛的應(yīng)用在有限狀態(tài)系統(tǒng)的行為描述上。但是因?yàn)榫€性時(shí)態(tài)邏輯主要體現(xiàn)被描述系統(tǒng)的時(shí)序狀態(tài)，所以一般配合FSM或Petri網(wǎng)進(jìn)行建模。</p><p>　　通信進(jìn)程演算是計(jì)算機(jī)通信系統(tǒng)的基本理論模型，它是許多形式化語言的基礎(chǔ)。CCS( Calculus of Communication System )的基本成分是事件與

27、進(jìn)程，而進(jìn)程是通過順序、選擇和并行三個(gè)基本算子來定義的。通信進(jìn)程演算最初是由英國(guó)學(xué)者R. Milner提出的，最初用來描述通信開發(fā)系統(tǒng)的代數(shù)理論。Hoare在CCS的基礎(chǔ)上建立了通信順序進(jìn)程（CSP, Communication Sequential Processes）</p><p><b>　　主要工作和貢獻(xiàn)</b></p><p>　　本文通過對(duì)網(wǎng)絡(luò)協(xié)議BGP

28、（Border Gateway Protocol，邊界網(wǎng)關(guān)協(xié)議）的分析，用形式化的方法來進(jìn)行安全建模，在研究過程中采取了兩種方式對(duì)協(xié)議進(jìn)行了形式化描述，</p><p>　　一種方式主要是通過對(duì)協(xié)議進(jìn)行分析，然后用擴(kuò)展有向圖的方式來對(duì)協(xié)議進(jìn)行安全建模，最終建立相應(yīng)的庫，通過這種建模方式可以得出相應(yīng)的攻擊路徑，并對(duì)得到的路徑進(jìn)行了形式化描述，但是這種建模方式的形式化程度還不夠，在此基礎(chǔ)上，用CSP（Communic

29、ating Sequential Processes，通訊順序進(jìn)程）對(duì)協(xié)議進(jìn)行描述，將協(xié)議作為進(jìn)程來分別建模，最終是多個(gè)進(jìn)程的并行化，并對(duì)協(xié)議的一致性與正確性進(jìn)行了驗(yàn)證。</p><p><b>　　具體工作主要包括：</b></p><p>　　對(duì)協(xié)議進(jìn)行分析?；趨f(xié)議的RFC文檔，經(jīng)過閱讀與分析，得出協(xié)議的基本資源與行為，從這些基本知識(shí)中得出既定事實(shí)、相應(yīng)的推理規(guī)

30、則，查閱有關(guān)協(xié)議安全的RFC文檔，得出協(xié)議受攻擊的攻擊目標(biāo)，以及這些目標(biāo)所可能涉及的危害。</p><p>　　針對(duì)以上的分析，建立相應(yīng)的庫，包括資源表、行為表、既定事實(shí)表、規(guī)則表以及危害表。 </p><p>　　將上面的資源與行為用擴(kuò)展有向圖進(jìn)行描述，行為作為節(jié)點(diǎn)，資源作為節(jié)點(diǎn)參數(shù)，利用規(guī)則進(jìn)行推理。</p><p>　　根據(jù)有向圖來得出每條攻擊路徑，并用形式化

31、的方式來表示每條攻擊路徑，這些攻擊路徑可以用來驗(yàn)證協(xié)議設(shè)計(jì)中是否會(huì)產(chǎn)生某些攻擊危害。</p><p>　　對(duì)協(xié)議的狀態(tài)機(jī)進(jìn)行分析，然后用CSP的方式來描述對(duì)協(xié)議進(jìn)行建模。</p><p>　　對(duì)協(xié)議所滿足的性質(zhì)進(jìn)行CSP描述，描述了要滿足的一致性與正確性</p><p>　　利用FDR（Failures-Divergence Refinement）對(duì)協(xié)議模型與所要滿

32、足的描述進(jìn)行驗(yàn)證</p><p>　　對(duì)驗(yàn)證得到的結(jié)果進(jìn)行分析。</p><p><b>　　論文組織結(jié)構(gòu)</b></p><p>　　第一章主要闡述本論文的研究目的及意義，國(guó)內(nèi)外發(fā)展?fàn)顩r以及主要工作</p><p>　　第二章相關(guān)知識(shí)介紹，本章對(duì)于網(wǎng)絡(luò)協(xié)議、通訊順序進(jìn)程與FDR進(jìn)行了說明。</p><

33、;p>　　第三章對(duì)有向圖建模的方法進(jìn)行介紹，并對(duì)BGP協(xié)議進(jìn)行分析，得到最后結(jié)果。</p><p>　　第四章用CSP對(duì)協(xié)議進(jìn)行建模與驗(yàn)證，同時(shí)對(duì)BGP的建模過程以及驗(yàn)證進(jìn)行分析，對(duì)得出的結(jié)果進(jìn)行分析。</p><p>　　第五章總結(jié)與展望。通過對(duì)兩種方法進(jìn)行總結(jié)，提出了未來的研究方向。</p><p><b>　　相關(guān)概念介紹</b>&

34、lt;/p><p><b>　　網(wǎng)絡(luò)協(xié)議</b></p><p>　　在計(jì)算機(jī)網(wǎng)絡(luò)中要做到有條不紊的交換數(shù)據(jù)，就必須遵守一些事先規(guī)定好的規(guī)則。而這些規(guī)則明確規(guī)定了所交換的數(shù)據(jù)的格式以及有關(guān)的同步問題，這里的同步指的是在一定的條件下應(yīng)當(dāng)發(fā)生什么事件，因而同步含有時(shí)序的意思。而這些為進(jìn)行網(wǎng)絡(luò)中的數(shù)據(jù)交換而建立的規(guī)則、標(biāo)準(zhǔn)或約束稱為網(wǎng)絡(luò)協(xié)議。網(wǎng)絡(luò)協(xié)議是計(jì)算機(jī)網(wǎng)絡(luò)中不可缺少的組成

35、部分，其功能在于確保計(jì)算機(jī)之間能夠進(jìn)行正常、可靠的數(shù)據(jù)通信。</p><p>　　網(wǎng)絡(luò)協(xié)議主要由三個(gè)要素組成：</p><p>　　語法 即數(shù)據(jù)與控制信息的結(jié)構(gòu)或格式</p><p>　　語義 即需要發(fā)出何種控制信息，完成何種動(dòng)作以及做出何種響應(yīng)</p><p>　　同步 即事件實(shí)現(xiàn)順序的詳細(xì)說明</p><p>　　

36、基于系統(tǒng)的工程方法是保證網(wǎng)絡(luò)協(xié)議質(zhì)量的唯一方式。網(wǎng)絡(luò)協(xié)議的開發(fā)必須經(jīng)過協(xié)議設(shè)計(jì)、協(xié)議描述、協(xié)議驗(yàn)證與性能分析、協(xié)議實(shí)現(xiàn)、協(xié)議測(cè)試、協(xié)議維護(hù)六個(gè)階段。而一個(gè)協(xié)議是否正確與安全關(guān)鍵在于其設(shè)計(jì)是否滿足滿足應(yīng)具備的性質(zhì)，因此對(duì)設(shè)計(jì)的描述與驗(yàn)證遍顯得極其重要。對(duì)設(shè)計(jì)的協(xié)議進(jìn)行描述有三種方法：自然語言、程序設(shè)計(jì)語言以及形式化語言。用自然語言描述時(shí)，表達(dá)能力強(qiáng)，可讀性較好，但描述不準(zhǔn)確，存在二義性。而用程序設(shè)計(jì)語言來描述時(shí)便于協(xié)議的實(shí)現(xiàn)，但是可讀性很

37、差，表述協(xié)議的能力較差。形式化描述有嚴(yán)格的語法和語義定義。更準(zhǔn)確簡(jiǎn)明的描述系統(tǒng)特征。所以通過形式化的對(duì)協(xié)議進(jìn)行建模，對(duì)所建的模型也可以更好的驗(yàn)證，因?yàn)榉切问交尿?yàn)證一般還是基于人工經(jīng)驗(yàn)進(jìn)行驗(yàn)證，而形式化驗(yàn)證有相應(yīng)的工具支持，可以自動(dòng)執(zhí)行。綜上所述，對(duì)協(xié)議的形式化建模顯得尤為重要。</p><p><b>　　通訊順序進(jìn)程</b></p><p>　　CSP（Commu

38、nicating Sequential Processes，通訊順序進(jìn)程）是一個(gè)描述并行系統(tǒng)的概念，屬于一種面向分布式系統(tǒng)的程序設(shè)計(jì)語言嗎，是一種研究并發(fā)系統(tǒng)問題的良好工具。C.A.R.Hoare作為發(fā)明人寫了一部很好的著作來介紹CSP。</p><p>　　CSP將一個(gè)并發(fā)系統(tǒng)由若干個(gè)并行運(yùn)行的順序進(jìn)程組成，每個(gè)進(jìn)程不能對(duì)其他進(jìn)程的變量賦值。一個(gè)進(jìn)程是一序列的動(dòng)作，由相互影響的不同成分組成，每個(gè)或者一系列動(dòng)作是

39、一個(gè)事件，CSP的進(jìn)程通過通信與其它進(jìn)程或者環(huán)境進(jìn)行交互。因此CSP主要是對(duì)進(jìn)程進(jìn)行刻畫。可見的動(dòng)作有若干種，所有動(dòng)作的集合是∑。CSP的基本算子見表2-1。</p><p>　　每個(gè)進(jìn)程都由自己的軌跡，進(jìn)程的軌跡模型是描述進(jìn)程的重要手段，某個(gè)進(jìn)程的一個(gè)有限軌跡實(shí)際上是這個(gè)進(jìn)程通信至某個(gè)時(shí)刻為止發(fā)生的可見事件的序列，CSP的進(jìn)程進(jìn)程的軌跡模型即是它的軌跡集合。</p><p>　　利用CS

40、P描述協(xié)議的時(shí)候，主要是描述協(xié)議參與者的進(jìn)程，描述入侵者的進(jìn)程，然后將這些進(jìn)程并行起來，構(gòu)成了一個(gè)系統(tǒng)的進(jìn)程。然后再進(jìn)一步描述該系統(tǒng)所要滿足的安全屬性，最后來驗(yàn)證其是否滿足。</p><p>　　表2-1 CSP的基本算子</p><p><b>　　FDR</b></p><p>　　FDR（Failures-Divergence Refi

41、nement）是基于CSP的一個(gè)模型檢測(cè)工具，通過檢測(cè)系統(tǒng)的狀態(tài)，用來測(cè)試一個(gè)系統(tǒng)精簡(jiǎn)后是否滿足所要驗(yàn)證的性質(zhì)。FDR支持CSP的幾種模型：traces model、stable failures model 、failures/divergences model、refusal testing model、revivals model以及priority model。在檢測(cè)過程中，對(duì)不滿足描述的例子，將會(huì)給出一個(gè)反例。</p&g

42、t;<p>　　基于有向圖的網(wǎng)絡(luò)協(xié)議建模</p><p>　　網(wǎng)絡(luò)協(xié)議攻擊發(fā)現(xiàn)和分析架構(gòu)</p><p>　　網(wǎng)絡(luò)協(xié)議攻擊發(fā)現(xiàn)和分析的架構(gòu)圖如圖3-1所示：</p><p>　　圖3-1 網(wǎng)絡(luò)協(xié)議的攻擊發(fā)現(xiàn)和分析的構(gòu)架圖</p><p>　　網(wǎng)絡(luò)協(xié)議攻擊發(fā)現(xiàn)和分析主要包括三個(gè)部分：網(wǎng)絡(luò)協(xié)議知識(shí)，規(guī)則知識(shí)庫，以及分析推理系統(tǒng)。輸

43、入為網(wǎng)絡(luò)協(xié)議相關(guān)內(nèi)容，輸出為針對(duì)該網(wǎng)絡(luò)協(xié)議的攻擊方法和攻擊方法的緩和方案。包括的三個(gè)部分：</p><p><b>　　網(wǎng)絡(luò)協(xié)議知識(shí)：</b></p><p>　　為攻擊發(fā)現(xiàn)和分析理論的數(shù)據(jù)源，主要為RFC所聲明的網(wǎng)絡(luò)協(xié)議以及實(shí)現(xiàn)這些網(wǎng)絡(luò)協(xié)議的應(yīng)用。網(wǎng)絡(luò)協(xié)議知識(shí)是理論的數(shù)據(jù)基礎(chǔ)。</p><p><b>　　規(guī)則知識(shí)庫：</b&

44、gt;</p><p>　　通過對(duì)網(wǎng)絡(luò)協(xié)議知識(shí)的分類整理、提煉和抽象，提取出網(wǎng)絡(luò)協(xié)議相關(guān)的協(xié)議資源庫、行為庫和規(guī)則庫。協(xié)議資源庫包括網(wǎng)絡(luò)協(xié)議中涉及的網(wǎng)絡(luò)數(shù)據(jù)，如一個(gè)IP地址，一個(gè)報(bào)文，服務(wù)器的進(jìn)程池等；行為庫為網(wǎng)絡(luò)協(xié)議相關(guān)的組件和應(yīng)用進(jìn)行的交互，如驗(yàn)證報(bào)文，應(yīng)答報(bào)文等；因?yàn)樵诰W(wǎng)絡(luò)組件進(jìn)行交互的過程中，往往會(huì)涉及一部分的網(wǎng)絡(luò)數(shù)據(jù)，所以網(wǎng)絡(luò)行為往往伴隨有網(wǎng)絡(luò)資源，并且行為之間可能有推算關(guān)系，即某些網(wǎng)絡(luò)行為通過AND和

45、OR關(guān)系能夠推理出下一步的行為，而規(guī)則庫就是用來對(duì)這兩部分的內(nèi)容進(jìn)行描述。</p><p><b>　　分析推理系統(tǒng)： </b></p><p>　　分析和推理系統(tǒng)輸入規(guī)則知識(shí)庫的數(shù)據(jù)知識(shí)，將這些知識(shí)進(jìn)行建模，通過對(duì)模型的分析和推理，能夠推理出網(wǎng)絡(luò)協(xié)議相關(guān)的攻擊方式，并且通過規(guī)則的不斷完善和改進(jìn)迭代，最后得到針對(duì)協(xié)議的攻擊方法，通過規(guī)則知識(shí)庫中的資源和行為形式化定義，

46、將這些攻擊方法進(jìn)行形式化。</p><p><b>　　網(wǎng)絡(luò)協(xié)議建模</b></p><p>　　網(wǎng)絡(luò)協(xié)議的模型為帶有網(wǎng)絡(luò)相關(guān)特性的擴(kuò)展有向圖G(V,E)，擴(kuò)展有向圖的節(jié)點(diǎn)為分析的網(wǎng)絡(luò)行為庫中的內(nèi)容，每個(gè)節(jié)點(diǎn)上帶有若干相關(guān)的網(wǎng)絡(luò)資源，這些資源可以作為節(jié)點(diǎn)的參數(shù)。有向圖的邊為規(guī)則庫中定義的網(wǎng)絡(luò)協(xié)議之間的推理過程，根據(jù)規(guī)則庫中的定義，每個(gè)邊都有AND或者OR的屬性，用來標(biāo)

47、明節(jié)點(diǎn)之間進(jìn)行推理關(guān)系。根據(jù)規(guī)則知識(shí)庫進(jìn)行建模的模型如圖3-1所示：</p><p>　　圖3-2 網(wǎng)絡(luò)協(xié)議規(guī)則的模型</p><p>　　在圖3-1表述的模型中，通過規(guī)則將行為與資源建立包含關(guān)系，將行為與行為之間建立推理關(guān)系，我們用OR來表示行為之間存在的OR關(guān)系，AND來表示行為之間存在的AND關(guān)系。我們用淺藍(lán)色方形來表示網(wǎng)絡(luò)協(xié)議中基本的網(wǎng)絡(luò)行為，深藍(lán)色方形來表示網(wǎng)絡(luò)協(xié)議中的既定事實(shí)，

48、即任何時(shí)候都默認(rèn)成立。黑色方形來表述協(xié)議相關(guān)的攻擊目標(biāo)，而紅色橢圓來表述該攻擊目標(biāo)能夠造成的直接危害，這些危害是協(xié)議無關(guān)的。</p><p><b>　　攻擊路徑分析過程</b></p><p>　　首先從網(wǎng)絡(luò)協(xié)議進(jìn)行總結(jié)和分析，提取出網(wǎng)絡(luò)協(xié)議所涉及的資源，行為和危害；然后對(duì)這些知識(shí)進(jìn)行細(xì)粒度的建模，形成攻擊規(guī)則圖，通過對(duì)模型的分析和推理，能夠獲取針對(duì)網(wǎng)絡(luò)協(xié)議的攻擊方

49、式；再然后是進(jìn)行逆向驗(yàn)證，把所有節(jié)點(diǎn)上的可選參數(shù)選擇并組合，推理所有的攻擊模式，即對(duì)所有可能的攻擊路徑進(jìn)行搜索，這樣就有可能發(fā)現(xiàn)新的攻擊路徑或攻擊模式，整個(gè)過程是一個(gè)迭代的過程，對(duì)新發(fā)現(xiàn)的攻擊模式重新總結(jié)和建模，以完善規(guī)則知識(shí)庫；最后當(dāng)?shù)^程完成以后，對(duì)分析得到的攻擊模式進(jìn)行形式化并建立緩和方案，將這些數(shù)據(jù)保存到安全知識(shí)庫中并生成安全報(bào)告。</p><p><b>　　具體的步驟是：</b>

50、;</p><p>　　1) 從網(wǎng)絡(luò)協(xié)議中總結(jié)所涉及的資源，行為和危害。網(wǎng)絡(luò)協(xié)議由于其功能不同而千差萬別，網(wǎng)絡(luò)攻擊也因此而各式各樣，但是許多攻擊的思路是相似的，所采用的攻擊方法是相近的，可以被抽取為數(shù)量較少的攻擊模式，同樣道理，由于網(wǎng)絡(luò)協(xié)議所使用的資源、發(fā)出的動(dòng)作和攻擊造成的危害的類型數(shù)量有限，為我們對(duì)協(xié)議和攻擊模式的建模提供了可能性。在本論文中，由于時(shí)間原因，只分析了BGP協(xié)議，能夠總結(jié)的內(nèi)容有限，可能使得我們

51、后面所做的推理的效果不是很好，如果能夠分析網(wǎng)絡(luò)中的多數(shù)協(xié)議，推理的結(jié)果應(yīng)該能夠得到很多的提升。</p><p>　　2) 對(duì)規(guī)則知識(shí)庫建模，根據(jù)規(guī)則知識(shí)庫中的規(guī)則，將網(wǎng)絡(luò)資源，行為，危害等信息進(jìn)行組合進(jìn)行細(xì)粒度的建模，主要的工作是形成攻擊規(guī)則圖，在圖3-1中行為是圖中的節(jié)點(diǎn)，資源作為可選參數(shù)加入到行為中。建模后的規(guī)則圖可以理解為多個(gè)攻擊模式的抽象，圖中的參數(shù)確定的路徑都是潛在的攻擊模式。抽取的規(guī)則和分析過的行為、

52、行為被存儲(chǔ)到規(guī)則知識(shí)庫當(dāng)中，作為推理步驟的支持。</p><p>　　3) 逆向驗(yàn)證，完善知識(shí)庫。攻擊規(guī)則圖中許多行為在不同的資源條件下會(huì)有不同的效果，由于行為對(duì)應(yīng)節(jié)點(diǎn)和資源對(duì)應(yīng)參數(shù)，所以對(duì)圖中所有節(jié)點(diǎn)的可選參數(shù)依次選擇，它們的組合就是所有的潛在的攻擊的可能。我們用自動(dòng)推理的方式對(duì)所有的攻擊可能進(jìn)行搜索。對(duì)于新發(fā)現(xiàn)的攻擊模式，使用迭代的方式對(duì)其重新總結(jié)，建模和推理。這樣就使得所建立的規(guī)則知識(shí)庫更加完善，增強(qiáng)了其推

53、理能力。</p><p>　　4) 攻擊模式形式化。迭代過程完成以后，即不能再發(fā)現(xiàn)新的攻擊模式，就可以認(rèn)為已經(jīng)利用現(xiàn)有的知識(shí)發(fā)現(xiàn)了所有可能的攻擊模式，并把攻擊模式進(jìn)行形式化表示。</p><p>　　針對(duì)BGP的建模和攻擊分析案例</p><p>　　BGP（Border Gateway Protocol）是一種自治系統(tǒng)間的動(dòng)態(tài)路由發(fā)現(xiàn)協(xié)議，它的基本功能是在自治系統(tǒng)

54、間自動(dòng)交換無環(huán)路的路由信息，通過交換帶有自治系統(tǒng)號(hào)（AS）序列屬性的路徑可達(dá)信息，來構(gòu)造自治區(qū)域的拓?fù)鋱D，從而消除路由環(huán)路并實(shí)施用戶配置的路由策略。與OSPF和RIP 等在自治區(qū)域內(nèi)部運(yùn)行的協(xié)議對(duì)應(yīng)，BGP是一類EGP（Exterior Gateway Protocol）協(xié)議，而OSPF和RIP等為IGP（Interior Gateway Protocol）協(xié)議。BGP協(xié)議經(jīng)常用于ISP之間。</p><p>　

55、　通過對(duì)網(wǎng)絡(luò)協(xié)議RFC文檔的閱讀與分析，需要得出它的資源表、行為表、危害表，并且總結(jié)出規(guī)則表。經(jīng)過對(duì)BGP有關(guān)文檔的分析與總結(jié)，得出了相關(guān)的協(xié)議內(nèi)容。</p><p><b>　　BGP協(xié)議資源分析</b></p><p>　　BGP中，基本資源見表3-3，主要包括：</p><p>　　網(wǎng)絡(luò)環(huán)境，即協(xié)議所處的環(huán)境；</p>&l

56、t;p>　　網(wǎng)絡(luò)信息包，即協(xié)議傳遞信息包的統(tǒng)稱；</p><p>　　網(wǎng)關(guān)IP，客戶端IP地址，指的是相關(guān)路由器的IP地址；</p><p>　　MAC地址，相關(guān)主機(jī)的MAC地址；</p><p>　　中央處理器，是相關(guān)主機(jī)的CPU；</p><p>　　路由，即協(xié)議之間交換的路由；</p><p>　　網(wǎng)絡(luò)帶寬

57、，協(xié)議通信的帶寬；</p><p>　　BGP報(bào)文，該協(xié)議所傳遞的報(bào)文，有四種：OPEN、UPDATE、KEEPALIVE</p><p>　　NOTIFICATION；</p><p>　　UPDATE報(bào)文中路由屬性、網(wǎng)絡(luò)可達(dá)信息、撤銷路由，這些是UPDATE報(bào)文中的內(nèi)容，UPDATE是幾種報(bào)文中最重要的報(bào)文，路由的增刪改都是通過該報(bào)文，所以報(bào)文中的屬性會(huì)影響路由

58、的變化，這些屬性也將作為協(xié)議的基本資源，他們的變化對(duì)協(xié)議的行為有重要影響。</p><p>　　表3-3 BGP中網(wǎng)絡(luò)資源表</p><p><b>　　BGP協(xié)議行為分析</b></p><p>　　BGP所涉及的行為見表3-4，其中參數(shù)指的是該行為可能包括的資源，主要包括：</p><p>　　不可靠的資源或環(huán)境：

59、是指協(xié)議所處的環(huán)境不安全、不可靠，肯那個(gè)導(dǎo)致報(bào)文不安全。</p><p>　　生成報(bào)文：指發(fā)送發(fā)對(duì)報(bào)文生成報(bào)文并進(jìn)行封裝，待發(fā)送。</p><p>　　安全驗(yàn)證：對(duì)傳遞的報(bào)文進(jìn)行驗(yàn)證。</p><p>　　虛假信息：指的是一個(gè)虛假動(dòng)作，可能包括虛假包，也可能有虛假路由，虛假的資源</p><p>　　接收?qǐng)?bào)文：接收所發(fā)來的報(bào)文</p&g

60、t;<p>　　報(bào)文過濾：對(duì)所發(fā)來的報(bào)文進(jìn)行過濾</p><p>　　資源耗盡：指主機(jī)的內(nèi)存或CPU資源耗盡</p><p>　　拒絕服務(wù)：是一種造成攻擊的行為</p><p>　　發(fā)送報(bào)文：發(fā)送端發(fā)送報(bào)文</p><p>　　連接沖突：當(dāng)兩邊同時(shí)建立TCP連接的時(shí)候會(huì)出現(xiàn)連接沖突</p><p>　　T

61、CP連接成功：雙方主機(jī)成功建立連接</p><p>　　產(chǎn)生回路：收到UPDATE的AS號(hào)產(chǎn)生回路</p><p>　　刪除可用路由：在UPDATE有要?jiǎng)h除的路由，但是有些路由可用有的不可用。</p><p>　　關(guān)閉連接并釋放資源，刪除路由：當(dāng)連接被關(guān)閉后，所有的資源會(huì)被釋放，雙方所交換的路由也將會(huì)被刪除。</p><p>　　選擇錯(cuò)誤路由

62、：當(dāng)UPDATE報(bào)文有粗的時(shí)候，會(huì)影響路由的選擇結(jié)果，選擇根本不能到達(dá)的路由</p><p>　　選擇費(fèi)最有路由：當(dāng)報(bào)文有誤的時(shí)候，可能性選擇的路由并非最優(yōu)</p><p>　　表3-4 BGP中網(wǎng)絡(luò)行為表</p><p>　　BGP協(xié)議危害與行為規(guī)則分析</p><p>　　在BGP行為中，有部分屬于攻擊目標(biāo)，攻擊目標(biāo)就是可以直接導(dǎo)致攻擊

63、危害的行為，其中包括：選擇錯(cuò)誤路由，選擇非最優(yōu)路由，資源耗盡，連接沖突，產(chǎn)生回路，刪除可用路由，關(guān)閉連接釋放資源。攻擊目標(biāo)可能產(chǎn)生的危害見表3-5：</p><p>　　表3-5 BGP中攻擊危害表</p><p>　　資源表、行為表以及危害表是BGP協(xié)議中的基本元素，在此基礎(chǔ)上，需要將這三部分進(jìn)行組合建模，表3-6是分析后的行為之間推導(dǎo)規(guī)則：</p><p>　

64、　表3-6 BGP中行為規(guī)則表</p><p>　　規(guī)則圖以及攻擊路徑分析</p><p>　　在前面的基礎(chǔ)上，我們將資源、行為、以及危害結(jié)合規(guī)則得出該協(xié)議的規(guī)則圖：</p><p>　　圖3-7 BGP攻擊發(fā)現(xiàn)和分析規(guī)則圖</p><p>　　通過以上規(guī)則圖的分析和處理，我們可以得到以下攻擊方法：</p><p>

65、;　　圖3-7 攻擊方法1</p><p>　　如上圖所示，攻擊者如果可以攔截到傳遞中的包，則會(huì)對(duì)截獲的包進(jìn)行修改。這樣在接收端如過收到相應(yīng)的報(bào)文，其中的某些參數(shù)被修改，最終導(dǎo)致危害。攻擊步驟主要有：</p><p>　　攻擊者截獲相應(yīng)的報(bào)文</p><p><b>　　修改報(bào)文的一些參數(shù)</b></p><p>　　然

66、后接收端收到相應(yīng)的報(bào)文</p><p>　　如果修改的是UPDATE報(bào)文中的 withdrawn routes域，此時(shí)接收方收到后，會(huì)對(duì)該域中的路由刪除，這樣可能會(huì)導(dǎo)致刪除正確的路由，最終會(huì)網(wǎng)絡(luò)中斷。</p><p>　　圖3-7 攻擊方法2</p><p>　　如上圖所示，BGP工作過程中，通常雙方主機(jī)端沒有相應(yīng)的認(rèn)證機(jī)制，如果一方收到的報(bào)文沒有經(jīng)過驗(yàn)證，那么所得

67、到的報(bào)文就是不可靠的，接收到的包中所包含的BGP報(bào)文（四種報(bào)文）就是不可靠的，可能被修改過，也可能是虛假報(bào)文。其攻擊步驟主要是;</p><p>　　攻擊者偽造BGP報(bào)文</p><p><b>　　修改其中的網(wǎng)絡(luò)參數(shù)</b></p><p><b>　　另一端接收到該報(bào)文</b></p><p>

68、　　若此時(shí)另一端收到了非預(yù)期的報(bào)文，此時(shí)接收端會(huì)斷開雙方的TCP連接，釋放所有的BGP資源，刪除相關(guān)的路由，最終會(huì)導(dǎo)致這些正確的路由不可用，結(jié)果會(huì)導(dǎo)致網(wǎng)絡(luò)中斷或者網(wǎng)絡(luò)擁塞。</p><p>　　由于在各個(gè)節(jié)點(diǎn)中有許多的參數(shù)，我們通過以上的兩種規(guī)則圖還可以找到許多攻擊方法，這里只列出其中的兩個(gè)。</p><p><b>　　攻擊路徑的規(guī)范描述</b></p>

69、<p>　　經(jīng)過分析后，我們得到了資源表、行為表、危害表、規(guī)則表以及規(guī)則圖，規(guī)則圖中有很多攻擊路徑，按照上節(jié)描述的方法，我們一個(gè)發(fā)現(xiàn)28條攻擊路徑，我們需要對(duì)其進(jìn)行形式化描述，以便計(jì)算機(jī)可以識(shí)別。下面列出5條示例路徑。</p><p>　　1.Encapsulate(Packet)[true];Untrustworthy(Environment)[true];->Untrustworthy(P

70、acket)</p><p>　　Untrustworthy(Packet)[true];Contain(BGP OPEN)[true];->Untrustworthy(BGP OPEN)</p><p>　　Untrustworthy(BGP OPEN)[true];->Fake(BGP OPEN)</p><p>　　TcpConnected(nul

71、l)[true];Fake(BGP OPEN)[true];->ConCollision(null)</p><p>　　詳細(xì)描述：在不安全的環(huán)境下生成報(bào)文，若此報(bào)文包含BGP OPEN，則會(huì)導(dǎo)致不可靠的、虛假的BGP OPEN報(bào)文，由于BGP OPEN會(huì)表示一條TCP的成功建立，若此時(shí)已經(jīng)有一條正常TCP建立，則會(huì)導(dǎo)致連接沖突。</p><p>　　2.Encapsulate(Pa

72、cket)[true];Untrustworthy(Environment)[true];->Untrustworthy(Packet)</p><p>　　Untrustworthy(Packet)[true];Contain(AS_PATH)[true];->Untrustworthy(AS_PATH)</p><p>　　Untrustworthy(AS_PATH)[tr

73、ue];->Fake(AS_PATH)</p><p>　　Fake(AS_PATH)[true];->loop(null)</p><p>　　詳細(xì)描述：在不安全的環(huán)境下生成報(bào)文，若報(bào)文中含有UPDATE報(bào)文，則AS_PATH屬性可能被修改，此時(shí)會(huì)導(dǎo)致虛假的AS_PATH屬性，所以接收方會(huì)發(fā)現(xiàn)可能有回路。</p><p>　　3．Encapsulate

74、(Packet)[true];Untrustworthy(Environment)[true];->Untrustworthy(Packet)</p><p>　　Untrustworthy(Packet)[true];Contain(Withdrawn routes)[true];->Untrustworthy(Withdrawn routes)</p><p>　　Untr

75、ustworthy(Withdrawn routes)[true];->Fake(Withdrawn routes)</p><p>　　Fake(Withdrawn routes)[true];->DeleteRoute(null)</p><p>　　詳細(xì)描述：在不安全的環(huán)境下生成報(bào)文，若報(bào)文中含有UPDATE報(bào)文，則參數(shù)Withdrawn routes可能被修改，此時(shí)會(huì)導(dǎo)

76、致虛假的Withdrawn routes屬性，接收方收到后會(huì)根據(jù)該屬性刪除某些路由，最終導(dǎo)致刪除正確的路由。</p><p>　　4.Untrustworthy(Environment)[true];Authenticate(Packet)[false];TransitPacket(Packet)[true];->Untrustworthy(Packet)</p><p>　　Unt

77、rustworthy(Packet)[true];Contain(BGP OPEN)[true];->Untrustworthy(BGP OPEN)</p><p>　　Untrustworthy(BGP OPEN)[true];->Fake(BGP OPEN)</p><p>　　Fake(BGP OPEN)[true];->Release(null)</p>

78、;<p>　　詳細(xì)描述:在不安全并且未進(jìn)行安全驗(yàn)證的情況下傳遞報(bào)文，此時(shí)若報(bào)文是BGP OPEN報(bào)文，則在不合適的時(shí)間得到非預(yù)期的OPEN報(bào)文，最終導(dǎo)致關(guān)閉該連接，釋放資源并刪除相關(guān)路由</p><p>　　5.Untrustworthy(Environment)[true];Authenticate(Packet)[false];TransitPacket(Packet)[true];->U

79、ntrustworthy(Packet)</p><p>　　Untrustworthy(Packet)[true];Contain(NLRI)[true];->Untrustworthy(NLRI)</p><p>　　Untrustworthy(NLRI)[true];->Fake(NLRI)</p><p>　　Fake(NLRI)[true];-

80、>ChooseWorseRoute(null)</p><p>　　詳細(xì)描述：在不安全并且未進(jìn)行安全驗(yàn)證的情況下傳遞報(bào)文，此時(shí)若報(bào)文中由NLRI（網(wǎng)絡(luò)可達(dá)信息）屬性，則該屬性可能已被修改，虛假的NLRI屬性最終導(dǎo)致選擇錯(cuò)誤的路由。</p><p>　　基于規(guī)則庫的網(wǎng)絡(luò)協(xié)議的攻擊發(fā)現(xiàn)</p><p>　　分別將分析的資源、行為、危害以及規(guī)則入庫，然后基于規(guī)則庫來

81、匹配協(xié)議設(shè)計(jì)過程中順序圖表達(dá)的事件序列，最終發(fā)現(xiàn)協(xié)議的缺陷。架構(gòu)圖見圖3-8。具體說明：</p><p>　　輸入：順序圖和順序圖的Z規(guī)格描述</p><p>　　輸出：攻擊路徑分析報(bào)告</p><p>　　過程：在實(shí)際開發(fā)過程中，①通過順序圖來描述網(wǎng)絡(luò)協(xié)議；②使用Z語言來對(duì)此順序圖進(jìn)行擴(kuò)展描述；③解析該Z規(guī)格，提取出順序圖所表達(dá)的事件序列，④帶入網(wǎng)絡(luò)協(xié)議模型中進(jìn)行

82、推理，找出所有潛在的攻擊路徑；⑤生成攻擊路徑分析報(bào)告。</p><p>　　圖3-8 基于規(guī)則庫的攻擊路徑發(fā)現(xiàn)方法</p><p>　　基于CSP的網(wǎng)絡(luò)協(xié)議建模</p><p><b>　　形式化建模分析</b></p><p>　　從分析角度層面上來分析建模，形式化模型主要有兩個(gè)角度的建模分析：基本模型和攻擊者模型?；?/p>

83、本模型是從網(wǎng)絡(luò)協(xié)議的最初設(shè)計(jì)得來，網(wǎng)絡(luò)協(xié)議的基本要素包括：語法、語義和同步。在建模過程中，語法即是數(shù)據(jù)與控制信息的結(jié)構(gòu)或格式，是基本數(shù)據(jù)，包括協(xié)議的不同報(bào)文、協(xié)議的基本狀態(tài)以及其他事件。語義是需要發(fā)出何種控制信息，完成何種動(dòng)作以及做出何種響應(yīng)，同步是事件實(shí)現(xiàn)順序的詳細(xì)說明，在模型中，語義和同步是協(xié)議中事件的順序序列，協(xié)議的狀態(tài)遷移，我們用CSP的進(jìn)程來描述該元素，進(jìn)程是一個(gè)事件序列，所以這些事件即包括了語義的說明，而且CSP的進(jìn)程是一種

84、有先后順序的序列，因此也可以表達(dá)協(xié)議的同步說明，最終我們通過這樣的模型來對(duì)協(xié)議基本模型進(jìn)行描述。攻擊者模型是攻擊者的一個(gè)進(jìn)程，通過對(duì)協(xié)議的分析，得出攻擊者可能有的能力，例如：竊聽、任意發(fā)布報(bào)文、篡改報(bào)文等。我們將基本模型與攻擊者模型結(jié)合就獲得了現(xiàn)實(shí)環(huán)境下的網(wǎng)絡(luò)協(xié)議的模型。</p><p>　　從模型結(jié)構(gòu)層面，形式化模型主要包括三個(gè)主要內(nèi)容：環(huán)境變量、協(xié)議實(shí)體與系統(tǒng)進(jìn)程。環(huán)境變量為網(wǎng)絡(luò)協(xié)議應(yīng)用和實(shí)施的網(wǎng)絡(luò)環(huán)境，在模

85、型中體現(xiàn)在攻擊者進(jìn)程上；協(xié)議實(shí)體為該網(wǎng)絡(luò)協(xié)議所有的參與實(shí)施者，在模型中體現(xiàn)運(yùn)行該協(xié)議的實(shí)體；系統(tǒng)進(jìn)程可理解為網(wǎng)絡(luò)協(xié)議的實(shí)施行為和實(shí)現(xiàn)步驟，為協(xié)議的基本設(shè)計(jì)內(nèi)容。安全約束是對(duì)模型中三個(gè)方面的限制和約束，也是網(wǎng)絡(luò)協(xié)議需要實(shí)現(xiàn)的安全目標(biāo)，在模型中也屬于一個(gè)進(jìn)程。通過模型檢測(cè)的方法來驗(yàn)證協(xié)議模型是否滿足這些安全約束。</p><p>　　BGP協(xié)議的分析與建模案例</p><p>　　針對(duì)BGP協(xié)

86、議所建立的模型包括進(jìn)行通信的兩個(gè)路由終端，BGP協(xié)議，以及該協(xié)議所處環(huán)境中的攻擊者。下面我們對(duì)這幾部分進(jìn)行介紹。</p><p><b>　　整體模型介紹</b></p><p>　　圖4-1 BGP協(xié)議模型</p><p>　　如圖4-1所示，模型包括：兩個(gè)主機(jī)，Route A和Route B,每個(gè)主機(jī)有運(yùn)行的BGP協(xié)議，以及協(xié)議之間的TC

87、P連接。主機(jī)與協(xié)議之間通過cmd與get通道來通信，而BGP協(xié)議通過通道OpenCon來建立TCP連接，建立好后，他們之間通過tcp通道來進(jìn)行報(bào)文的傳遞。在本協(xié)議中主要側(cè)重于BGP協(xié)議本身，因此我們對(duì)TCP協(xié)議沒有進(jìn)行細(xì)粒度建模，而是假設(shè)TCP協(xié)議處于理想的情況下。另外還有攻擊者模型，在上圖中未進(jìn)行標(biāo)識(shí)，最終的系統(tǒng)是兩個(gè)通信終端與攻擊者之間的進(jìn)程并行運(yùn)行。為了可以用FDR進(jìn)行驗(yàn)證，本文模型代碼滿足于FDR的規(guī)范，下面進(jìn)行詳細(xì)的建模說明：

88、</p><p><b>　　BGP協(xié)議分析</b></p><p>　　圖4-2 BGP狀態(tài)機(jī)</p><p>　　如圖4-2所示，BGP協(xié)議狀態(tài)機(jī)有六個(gè)狀態(tài)，它們之間的轉(zhuǎn)換過程示意了BGP鄰居關(guān)系建立的過程。起初是Idle 狀態(tài)，接收Start事件 ，就進(jìn)入Connect 狀態(tài) ，在Connect 狀態(tài) ，如果Connect- Retry

89、 定時(shí)器超時(shí)，BGP狀態(tài)機(jī)會(huì)停留在Connect 狀態(tài)繼續(xù)試圖建立連接，如果TCP 連接建立失敗，BGP 狀態(tài)機(jī)進(jìn)入Active 狀態(tài)。 如果TCP 連接建立成功，BGP狀態(tài)機(jī)就直接進(jìn)入OpenSent 狀態(tài)。在Active 狀態(tài)，如果TCP 連接依然不能建立起來，那么BGP狀態(tài)機(jī)就會(huì)一直停留在Active 狀態(tài)，直到TCP 連接建立成功，才會(huì)進(jìn)入OpenSent 狀態(tài)。在OpenSent 狀態(tài) ，BGP一旦收到了一個(gè)正確的Open 報(bào)

90、文，就會(huì)進(jìn)入OpenConfirm 狀態(tài)。在OpenConfirm 狀態(tài) ，如果KeepAlive 定時(shí)器超時(shí)，BGP狀態(tài)機(jī)就會(huì)停留在OpenConfirm狀態(tài)。直到BGP收到KeepAlive 報(bào)文，BGP狀態(tài)機(jī)才會(huì)進(jìn)入Established 狀態(tài)。 這時(shí)BGP連接才算建立起來。另外，在除Idle 狀態(tài)以外的其它五個(gè)狀態(tài)出現(xiàn)任何E</p><p>　　以下是六個(gè)狀態(tài)的簡(jiǎn)單介紹：</p><p

91、>　　Idle（空閑）：Idle 是BGP連接的第一個(gè)狀態(tài)，在空閑狀態(tài)，BGP在等待響應(yīng)Start事件，Start事件相應(yīng)以后，BGP初始化資源，啟動(dòng)連接重試計(jì)時(shí)器（Connect-Retry），發(fā)起一條TCP連接，同時(shí)轉(zhuǎn)入Connect（連接）狀態(tài)。</p><p>　　Connect（連接）：在Connect 狀態(tài)，BGP等待TCP連接的建立完成，如果TCP 連接成功，重置連接重試計(jì)時(shí)器，將會(huì)發(fā)送一個(gè)O

92、PEN報(bào)文，轉(zhuǎn)入OpenSent 狀態(tài)，如果TCP 連接失敗，重置連接重試計(jì)時(shí)器，轉(zhuǎn)入Active 狀態(tài)。如果連接重試計(jì)時(shí)器（Connect-Retry）超時(shí)，就重新發(fā)起TCP連接，并繼續(xù)保持在Connect 狀態(tài)，如果有其他錯(cuò)誤產(chǎn)生，將會(huì)退回Idle狀態(tài)。</p><p>　　Active（活躍）：在Active狀態(tài)，BGP總是在試圖建立TCP 連接，如果連接重試計(jì)時(shí)器（Connect-Retry）超時(shí)，就退回

93、到Connect 狀態(tài)，如果TCP 連接成功，重置連接重試計(jì)時(shí)器，將會(huì)發(fā)送一個(gè)OPEN報(bào)文，就轉(zhuǎn)入OpenSent 狀態(tài)，如果TCP 連接失敗，重置連接重試計(jì)時(shí)器，就繼續(xù)保持在Active狀態(tài)，并繼續(xù)發(fā)起TCP連接。如果在該階段收到其他錯(cuò)誤事件，將會(huì)退回到Idle狀態(tài)。</p><p>　　OpenSent（打開消息已發(fā)送）：在OpenSent 狀態(tài)，TCP連接已經(jīng)建立，BGP也已經(jīng)發(fā)送了第一個(gè)Open報(bào)文， B

94、GP就在等待其對(duì)等體發(fā)送Open 報(bào)文。并對(duì)收到的Open報(bào)文進(jìn)行正確性檢查，如果有錯(cuò)誤，系統(tǒng)就會(huì)發(fā)送一條NOTIFICATION消息并退回到Idle狀態(tài)，如果沒有錯(cuò)誤，BGP就開始發(fā)送Keepalive 報(bào)文，并復(fù)位Keepalive 計(jì)時(shí)器，開始計(jì)時(shí)。最后進(jìn)入OpenConfirm狀態(tài)。如果在該階段收到其他錯(cuò)誤事件，將會(huì)退回到Idle狀態(tài)。</p><p>　　OpenConfirm（打開消息確認(rèn)）：在Ope

95、nConfirm狀態(tài)，BGP等待一個(gè)Keepalive 報(bào)文，同時(shí)復(fù)位HoldTimer，如果收到了一個(gè)Keepalive 報(bào)文，就轉(zhuǎn)入Established 階段，BGP鄰居關(guān)系就建立起來了。如果在該階段收到其他錯(cuò)誤事件，將會(huì)退回到Idle狀態(tài)。</p><p>　　Established（連接已建立）：在Established 狀態(tài)，BGP 鄰居關(guān)系已經(jīng)建立，這時(shí)，BGP將和它的鄰居們交換Update 報(bào)文以

96、及KEEPALIVE報(bào)文，收到KEEPALIVE，如果沒錯(cuò)則會(huì)重啟Hold timer，收到Update報(bào)文，重啟Hold timer，并對(duì)其進(jìn)行檢查。其他有誤的事件都會(huì)導(dǎo)致退回Idle狀態(tài)。</p><p><b>　　BGP協(xié)議模型介紹</b></p><p>　　基本數(shù)據(jù)類型與通信通道</p><p>　　我們假設(shè)一個(gè)主機(jī)集合命名為Ho

97、sts，包括所有主機(jī)，在這里包括A和B，并且描述各種報(bào)文的集合為Packet。BgpState表示狀態(tài)的集合。</p><p>　　datatype Hosts=A|B</p><p>　　A與B分別為Route A和Route B</p><p>　　datatype Packet=OPEN |KEEPALIVE| UPDATE|NOTIFICATION |NON

98、E</p><p>　　分別代表了BGP的四種報(bào)文，其中NONE不表示任何報(bào)文，在這里是虛構(gòu)的一個(gè)，為了CSP的語法正確，后面會(huì)進(jìn)行介紹。</p><p>　　datatype BgpState=Idle | Connect| Active| OpenSent| OpenConfirm| Established</p><p>　　分別代表BGP協(xié)議的六種狀態(tài)。&l

99、t;/p><p>　　datatype Command=Start| Stop| TcpConnected | TcpConFailed |TcpConErr |</p><p>　　StartTcpConnection | Ready |ProcessUp |Error</p><p>　　表示主機(jī)應(yīng)用層向協(xié)議發(fā)送與接收的一些命令，包括：?jiǎn)?dòng)、停止事件。由于協(xié)議中不側(cè)

100、重于TCP的建立，因此忽略了TCP的三次握手建模，用TcpConnected來表示連接成功，TcpConFailed表示連接失敗，TcpConErr表示連接出錯(cuò)，StartTcpConnection表示發(fā)起一個(gè)連接，Ready是一種虛擬事件，表示直接進(jìn)入Active狀態(tài)。</p><p>　　channel cmd:Command.Hosts.Hosts</p><p>　　channel

101、 get:Command.Hosts.Hosts</p><p>　　通道cmd與get表示主機(jī)的一條命令，或發(fā)起的一個(gè)事件。以上數(shù)據(jù)類型區(qū)別不同。Hosts通信之間的事件，例如Start.A.B表示A與B通信過程中的Start事件，而不是A與其他主機(jī)。當(dāng)然在本文中只有A與B兩個(gè)。</p><p>　　channel tcp: Hosts.Hosts.Packet.PacketState&

102、lt;/p><p>　　tcp是建立TCP連接的兩個(gè)主機(jī)之間發(fā)送報(bào)文的通道，PacketState表示該報(bào)文是否正確，例如：A.B.UPDATE.correct，則表示A向B發(fā)送了一條沒有錯(cuò)誤的UPDATE報(bào)文。</p><p>　　channel OpenCon:Command.Hosts.Hosts</p><p>　　OpenCon是用來建立連接的通道。表示一個(gè)主

103、機(jī)向另一個(gè)主機(jī)發(fā)送了條命令，建立TCP連接。</p><p><b>　　BGP進(jìn)程建模</b></p><p>　　BGP_STA(id, init_state) =</p><p>　　let otherhost=diff(Hosts,{id})</p><p>　　BGP(id,state,param)=</

104、p><p>　　state==Idle & ((cmd?x?y?z->(</p><p>　　if(x==Start) then OpenCon!StartTcpConnection.id.z-> BGP(id,Connect,z)</p><p>　　else if(x==Ready) then BGP(id,Active,param)</p

105、><p>　　else BGP(id,Idle,param))</p><p><b>　　))</b></p><p><b>　　[]</b></p><p>　　state==Connect &(</p><p>　　(OpenCon?x?y?z->(<

106、;/p><p>　　if(x==TcpConnected and member(y,otherhost) and z==id) then tcp?y.id.OPEN.correct->tcp!id.y.OPEN.correct->get!TcpConnected!y!id->BGP(id,OpenConfirm,y)</p><p>　　else if(x==TcpConEr

107、r and z==id) then OpenCon!StartTcpConnection.id.y->BGP(id,Active,y)</p><p>　　else if(x==Start ) then BGP(id,Connect,param)</p><p>　　else BGP(id,Idle,param))</p><p><b>　　)&l

108、t;/b></p><p><b>　　)</b></p><p><b>　　[]</b></p><p>　　state==Active &((OpenCon?x?y?z->(</p><p>　　if(x==StartTcpConnection and z==id and

109、member(y,otherhost) )then OpenCon!TcpConnected.id.y ->get!TcpConnected!y!id->connected->tcp!id.y.OPEN.correct->BGP(id,OpenSent,y)</p><p>　　else if(x==TcpConnected and member(y,otherhost) and z==

110、id) then tcp?y.id.OPEN.correct->tcp!id.y.OPEN.correct->get!TcpConnected.y.id->BGP(id,OpenSent,y)</p><p>　　else if(x==TcpConErr) then OpenCon!StartTcpConnection.id.y->BGP(id,Active,y)</p>