基于符號模型的Mynah協(xié)議安全性自動(dòng)化分析

李鏡

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

關(guān)鍵詞關(guān)鍵詞：SDN安全；Openflow協(xié)議；應(yīng)用PI演算；符號模型；自動(dòng)化分析

DOIDOI：10.11907/rjdk.171200

中圖分類號：TP309

文獻(xiàn)標(biāo)識(shí)碼：A文章編號文章編號：16727800（2017）005016404

0引言

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

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

1Mynah消息結(jié)構(gòu)

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

1.1交換機(jī)和控制器建立連接

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

1.2控制器獲得交換機(jī)信息

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

1.3交換機(jī)生成會(huì)話密鑰

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

1.4控制器認(rèn)證密鑰

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

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

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

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

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

建模過程中要使用到函數(shù)及等式理論，本文使用應(yīng)用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進(jìn)程

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

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

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

3利用ProVerif驗(yàn)證Mynah協(xié)議的認(rèn)證性

利用PI演算進(jìn)行安全協(xié)議建模時(shí)，首先要對事件進(jìn)行聲明，并給出最終需要明確證明的目標(biāo)，在ProVerif中使用query attack（OPmessage）來驗(yàn)證消息項(xiàng)OPmessage的保密性，ProVerif使用非單射一致性來建模認(rèn)證性，如表1所示，因此使用query ev：e1==>ev：e2來建模認(rèn)證性，當(dāng)事件e1執(zhí)行并且事件e2在其之后執(zhí)行時(shí)結(jié)果為真。在表1中，語句ev：endauthcon_s（x）==>ev：beginaauthcon_s（x）用來建?？刂破鲗粨Q機(jī)的認(rèn)證性，ev：endauthswit_c（x）==>ev：beginaauthswit_c（x）用來建模交換機(jī)對控制器的認(rèn)證性。

表1認(rèn)證性目標(biāo)

圖5是ev：endauthcon_s（x）==>ev：beginaauthcon_s（x）的建模認(rèn)證結(jié)果，圖6是ev：endauthswit_c（x）==>ev：beginaauthswit_c（x）的建模認(rèn)證結(jié)果，結(jié)果均為false，表明交換機(jī)和控制器無法互相認(rèn)證。經(jīng)過分析可知，由于采用公鑰加密機(jī)制，交換機(jī)和控制器擁有相同的會(huì)話密鑰，在消息傳遞時(shí)沒有采用相應(yīng)的安全策略，控制器和交換機(jī)均可偽造消息項(xiàng)。同時(shí)由于生產(chǎn)會(huì)話密鑰的數(shù)據(jù)項(xiàng)均不保密，攻擊者也可以使用同一個(gè)DatapathID偽造會(huì)話密鑰和控制器進(jìn)行通信，因此Mynah協(xié)議無法解決Datapath Duplication攻擊?？梢圆捎脭?shù)字簽名機(jī)制，在發(fā)送加密消息時(shí)，使用公鑰PU（sessionkey）對消息項(xiàng)進(jìn)行簽名，從而解決認(rèn)證性問題。

4結(jié)語

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

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

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

參考文獻(xiàn)參考文獻(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技術(shù)研究[J].軟件學(xué)報(bào)，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.

責(zé)任編輯（責(zé)任編輯：孫娟）