MANET安全路由協(xié)議自動化分析

毛立強，黃 影

(1. 西安電子科技大學 計算機學院，陜西 西安 710071; 2. 西安文理學院 數(shù)學與計算機工程學院，陜西 西安 710068)

?

MANET安全路由協(xié)議自動化分析

毛立強1，黃 影2

(1. 西安電子科技大學 計算機學院，陜西 西安 710071; 2. 西安文理學院 數(shù)學與計算機工程學院，陜西 西安 710068)

移動ad hoc網(wǎng)絡安全路由協(xié)議已經(jīng)成為一個熱門的研究領(lǐng)域，其中協(xié)議的安全性分析方法及其自動化實現(xiàn)倍受關(guān)注．利用SPIN工具自動分析了SRP和Ariadne協(xié)議，首先通過網(wǎng)絡拓撲建模和自動生成，可以全面分析在不同網(wǎng)絡拓撲下協(xié)議的安全性．再通過節(jié)點丟棄攻擊和協(xié)議建模，自動發(fā)現(xiàn)了針對協(xié)議的有效攻擊，證明基于模型檢測及SPIN工具自動分析安全路由協(xié)議的方法是有效的．

路由協(xié)議;形式化分析;SPIN;模擬模型

移動自組網(wǎng)(Mobile Ad Hoc Networks，MANET)是一個非常復雜的分布式系統(tǒng)，在諸如指揮作戰(zhàn)、會務通信、保障救災、實施危險環(huán)境或遠距離監(jiān)控等無固定網(wǎng)絡設施的環(huán)境中，有著廣泛的應用．安全路由協(xié)議的設計與分析[1]是移動ad hoc網(wǎng)絡中一個熱門的研究領(lǐng)域，目前大部分安全路由協(xié)議分析都是基于直接觀察或者模擬仿真等方法，這些非形式方法缺乏嚴格精確的分析過程，導致協(xié)議設計者宣稱“安全”的路由協(xié)議相繼被發(fā)現(xiàn)仍存在安全漏洞．

近年來有學者開始嘗試MANET安全路由協(xié)議形式化分析方法及其自動化實現(xiàn)的研究．文獻[2]利用Succinct Solver分析安全按需距離矢量路由(Secure Ad hoc On-demand Distance Vector，SAODV)協(xié)議，但有著嚴格的通信環(huán)境假設，不具有通用性．文獻[3]提出了基于演繹證明和反向可達性的分析方法，利用Java開發(fā)了自動化分析工具，發(fā)現(xiàn)了針對安全路由協(xié)議(Secure Routing Protocol，SRP)和Ariadne協(xié)議的攻擊，該方法對網(wǎng)絡拓撲沒有嚴格要求，但其分析過程只適用于一個敵手節(jié)點的情況．文獻[4]基于代數(shù)Petri網(wǎng)，利用模型檢測工具AlPiNA，發(fā)現(xiàn)了針對ad hoc認證路由協(xié)議(Authenticated Routing for Ad-hoc Networks，ARAN)的攻擊，但該分析過程僅針對ARAN協(xié)議，缺乏通用性．文獻[5]利用模型檢測工具AVISPA分析ARAN和endairA協(xié)議，發(fā)現(xiàn)了針對ARAN的3個攻擊方法，未發(fā)現(xiàn)針對endairA的攻擊，但其分析僅限于固定的網(wǎng)絡拓撲．文獻[6]同樣利用AVISPA分析ARAN，試圖分析所有的網(wǎng)絡拓撲和消息交互過程，但沒有很好的解決時間復雜度問題．

與AVISPA類似，簡單進程元語言解釋器(Simple Promela INterpreter，SPIN)是一個用來驗證分布式系統(tǒng)操作的通用模型檢測工具，已經(jīng)成功應用于安全認證協(xié)議的自動化分析及安全環(huán)境下MANET路由協(xié)議性能分析[7-8]．SPIN利用建模語言Promela描述協(xié)議操作和目標，構(gòu)造一個有限狀態(tài)機并進行搜索，以確定目標是否能夠達到．若不能達到目標，SPIN則產(chǎn)生導致目標失敗的事件序列．筆者利用SPIN工具，通過對協(xié)議、攻擊者和網(wǎng)絡拓撲的建模，分析SRP和Ariadne，表明SPIN分析MANET安全路由協(xié)議的有效性．

