基于符號模型的Mynah協議安全性自動化分析

李鏡

摘要摘要：Openflow是目前使用最為廣泛的SDN通信協議，由于其協議規范還在不斷完善，因此存在一定的安全隱患，對Openflow協議及其相關應用的安全分析也越來越受到重視。Mynah協議是在Openflow協議的基礎上實現的安全認證協議。對Mynah協議的保密性和認證性進行分析，基于符號模型，利用應用PI演算對Mynah協議進行形式化建模，并使用安全協議分析工具Proverif進行自動化分析。結果表明，Mynah協議并不具備保密性和認證性，為此，給出了Mynah協議中不具備保密性和認證性的解決辦法。

關鍵詞關鍵詞：SDN安全；Openflow協議；應用PI演算；符號模型；自動化分析

DOIDOI：10.11907/rjdk.171200

中圖分類號：TP309

文獻標識碼：A文章編號文章編號：16727800（2017）005016404

0引言

隨著SDN網絡的推廣和應用，其安全問題也日益凸顯。Openflow[1]是2008年由Mcknown教授提出的SDN協議標準，也是目前應用最為廣泛的SDN協議，用以解決傳統TCP/IP網絡架構中存在的性能瓶頸問題[2]。在Openflow協議標準中，采用TLS作為消息加密的手段[3]。然而由于TLS協議本身結構復雜、實現困難，且效率較低，因此在控制器端和設備廠商之間都沒有實現TLS協議，通信消息也未作任何加密處理。在實際網絡環境中，控制器和交換機的連接可能跨越多個物理網絡，硬件和軟件都面臨著各種潛在攻擊[45]，攻擊者可以冒充正常交換機獲取控制器的通信數據，從而攻擊整個網絡[6]。因此，實現控制器和交換機之間的認證性是當務之急。

Mynah[7]協議是2015年提出的輕量級認證協議，旨在解決SDN網絡中數據轉發層面的認證性缺失問題。Openflow協議使用DatapathID對數據通路進行標識，而DatapathID在同一個交換機中可能存在重復，控制器因此產生邏輯錯誤，將同一消息的多個副本發送至DatapathID相同的信道，從而泄露通信數據。Mynah協議利用Openflow現有的消息結構，以DatapathID為基礎生成會話密鑰，并以該會話密鑰作為加密密鑰對Openflow消息進行加密和認證。本文對Mynah協議的安全性進行了全面分析，利用應用PI演算對Mynah協議進行形式化建模[8]，并使用Proverif進行自動化分析[9]，根據分析結果給出了解決方案。

1Mynah消息結構

Mynah協議由4部分組成，分別是：Openflow擴展庫、加密模塊、Mynah控制器模塊、Mynah交換機模塊。Mynah協議消息結構如圖1所示。

1.1交換機和控制器建立連接

如果交換機需要和控制器建立連接，首先需要根據配置項Connection URI中的IP地址、通信端口等信息初始化一個到控制器的TCP連接。連接建立后，交換機和控制器立刻發送一個OPFT_Hello消息給對方，進行協議版本協商。由于Openflow協議仍在不斷更新和完善之中，每一次更新后的協議標準和之前的版本存在較大差異，因此必須統一通信雙方的協議版本，才能進行后續的消息發送。OPFT_Hello消息包含版本參數標識符OFPHET_VERSIONBITMAP，為發送方所能支持的Openflow協議的最高版本。交換機和控制器接收到對方的Hello消息之后，將對方所能支持的最高版本和本地支持的最高版本進行比較，最終以版本較低的一方為最終使用的版本。否則，接收方返回一個Hello Failed錯誤消息并終止該連接。

1.2控制器獲得交換機信息

版本協商完成后，控制器向交換機發送OFPT_FEATURES_REQUEST消息，請求獲得交換機的配置參數和關鍵參數。在SDN網絡架構中，一般由控制器主導通信的相關規則和數據流向，一臺控制器同時管理多個交換機，因此在連接建立過程中需要保存交換機的獨立信息，避免數據發送相互干擾。交換機則應答OFPT_FEATURES_REPLY消息，該消息包含交換機的Datapath ID，作為該數據通路的唯一標識，以及最大緩存數量、最大轉發表數量和最大輔助連接數量等。隨后控制器發送OPFT_Set_Config消息，新增或修改交換機的部分配置參數。

