李鏡

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

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

DOIDOI：10.11907/rjdk.171200

中圖分類號：TP309

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

0引言

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

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

1Mynah消息結構

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

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

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

1.2控制器獲得交換機信息

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

1.3交換機生成會話密鑰

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

1.4控制器認證密鑰

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

2應用PI演算對Mynah協(xié)議建模

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

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

2.1函數(shù)與等式理論

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

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

2.2進程

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

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

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

3利用ProVerif驗證Mynah協(xié)議的認證性

利用PI演算進行安全協(xié)議建模時，首先要對事件進行聲明，并給出最終需要明確證明的目標，在ProVerif中使用query attack（OPmessage）來驗證消息項OPmessage的保密性，ProVerif使用非單射一致性來建模認證性，如表1所示，因此使用query ev：e1==>ev：e2來建模認證性，當事件e1執(zhí)行并且事件e2在其之后執(zhí)行時結果為真。在表1中，語句ev：endauthcon_s（x）==>ev：beginaauthcon_s（x）用來建?？刂破鲗粨Q機的認證性，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，表明交換機和控制器無法互相認證。經(jīng)過分析可知，由于采用公鑰加密機制，交換機和控制器擁有相同的會話密鑰，在消息傳遞時沒有采用相應的安全策略，控制器和交換機均可偽造消息項。同時由于生產(chǎn)會話密鑰的數(shù)據(jù)項均不保密，攻擊者也可以使用同一個DatapathID偽造會話密鑰和控制器進行通信，因此Mynah協(xié)議無法解決Datapath Duplication攻擊?？梢圆捎脭?shù)字簽名機制，在發(fā)送加密消息時，使用公鑰PU（sessionkey）對消息項進行簽名，從而解決認證性問題。

4結語

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

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

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

參考文獻參考文獻：

[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，F(xiàn)OURNET C.Mobile values，new names and secure communication[C].Proceeding of the 28th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages，London，2001：104115.

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