1 協(xié)議建模

無線ad hoc網(wǎng)絡安全路由協(xié)議的兩個基本目標是正確性和可靠性，前者是指在路由發(fā)現(xiàn)階段，協(xié)議能夠發(fā)現(xiàn)在當時網(wǎng)絡拓撲下確實“存在的”路由; 后者是指在數(shù)據(jù)傳輸階段，協(xié)議能夠識別路由是否失效，并啟動路由發(fā)現(xiàn)過程或者選用其他可用路由．利用基于模型檢測的自動化分析工具，通過對路由發(fā)現(xiàn)過程進行建模分析，驗證是否攻擊者可以破壞路由發(fā)現(xiàn)過程，如果不能成功進行攻擊，則表明協(xié)議是安全的; 如果可以成功進行攻擊，則能夠發(fā)現(xiàn)攻擊步驟和方法．

按需源路由協(xié)議將路由信息嵌入在節(jié)點間互相發(fā)送的路由消息中，其路由發(fā)現(xiàn)過程可以分為路由請求過程和路由回復過程，兩個過程都有可能被攻擊．動態(tài)源路由(Dynamic Source Routing，DSR)是被廣泛研究的按需源路由協(xié)議，SRP和Ariadne都是在DSR基礎(chǔ)上進行安全擴展．假設節(jié)點通信都是雙向的，目標節(jié)點接收到路由請求rreq，通過路由回復rrep返回發(fā)現(xiàn)的路由．通過驗證安全環(huán)境下協(xié)議能夠發(fā)現(xiàn)所有可能的路由，以及協(xié)議安全機制能夠發(fā)現(xiàn)協(xié)議可能受到的攻擊，來證明協(xié)議滿足其安全目標．

DSR只實現(xiàn)了基本的移動路由功能，沒有任何安全機制保護路由發(fā)現(xiàn)過程，其路由發(fā)現(xiàn)過程如下：

rreq process:

◆Initiator node

—Initiate rreq to target

◆Intermediate nodes

—If previously seen rreq→take no action

—Else

◇If not target→append id to path

and retransmit rreq

◇If target→generate rrep rrep process:

◆Target node

—Unicast the rrep

◆Intermediate nodes(along unicast path)

—If not initiator→retransmit rrep

—If initiator→accept route

DSR路由發(fā)現(xiàn)過程的消息格式為_msg_type， initiator， target， id， accum_path．其中msg_type表示消息類型為路由請求或者路由回復; initiator和target表示路由的源節(jié)點和目標節(jié)點; id作為消息惟一標識，保證節(jié)點發(fā)送的rreq為該節(jié)點第一次接收的路由請求; accum_path表示已經(jīng)發(fā)現(xiàn)的節(jié)點路徑，包括路徑上所有中間節(jié)點，當節(jié)點繼續(xù)發(fā)送該路由請求時，節(jié)點路徑被更新，這里所發(fā)現(xiàn)的路由將包括路由源節(jié)點和目標節(jié)點在內(nèi)的路徑上的所有節(jié)點，并允許模型檢測器在分析過程中將該信息與網(wǎng)絡拓撲結(jié)構(gòu)進行比較;增加定義一個位置參數(shù)accum_pos用來跟蹤記錄節(jié)點數(shù)組的當前位置，于是DSR路由消息格式可以建模為_msg_type， initiator， target， accum_path， accum_pos．一旦路由請求到達目標節(jié)點，目標節(jié)點就產(chǎn)生一個路由回復并發(fā)送回源節(jié)點．在路由回復過程中，模型檢測器通過讀取accum_path和accum_pos，決定路由回復消息發(fā)送給接下來哪一個節(jié)點．