1.3交換機生成會話密鑰

在控制器獲得交換機的DatapathID之后，交換機生成時間戳Timestamp和事務序列Transaction Sequence Number，經過計算后生成會話密鑰Session Key，使用本方公鑰加密，封裝至Echo_Request消息中，發送至控制器。

1.4控制器認證密鑰

控制器收到Echo_request消息，使用私鑰解密獲得Session key并驗證其完整性和合法性，若驗證成功則表明Session key有效，同時控制器應將該Session key中包含的DatapathID與之前接收到的DatapathID進行比對，以確認交換機的身份。最后控制器生成DPID verified消息并封裝至Echo_Reply中，使用Session key加密后續消息，發送至交換機。

2應用PI演算對Mynah協議建模

應用PI演算[10]是用來形式化建模并發進程之間相互通信的形式化語言，它在PI演算的通信與并發結構的基礎上，增加了函數和等式原語。消息不僅只包含名還可以是由函數和名構成的值。應用PI演算使用函數來表示通用的密碼學原語，比如加密、解密、數字簽名等，不需要為每一個密碼操作都構造新的密碼學原語，具有很好的通用性，因此可以對非常復雜的安全協議進行建模和分析。

ProVerif是Blanchet于2001年開發的基于重寫逼近法的一階定理證明器，可以對使用Horn子句或者應用PI演算描述的安全協議進行分析驗證，也可以建模各種密碼學原語，包括共享密鑰密碼學、公鑰密鑰密碼學、數字簽名、哈希函數以及DiffieHellman密鑰交換等。同時，它克服了模型檢測方法固有的缺陷——狀態空間爆炸問題，能夠處理無窮狀態系統。目前，ProVerif已經成功分析了大量的安全協議。

2.1函數與等式理論

建模過程中要使用到函數及等式理論，本文使用應用PI演算來建模Mynah協議。Mynah協議函數及等式理論如圖2所示。

用公鑰PU通過函數fun senc（x，PU）來加密消息x，用公鑰PU 通過函數fun sdec（x，PU）來解密消息x。用公鑰PU通過函數fun aenc（x，PU）來加密消息x，用私鑰PR通過函數fun adec（x，PR）解密消息x。通過函數fun PR（b）接收私有值b作為輸入并產生私鑰作為輸出，同理通過函數fun PU（b）接收共有值b作為輸入并產生公鑰作為輸出。

2.2進程

完整的Mynah協議進程主要包含兩個進程：Switch進程和Controller進程。它們共同構成了主進程，如圖3所示。

交換機進程的形式化建模如圖4所示。首先它通過公開信道c發送helloSwitch消息至Controller進程，然后通過信道c接收從Controller進程接收對等消息helloController，進行消息版本協商。版本確定后，Switch進程通過信道c接收featureRequest消息，生成應答消息featureReply，將自身的DatapathID封裝至featureReply中通過信道c發送至Controller進程。Switch進程接收到該DatapathID之后，Switch進程使用DatapathID，時間戳Timestamp和事務序列xid3生成會話密鑰Session key，使用非對稱加密算法加密后封裝至echoRequest消息中發送至Controller進程。然后從Controller進程接收echoReply消息，使用之前已有的Session key和對稱解密算法解密echoReply消息中的secretMessage部分，若解密成功則通過信道c輸出Finished，至此協議通信結束。

控制器進程的形式化建模如圖5所示。首先它通過公開信道c發送helloController消息至Switch進程，然后通過信道c接收從Switch進程接收對等消息helloSwitch，進行消息版本協商，這一過程與Switch進程類似。版本確定后，Controller進程通過信道c立即發送featureRequest消息，并等待接收Switch進程的應答消息featureReply。在接收到的featureReply消息中，Controller進程獲得發送方Switch進程的DatapathID并保存。然后通過信道c接收Switch進程的echoRequest消息，使用私鑰PR（keyop1）解密Secretkey部分獲得會話密鑰，將會話密鑰中的DatapathID與之前保存的DatapathID作比對驗證。若驗證成功，則使用Sessionkey對參數OPmessage進行加密并封裝至echoReply消息中，通過信道c發送至Switch進程。具體建模代碼如下

