基于符号模型的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.

責任编辑（责任编辑：孙娟）