SRP對DSR進行了安全擴展，其假設源節(jié)點和目標節(jié)點之間存在安全鏈接，可以共享加密消息認證碼(Message Authentication Code，MAC)，此MAC只能由源節(jié)點或目標節(jié)點進行計算和驗證，中間節(jié)點在路由發(fā)現(xiàn)過程中沒有任何加密機制，與DSR中間節(jié)點的操作相同，路由過程如下:

rreq process:

◆Initiator node

—Compute MAC over initiator， target，Qid，

andQsn

—Initiate rreq to target

◆Intermediate nodes

—If previously seen rreq→take no action

—Else

◇If not target→append id to path

and retransmit rreq

◇If target→take actions below in rreprrep process:

◆Target node

—Validate MAC contained in rreq

—Compute new MAC over initiator， target，

Qid，Qsn， and accumulated path

—Unicast the rrep

◆Intermediate nodes(along unicast path)

—If not initiator→retransmit rrep

—If initiator

◇Validate MAC contained in rrep

◇Accept path if MAC validates

SRP消息格式表示為_ msg_type， initiator， target，Qid，Qsn， MACit， accum_path．其中，參數(shù)Qid和Qsn用來保證路由請求是惟一的，中間節(jié)點可以利用一個布爾參數(shù)判斷其是否多次轉(zhuǎn)發(fā)某一rreq．對于給定的一個路由發(fā)現(xiàn)過程，MAC的計算包含了惟一的Qid和Qsn，所以路由請求過程中加密的MACit可以抵御replay攻擊．因為假設中間節(jié)點不具備攻擊MAC的能力，所以在路由請求過程中不需建模MAC計算過程．然而，在路由回復過程中，需要建模MAC計算過程，以分析可能的針對所發(fā)現(xiàn)路由的攻擊．這樣，也可以減少建模后的狀態(tài)空間．為了能夠分析針對accum_path的攻擊，正確計算并驗證rrep中的MAC，SRP路由消息格式可以建模為_msg_type， initiator， target， accum_path， accum_pos， mac_path．在路由發(fā)現(xiàn)過程中，目標節(jié)點拷貝rreq中收到的路由信息到mac_path變量中，并將其加到rrep中，以此來建模其對所發(fā)現(xiàn)路由進行的MAC計算．根據(jù)假設條件，MAC只能由源節(jié)點和目標節(jié)點計算和驗證，攻擊者不具備破壞MAC的能力，這一點通過不允許模型的中間節(jié)點訪問mac_path來表示．一旦源節(jié)點接收到rrep，通過驗證發(fā)現(xiàn)的路由與mac_path中包含的路由信息的一致性，來判斷是否接受所發(fā)現(xiàn)的路由．

Ariadne協(xié)議也是對DSR的擴展，其安全機制包括每個中間節(jié)點計算每跳單向散列值，保證路由請求安全;附加目標節(jié)點對于所發(fā)現(xiàn)路由的簽名信息，保證路由回復安全．其消息格式為:

_rreq， initiator， target， id， hash_value， accum_path，sig_list，

_rrep， initiator， target， accum_path， sig_list， target_sig．

散列值hx是防止攻擊者從已經(jīng)發(fā)現(xiàn)的路由中刪除某個節(jié)點，每個中間節(jié)點增加其id到accum_path中，計算并插入一個新的每跳散列值hash_value．此外，還計算并附加一個簽名sig_list到完整的消息上，以保證路由只包含可信節(jié)點，節(jié)點x的簽名表示為sigx．一旦目標節(jié)點收到rreq，就對單向散列值進行驗證，如果驗證有效，則目標節(jié)點對發(fā)現(xiàn)的路由進行簽名，并將路由和簽名一起通過rrep返回．在路由回復過程中，中間節(jié)點按照路由上的節(jié)點反向依次發(fā)送路由回復．源節(jié)點通過驗證收到的簽名是否有效，判斷是否接受收到的路由．Ariadne協(xié)議路由發(fā)現(xiàn)過程與DSR類似，只是增加了散列和簽名計算，以及相應的源節(jié)點和目標節(jié)點的有效性驗證，其路由過程如下：

rreq process:

◆Initiator node

—Compute initial hash value over the message

id and initiator-target secret

—Initiate rreq to target