3利用ProVerif驗證Mynah協議的認證性

利用PI演算進行安全協議建模時，首先要對事件進行聲明，并給出最終需要明確證明的目標，在ProVerif中使用query attack（OPmessage）來驗證消息項OPmessage的保密性，ProVerif使用非單射一致性來建模認證性，如表1所示，因此使用query ev：e1==>ev：e2來建模認證性，當事件e1執行并且事件e2在其之后執行時結果為真。在表1中，語句ev：endauthcon_s（x）==>ev：beginaauthcon_s（x）用來建模控制器對交換機的認證性，ev：endauthswit_c（x）==>ev：beginaauthswit_c（x）用來建模交換機對控制器的認證性。

表1認證性目標

圖5是ev：endauthcon_s（x）==>ev：beginaauthcon_s（x）的建模認證結果，圖6是ev：endauthswit_c（x）==>ev：beginaauthswit_c（x）的建模認證結果，結果均為false，表明交換機和控制器無法互相認證。經過分析可知，由于采用公鑰加密機制，交換機和控制器擁有相同的會話密鑰，在消息傳遞時沒有采用相應的安全策略，控制器和交換機均可偽造消息項。同時由于生產會話密鑰的數據項均不保密，攻擊者也可以使用同一個DatapathID偽造會話密鑰和控制器進行通信，因此Mynah協議無法解決Datapath Duplication攻擊。可以采用數字簽名機制，在發送加密消息時，使用公鑰PU（sessionkey）對消息項進行簽名，從而解決認證性問題。

4結語

由于Openflow協議本身仍在不斷完善和規范之中，因此協議本身存在較大的安全隱患。Openflow協議規范指出用標準的安全協議如TLS等來解決其安全性。然而，部署TLS協議的開銷比較大、實現復雜，同時也使得通信效率降低。Mynah協議是以Openflow協議的消息結構為基礎而提出的一套實現控制器和交換機認證和消息加密的機制。為了研究Mynah協議的實體之間是否具有認證性以及消息發送的保密性和認證性，本文通過對Mynah協議消息流中的數據項進行分析，得到其整體的消

息結構，然后利用PI演算對Mynah協議進行建模，并將建模語句導入自動化驗證工具Proverif中進行自動化分析。結果表明，Mynah協議能夠確保發送的消息具有保

密性，但通信雙方，即控制器和交換機之間無法相互認證。如果通過數字簽名機制來解決，則不存在認證性的問題，在技術上可以實現，本文也給出了相應的解決方案。

參考文獻參考文獻：

[1]N MCKEOWN，T ANDERSON，H BALAKRISHNAN，et al.OpenFlow： enabling innovation in campus networks[J].ACM SIGCOMM Computer Communication Review，2008，38（2）：6974.

[2]左青云，陳鳴，趙廣松，等.基于OpenFlow的SDN技術研究[J].軟件學報，2013（5）：10781097.

[3]OPEN NETWORKING FOUNDATION.OpenFlow switch specification Version 1.5[EB/OL].https：//www.opennetworking.org.

[4]R KLTI，V KOTRONIS，P SMITH.OpenFlow： a security analysis[C].IEEE International Conference on Network Protocols，2013：16

[5]K BENTON，L J CAMP，C SMALL.OpenFlow vulnerability assessment[C].ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking，ACM，2013：151152.

[6]X WEN，Y CHEN，C HU，et al.Towards a secure controller platform for openflow applications[C].ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking，2013：171172.

[7]JW KANG，SH PARK，J YOU.Mynah： enabling lightweight data plane authentication for SDN controllers[C].International Conference on Computer Communication & Networks，2015：16.

[8]GUANGYE S，MOHAMED M FASER.Formal and automatic security enforcement by rewriting by BPA algebra with test[J].International Journal of Grid and Utility Computing，2013，4（23）：204211.

[9]BLANCHET B.An efficient cryptographic protocol verifier based on prolog rules[C].Proceeding of the 14th IEEE Computer Security Foundations Workshop，Cape Breton，2011：8296.

[10]ABADI M，FOURNET C.Mobile values，new names and secure communication[C].Proceeding of the 28th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages，London，2001：104115.

責任編輯（責任編輯：孫娟）