◆Intermediate nodes

—If previously seen rreq→take no action

—Else

◇If not target

Append node_id to path

Calculate new hash value

Attach signature

Retransmit rreq

◇If target→take actions below in rreprrep process:

◆Target node

—Validate one-way hash to detect

path attacks against rreq

—Calculate and attach signature

over the received rreq

—Unicast the rrep

◆Intermediate nodes(along unicast path)

—If not initiator→retransmit rrep

—If initiator

◇Validate node signature to ensure path

only contains insiders

◇Validate target signature to ensure

route not corrupted during rrep

這里把rreq和rrep表示成相同形式，將目標節(jié)點和中間節(jié)點的簽名進行組合，消息結(jié)構(gòu)建模為_msg_type， initiator， target， accum_path， hash_chain， sig_list．需要注意的是，hash_chain和sig_list分別表示加密的單向散列值和簽名列表．對于前者，每個中間節(jié)點都需要增加其id到先前的散列值之后，重新進行散列計算，于是產(chǎn)生了單向散列鏈 hi= H[ni， hn(i-1)]= Hni， H[ni-1，…， H[n0， h0]]，這里i表示rreq中當前節(jié)點，i-1 表示前一節(jié)點．在協(xié)議操作過程中，重新計算的散列鏈包含在每個發(fā)送的消息中，這里將散列計算和散列鏈表示成[ni， ni-1，…， n1， n0]．中間節(jié)點只能轉(zhuǎn)發(fā)整個散列鏈或者附加之前收到的散列鏈重新進行散列計算．與accum_path不同，hash_chain不允許中間節(jié)點修改．當目標節(jié)點收到路由請求時，驗證其中發(fā)現(xiàn)的路由與散列鏈是否匹配．Ariadne協(xié)議通過中間節(jié)點的簽名列表sig_list防止路由中插入外部惡意節(jié)點，源節(jié)點通過簽名驗證接收到的路由．sig_list的表示方式與散列值相同，通過增加節(jié)點id到sig_list來表示對收到的消息進行簽名．sig_list用數(shù)組來表示，其中最后一個元素表示最新的一個用接收到的消息和之前所有簽名信息計算得到的簽名．這里，簽名列表不能被重新排序，但是最后一個簽名可以被丟棄，以表示攻擊者可以丟棄當前所發(fā)現(xiàn)路由中最后一個節(jié)點信息．

綜上，Ariadne建模需要表示路由請求過程中的每跳單向散列值和路由回復過程中保證所發(fā)現(xiàn)路由安全的目標節(jié)點的簽名．目標節(jié)點通過拷貝rreq中所發(fā)現(xiàn)的路由到rrep的簽名中，來表示對接收消息的簽名．路由回復過程中的簽名機制不能被破壞，這樣源節(jié)點就能夠通過簽名來驗證返回的路由，由此發(fā)現(xiàn)針對路由回復過程的攻擊．于是，Ariadne協(xié)議消息格式可以建模為_msg_type， initiator， target， accum_path， accum_pos， crypt_val， hash_pos．其中，accum_pos用來表示內(nèi)部可信節(jié)點增加其id到發(fā)現(xiàn)的路由后的當前位置，hash_pos表示當前路由請求rreq消息中散列鏈的當前位置．數(shù)組crypt_val用來表示散列鏈和目標節(jié)點簽名，在路由請求過程中，代表散列鏈; 在路由回復過程中，代表目標節(jié)點簽名．

2 攻擊者建模

假設攻擊者將主動攻擊路由發(fā)現(xiàn)過程，成功攻擊的結(jié)果使得協(xié)議返回與實際網(wǎng)絡拓撲不一致的路由．針對SRP的攻擊可以考慮節(jié)點丟棄攻擊(Node Drop Attack，NDA)，可以選擇攻擊路由請求過程，使得目標節(jié)點對已經(jīng)破壞的路由計算MAC，源節(jié)點在驗證時，就不會發(fā)現(xiàn)不一致．上述針對SRP的NDA模型能夠利用SPIN完全自動化實現(xiàn)，不需要任何手動交互，具體過程描述如下：

rreq process:

◆If previous node initiator→take no action

◆Else

—Remove previous node id from

accumulated path

—Add own id to path

—Retransmit rreq rrep process:

◆Relay unicast message to all

upstream nodes

在路由請求過程中，攻擊者將當前收到的路由的最后一個節(jié)點信息刪除，用自己的id替換，只要刪除的節(jié)點不是源節(jié)點即可成功．該路由信息到達目標節(jié)點后，MAC依此進行計算．在路由回復過程中，攻擊者轉(zhuǎn)發(fā)rrep給路由上所有的節(jié)點，試圖將該信息發(fā)送給源節(jié)點或者能夠轉(zhuǎn)發(fā)該信息給源節(jié)點的節(jié)點．只要消息能夠被源節(jié)點接收，則攻擊就成功了．

針對Ariadne的攻擊也可以考慮在路由請求過程進行節(jié)點丟棄攻擊．觀察rreq消息結(jié)構(gòu)可以發(fā)現(xiàn)，其中的路由信息是可以修改的，只要相應的散列鏈和簽名與所做修改一致即可．雖然簽名機制使得攻擊者不能改變路由中的節(jié)點順序，也能夠防止路由中插入外部節(jié)點，但是惡意的內(nèi)部節(jié)點還是可以在當前路由最后位置插入或者丟棄一個節(jié)點，惡意的外部節(jié)點就只能丟棄最后一個節(jié)點．下面描述一個惡意內(nèi)部節(jié)點針對Ariadne的NDA過程，如果攻擊者直接收到源節(jié)點的rreq，就將散列值存儲下來，不進行任何其他操作，一旦收到其他中間節(jié)點的rreq，則先存儲這個節(jié)點的散列值，并與之前存儲的散列值進行比較，以便形成可以用來攻擊所必需的信息．

rreq process:

◆If previous node initiator→store hash value

◆Else

—store hash value

—if a hash is known for any upstrorm node in

the embedded path

◇Drop previous node and add own id to path

◇Compute hash value to match current path

◇Retransmit changed rreqrrep process:

◆Relay unicast message to all upstream nodes

3 SPIN運行實例

利用SPIN實現(xiàn)針對Ariadne協(xié)議的NDA模型．系統(tǒng)中定義了一個反映當前網(wǎng)絡拓撲結(jié)構(gòu)的連通性數(shù)組，當發(fā)起路由發(fā)現(xiàn)過程的源節(jié)點接收到返回的路由時，將路由節(jié)點列表與該數(shù)組進行比較，如果驗證失敗，SPIN則產(chǎn)生一個異常警告并終止運行，同時生成一個文件用來記錄導致失敗的消息序列．通過對該序列的分析，可以得到針對協(xié)議的有效攻擊方法．

圖1 Ariadne協(xié)議攻擊序列

給定一個含有5個節(jié)點的網(wǎng)絡拓撲，如圖1所示．0為源節(jié)點，3為目標節(jié)點，4為攻擊者．圖中顯示了一個導致路由失敗的消息序列，節(jié)點4將msg3中的節(jié)點2刪除，將自己id增加到當前的路由中，計算相對應的散列值，形成msg4繼續(xù)發(fā)送．被破壞的路由0-1-4-3通過msg5返回到源節(jié)點0，并將驗證通過．文獻[9]通過模擬模型和直接觀察方法也發(fā)現(xiàn)了同樣的針對Ariadne協(xié)議的攻擊．

4 結(jié) 束 語

MANET安全路由協(xié)議的形式化分析方法受到了越來越多的關(guān)注，也有學者嘗試對協(xié)議進行自動化分析．筆者利用SPIN工具，通過對協(xié)議過程及攻擊者的建模，分析按需源路由協(xié)議SRP和Ariadne，發(fā)現(xiàn)了針對協(xié)議的有效攻擊，表明了SPIN分析移動MANET安全路由協(xié)議的有效性．因為無線環(huán)境下不能保證所有消息都能夠被接收，SPIN需要對攻擊者可能產(chǎn)生的破壞路由發(fā)現(xiàn)過程的所有消息序列進行分析．此外，針對協(xié)議的可能攻擊與協(xié)議本身的漏洞、所分析的網(wǎng)絡拓撲都有關(guān)系，所以分析過程需要針對所有可能的網(wǎng)絡拓撲結(jié)構(gòu)．后續(xù)將對SPIN中如何更好地表示網(wǎng)絡拓撲結(jié)構(gòu)以及如何減少狀態(tài)空間[10]，避免狀態(tài)空間爆炸問題進行研究．

[1] SHARMA S B, CHAUHAN N. Security Issues and Their Solutions in MANET[C]//Proceedings of the 2015 1st International Conference on Futuristic Trends in Computational Analysis and Knowledge Management. Piscataway: IEEE, 2015: 289-294.

[2]NANZ S, HANKIN C. A Framework for Security Analysis of Mobile Wireless Networks [J]. Theoretical Computer Science, 2006, 367(1/2): 203-227.

[3]THONG T V, BUTTYAN L. On Automating the Verification of Secure Ad-hoc Network Routing Protocols[J]. Telecommunication Systems, 2013, 52(4): 2611-2635.

[4]PURA M L, BUCHS D. Model Checking ARAN Ad Hoc Secure Routing Protocol with Algebraic Petri Nets[C]//Proceedings of the 10th IEEE International Conference on Communications. Piscataway: IEEE, 2014: 1-4.

[5]BENETTI D, MERRO M, VIGANO L. Model Checking Ad Hoc Network Routing Protocols: ARAN vs Endair A[C]//Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods. Piscataway: IEEE, 2010: 191-202.

[6]PURA M L, PATRICIU V V, BICA I. Formal Verification of Secure Ad Hoc Routing Protocols Using AVISPA: ARAN Case Study[C]//Proceedings of the 4th Conference on European Computing Conference. Athens: World Scientific and Engineering Academy and Society, 2010: 200-206.

[7]WIBLING O, PARROW J, PEARS A. Automatized Verification of Ad Hoc Routing Protocols[C]//Lecture Notes in Computer Science: 3235. Berlin: Springer Verlag, 2004: 343-358.

[8]ZAIDI F, LALLALI M, MAAG S. A Component Based Testing Technique for a MANET Routing Protocol[C]//Proceedings of the ACS/IEEE International Conference on Computer Systems and Applications. Piscataway: IEEE Computer Society, 2010: 5587040.

[9]ACS G, BUTTYAN L, VAJDA I. Provably Secure On-demand Source Routing in Mobile Ad Hoc Networks [J]. IEEE Transactions on Mobile Computing, 2006, 5(11): 1533-1546.

[10]CORTIER V, DEGRIECK J, DELAUNE S. Analysing Routing Protocols: Four Nodes Topologies Are Sufficient[C]//Lecture Notes in Computer Science: 7215. Berlin: Springer Verlag, 2012: 30-50.

(編輯：王 瑞)

Automated security analysis techniques in MANET routing protocols

MAOLiqiang1，HUANGYing2

(1. School of Computer Science and Technology, Xidian Univ., Xi’an 710071, China; 2. School of Mathematics and Computer Engineering, Xi’an Univ. of Arts and Science, Xi’an 710068, China)

Automated security analysis techniques in Mobile ad hoc network(MANET) routing protocols has become a hot research field. We have developed an automated evaluation process to analyze security properties of SRP and Ariadne. Using the automated security evaluation process, we can produce and analyze all topologies for a given network size. The NDA attackers and routing protocols are modeled in SPIN, and the route corruption attack is found automatically, which indicates the effectiveness of automated analysis of MANET route protocols using SPIN.

routing protocol;formal analysis;simple promela interpreter;simulatability model

2014-09-28

時間：2016-04-01

國家自然科學基金重點資助項目(U1135002)

毛立強(1978-)，男，高級工程師，博士，E-mail: lqmao@xidian.edu.cn．

http://www.cnki.net/kcms/detail/61.1076.tn.20160401.1622.020.html

10.3969/j.issn.1001-2400.2016.06.010

TP393.04

A

1001-2400(2016)06-0056-06