基于模型学习的OpenVPN系统脆弱性分析∗

2019-10-26申莹珠顾纯祥张协力卢政宇

软件学报 2019年12期

申莹珠 , 顾纯祥,2 , 陈熹 , 张协力 , 卢政宇

1(信息工程大学网络空间安全学院,河南郑州 450001)

2(河南省网络密码技术重点实验室,河南郑州 450001)

近年来,网络安全协议相关应用的安全性问题越来越受到重视.2014年,开源加密库OpenSSL的重大安全漏洞“心脏出血”(CVE-2014-0160)引起了业界广泛关注,攻击者可以从服务器内存中读取包括用户名、密码和信用卡号等隐私信息在内的数据,影响波及大量互联网公司.2016年,OpenSSL高危漏洞“DROWN”(CVE-2016-0800)以及2017年的OpenSSL拒绝服务漏洞(CVE-2017-3731)也同样为网络协议的安全性敲响了警钟.因此,如何对网络安全协议的安全性进行评估、尽快尽早发现其协议实现中的脆弱点,保护用户隐私数据安全可靠就显得格外重要.OpenVPN是一款基于OpenSSL库的应用层虚拟专用通道(VPN),在TLS之上建立安全的数据传输隧道,实现身份认证、数据加密、完整性保护和访问控制.OpenVPN在真实网络中被广泛部署且常应用于大型企业之中,对其进行脆弱性分析有着重要的现实意义.

协议脆弱性分析检测技术也叫协议漏洞挖掘技术.传统的漏洞挖掘技术主要依赖于安全人员的人工分析与测试,而模糊测试技术简单、有效、自动化程度比较高,是目前进行安全测试最有效的方法,被广泛应用于Web、系统、应用程序的漏洞挖掘.由于它一般属于黑盒测试,通过构造有效的畸形数据进行测试,因此该技术的代码覆盖率相对较低.2015年,Gascon等人[1]提出了可对私有协议进行态式黑盒模糊测试的PULSAR系统,通过将模糊测试与协议逆向、模拟自动化执行技术结合,提高了协议状态探索空间,能够挖掘协议实现中的深层漏洞;2016年,Ma等人[2]优化测试数据生成方法,提出了使用基于规则的状态机和状态规则树来生成模糊测试的数据,与传统模糊测试方法相比,使用更少的测试数据找到脆弱点,提高了测试效率;2017年,Kang等人[3]提出了一种结合静态分析和动态分析的智能模糊测试系统,在提高检测有效性的同时,减少了误报率和漏报率.

协议状态机推断是脆弱性分析非常关键的内容.2015年,de Ruiter提出了通过模型学习的方法分析具体TLS实现的安全性[4],该方法在仅采用黑盒测试的情况下,应用状态机学习自动推断出了协议实现的状态机,并通过观察推断出来的状态机来检测可能由程序逻辑漏洞引起的异常行为;Beurdouche等人[5]也提出了类似的通过系统测试非正常TLS消息流以检测协议实现中是否存在脆弱性的方法,并在测试中发现了新漏洞.2016年,Ruiter带领团队在其前期工作的基础上继续进行了许多相关研究:Ruiter进一步对过去 14年以来的OpenSSL以及LibreSSL的具体实现进行了并行自动化协议状态模糊测试,通过自动化学习,为145个不同版本的服务器端和客户端构建了状态机,并分析相关实现的安全性[6];Verleg则针对OpenSSH推断出了6个SSH服务器的状态机,验证了协议状态机推断方法的通用性和可行性[7].同年,Somorovsky提出了基于已知漏洞专家库的分阶段模糊测试框架TLS-attacker[8],能够提供简单接口支持定制TLS消息流,并允许任意修改消息中的内容,从而实现对TLS库安全性的评估.2017年,Ruiter团队的Lenaerts[9]对Verleg的方法[7]进行了改进,将Verleg分别对SSH协议的3个子层协议进行模型学习与检测的方法整合为统一的模型学习与检测,提出了对SSH服务器模型进行状态安全检测的新方法;同年,Veldhuizen针对 IPSEC也进行了协议状态机推断并分析[10].Novickis[11]在2016年将模型学习的方法扩展到OpenVPN协议进行研究分析,试图推断出OpenVPN系统的状态机,但在过程中遇到了许多困难最终并未实现目标.

本文基于模型学习的方法,利用协议状态模糊测试技术,对OpenVPN 2.0.9服务器端进行了模型学习和一致性检测,自动推演出目标系统的协议实现状态机,并对其状态机模型进行化简,对其实现逻辑及过程进行详细分析;提出了一种状态机时间压缩模型,与原始状态机及同版本OpenSSL状态机进行对比分析.结果表明:利用经化简后的模型可以更方便迅速地识别协议状态机中正常的和特殊的状态迁移路径,从而提高OpenVPN脆弱性检测与分析的效率.

1 基础知识

1.1 OpenVPN协议

VPN(虚拟专用通道)是企业与企业或者个人与企业之间安全数据传输的隧道,提供了身份认证、数据加密、完整性保护和访问控制安全服务.OpenVPN是一款基于OpenSSL库的应用层VPN实现,由于其简单易用的特性而被广泛部署.OpenVPN依赖OpenSSL的安全性,在客户端和服务器端通过指定端口建立TCP/UDP(一般默认使用UDP)安全隧道,然后在该TLS隧道中加密通信数据,隧道示意如图1所示.

· OpenVPN协议TLS模式下的实现

OpenVPN提供了两种完全不同的认证模式:TLS模式和预共享静态密钥(PSK)模式.预共享静态密钥模式使用预共享静态密钥认证身份并加密.TLS模式采用使用证书的SSL/TLS协议进行身份验证、建立安全隧道、交换对称会话密钥,并使用会话密钥加密数据隧道.TLS模式由于能够保证安全地分发和更新对称密钥,进而在现实应用中具有更强的安全性.因此,本文主要研究基于TLS认证模式的OpenVPN协议.

Fig.1 OpenVPN communication tunnel图1 OpenVPN通信隧道

OpenVPN安全通信过程如图2所示,依赖于以下子协议.

(1) OpenVPN握手协议,类似于TCP的3次握手过程,握手数据包包括:由客户端发起的握手请求数据包P_CONTROL_HARD_RESET_CLIENT_V1/V2(V1/V2代表后续两种不同的密钥协商方式,分别对应PSK认证模式和TLS认证模式,OpenVPN 2.0以上版本默认使用P_CONTROL_HARD_RESET_CLIENT_V2),服务器端的请求响应数据包P_CONTROL_HARD_RESET_SERVER_V1/V2(密钥协商方式与请求一致),客户端对服务器端响应的确认P_ACK_V1;

(2) OpenVPN控制协议,控制协议包括TLS握手和密钥协商两个阶段,封装在P_CONTROL_V1数据包中.当TLS握手完成后,TLS加密隧道已建立,会话密钥协商信息将被封装在TLS记录层中安全传输.需要时,可使用P_CONTROL_SOFT_RESET_V1请求会话密钥冲协商;

(3) OpenVPN记录协议,建立安全隧道和密钥交换完成后,双方进行加密数据通信P_DATA_V1.

Fig.2 OpenVPN communication process in TLS mode图2 TLS模式下OpenVPN通信过程

OpenVPN没有详细的官方规范,2016年,Tomas Novickis方法[11]中给出的在TLS模式下期望的OpenVPN状态机如图3所示.Novickis试图基于LearnLib得出真实的OpenVPN实现的状态机,但其在研究过程中主要遇到了以下困难:(1) 使用python库Scapy可以快速构造数据包,但仅尝试利用之前Wirshark捕获的数据包载荷进行复用,未根据协议原理精心设计每个数据包字段,导致无法通过证书验证或HMAC校验;(2) P_CONTROL_V1数据包载荷较多需要分块传输时还存在一些问题.因此,作者得到OpenVPN实现状态机的目标并未实现.

Fig.3 The expected OpenVPN state machine图3 期望的OpenVPN状态机

1.2 模型学习与一致性检测

为了解决使用常规技术难以分析检测安全协议的具体实现与协议标准之间差异性的问题,采用Angluin的MAT(minimally adequate teachers)框架[12],使用成员查询和等价查询进行模型学习;通过测试查询进行一致性测试,确保模型的推断结果符合要求;最后,进一步分析检测协议实现是否存在脆弱点.在MAT框架中,学习器必须通过询问预言机来推断目标安全协议的状态机.图4为MAT框架示意图.

Fig.4 MAT framework图4 MAT框架

基于MAT框架,模型推断与一致性检测系统可抽象为图5所示,学习器提供了一个可以发送给测试目标(SUT)的消息列表(输入表)以及一条重置测试目标到初始状态的命令.测试程序(test harness)可以将输入表中的抽象消息转换为可以发送给SUT的具体消息,也可以将SUT反馈的响应转换为学习器可识别的抽象消息.因此,测试程序相当于MAT框架中在学习器和预言机之间进行翻译转换的映射器(mapper).而实现测试程序就需要我们知道目标协议使用的具体消息集.

具体过程如下.

a.成员查询:通过发送一系列消息和重置命令,学习器使用如最早由Angluin提出的L*算法[12]、改进L*后去除大量冗余成员查询的TTT算法[13]等经典有限状态机学习算法,通过从SUT返回的响应推断出状态机模型;

b.等价查询:采用近似等价查询算法进行一致性检测,如Chow提出的W-method算法[14]、Ruiter改进的wmethod[4]等.通过有限数量的测试查询,检测该推断是否与实际的状态机等价.如果不等价,将会返回一个反例,学习器使用该反例重新进行推断,即进行模型修正.如果没有找到反例,则认为当前状态机推断近似等价于真实实现,得到协议实现的状态机.

Fig.5 System architecture图5 系统架构

2 基于模型学习的OpenVPN状态机推断

本文在模型学习与一致性检测技术的基础上,基于LearnLib平台[15,16]开发了针对OpenVPN的状态机推断框架,本文只考虑TLS模式下的OpenVPN状态机推断问题.

· 实验环境:Intel core i7-4790处理器、8G内存、Ubuntu 16.04-64位系统、Wireshark软件;

· 协议版本:OpenSSL 1.0.2h,OpenVPN 2.0.9;

· 编程语言:Java,Python;

· 环境配置:采用桥接模式,在两台虚拟机中分别配置本文系统与OpenVPN 2.0.9服务器端环境进行测试.其中,OpenVPN通信采用默认的UDP连接方式(在OpenVPN协议的可靠传输要求下,即使采用TCP连接,也同样需要实现确认机制).

2.1 输入/输出表构造

本文主要测试OpenVPN服务器端状态机,因此根据OpenVPN协议中客户端消息集构造输入表以及服务器端响应消息集构造输出表,输入/输出表的符号表示及消息含义见表1.

Table 1 Symbol representation and message meaning in input/output table表1 输入/输出表符号表示及消息含义

转换程序Test harness基于OpenVPN底层协议,对学习器的消息输入表中的消息进行精心构造,按照学习器中的状态机推断与近似等价算法与测试目标进行交互,并将服务器端返回的响应消息识别、抽象,送入学习器继续分析推断,直到完成真实的OpenVPN服务器端状态机的学习与检测;通过比对协议实现状态机与协议标准状态机(或期望的状态机)之间的差异性,找到可能存在的攻击路径.

2.2 数据包构造及状态机推断策略

网络安全协议的执行路径中往往存在许多条件控制,这也正是限制传统模糊测试进行脆弱性分析检测能力与效率的一个重要方面.因此在状态模糊测试中,数据包构造是整个测试的基础[17].OpenVPN协议中只有正确的证书验证、HMAC校验等才能顺利完成整个连接过程.

本文参考RFC 2246及Wireshark捕获的OpenVPN真实通信数据,精心构造转换程序中使用的数据包,并按照期望的路径进行测试,保证构造的消息集合产生的消息流能够生成正确的执行路径.

在TLS模式下,OpenVPN使用TLS协议认证、建立安全隧道,并交换安全隧道的会话密钥.基于TCP/UDP的OpenVPN报文格式如图6所示.

Fig.6 Message format图6 报文格式

OpenVPN报文主要包括IP头、TCP/UDP头、OpenVPN头和OpenVPN载荷字段.其中,基于TCP和UDP协议的OpenVPN头部有细微差异,UDP包含5位操作码字段以及3位KeyID(密钥标号),基于TCP连接的报文的OpenVPN头部信息还包括16位的包长度字段.本文实验采取OpenVPN默认的基于UDP连接的方式.数据包构造示例如下.

OpenVPN初始化时的第 1个消息是客户端向服务器端请求连接的 PHRCV2(P_CONTROL_HARD_RESET_CLIENT_V2)消息,其操作码为0X07,keyID为0,因此,其VPNType(由5位操作码与3位KeyID串联而成)为MSG_TYPE_P_CONTROL_HARD_RESET_CLIENT_V2=0X38,代码如下:

按照上述方法依次构造数据包,有效性测试结果如图7所示.可以看出,本文构造的数据包在测试中能够突破条件控制的限制.

OpenVPN协议没有标准的协议规范,现有的可参考研究资料很少,系统中映射程序只能根据Wireshark工具捕获真实数据包结合读OpenVPN源码来实现.结合Open VPN系统特点,在状态机推断过程中本文制定以下策略.

(1) OpenVPN按消息生成顺序为数据包编号,因此在进行状态模糊测试的过程中需要正确处理消息序号,否则会造成正确路径难以正常执行;

(2) 为了防止确认机制导致的ACK数据包过多而出现无限状态机,因此在测试程序test harness中每每收到服务器端发回的响应都对其进行确认,且认为状态不改变;

(3) 测试程序每次执行重置reset指令后,为了防止由于异常数据流导致抛出空指针异常,要对所有内部变量进行初始化;

(4) 出于应用场景及安全性考虑,OpenVPN建议默认配置下服务器要对客户端身份进行验证,因此测试程序对TLS中为可选项的客户端证书验证过程进行了实现,同时也对客户端证书为空时服务器端具体实现的逻辑行为进行了测试;

(5) 网络传输消息的拆分与组包,以及对每个拆分后数据包响应的识别;

(6) OpenVPN密钥协商子协议是在TLS加密隧道中完成的,整个过程都为密文封装,因此不再进行后续分析.

Fig.7 Packet construction test图7 数据包构造测试

2.3 状态机推断与化简

实验中,状态机推断采用经典的L*[12]算法,一致性测试采用改进的W[4]方法,用时19小时53分钟,经过76轮次的推断与修正,推演出OpenVPN系统的状态机见附录1.在本文所示的状态机图中,节点代表状态,S0为起始状态,S2为连接关闭状态.边上I/O形式的输入/输出符号对代表输入消息以及目标系统返回的响应消息.如S0→S1,表示向目标OpenVPN系统发送PHRCV2消息后得到响应PHRSV2,由状态S0迁移至状态S1.

推断得到的原始状态机共存在18个不同状态、133条状态迁移,状态迁移数量较多.过于复杂的状态迁移使安全性分析非常困难.对推断出的状态机进一步分析发现:一方面,在TLS隧道建立过程中,任意握手数据包或TLS数据流的错误都会导致连接关闭,产生大量关闭连接的状态迁移;另一方面,由于OpenVPN的确认机制,大量ACK数据包会导致状态机迁移冗余.然而这些状态迁移对协议实现的安全性分析并无影响,因此对原始状态机进行化简:将PCH/CLOSED,PCC/CLOSED,PCKE/CLOSED,PCV/CLOSED,PCCS/CLOSED,PF/CLOSED合并为Other/CLOSED,同时将服务器端接收不同消息并确认合并为状态迁移PF/PACK||PCCS/PACK||PCV/PACK||PCKE/PACK||PCH/PACK(“||”表示或的关系),化简后得到较为清晰简洁的状态机,如图8所示.

Fig.8 The simplified state machine图8 化简状态机

2.4 时间压缩模型

由本文第2.3节中推断并化简后的状态机可以看出:通过模型学习得到的OpenVPN系统状态机,除了正确路径外还存在相似行为路径,这说明状态机在一定程度上可能存在状态及路径的近似等价.由于状态机主要是描述对象在它的生命周期内所经历的状态序列,因此协议状态机也具有时间特性.我们考虑将状态机在时间轴上进行压缩,对比其状态及路径的近似等价部分的差异性.

状态融合技术是状态机推断相关研究中的一部分重要内容.正则语言推断中的RPNI算法[18]可根据样本集构建初始状态机,并不断融合冗余状态,最终推断出与给定样本相一致的有限状态自动机.但该算法在检测候选状态融合正确性时会产生大量的无效主动推断测试请求.因此,Lang等人[19]提出了依据状态之间相似度对候选状态排序的解决方案Blue-Fringe算法.本文借鉴王辰等人[20]对原始的Blue-Fringe算法相似度规则进行扩展的方法,提出状态机时间压缩模型.

由于协议实现都是根据输入消息进行响应的网络交互系统,而协议状态机描述了协议实体间的消息序列及状态迁移,因此特别适合使用确定型的Mealy机来形式化描述协议状态机模型[21].

定义1.协议状态机模型定义为一个六元组M=(Q,I,O,δ,λ,q0),其中,Q为非空有限状态集,I为有限输入符号集,O为有限输出符号集,q0∈Q为初始状态,δ:Q×I→Q为状态迁移函数,λ:Q×I→O为输出函数.

针对协议系统是对一系列通信报文序列进行交互处理的特点,将定义1中的状态转移函数δ和输出函数λ的输入从单个符号i∈I扩展至符号序列w∈I*,对应的输出也为迁移状态序列Q∈O*和输出符号序列μ∈O*.例如:对于状态q1∈Q,输入字符序列w=i1…ik∈I*,输出符号序列μ=λ(q1,w)=o1o2…ok,中间经历的迁移状态Q=q2…qk+1∈O*.

定义2.状态后缀定义为一个输入/输出符号序列集L={l1,l2,…,ln},输入/输出符号序列定义为l=i1/o1i2/o2...ik/ok,其中,in/on∈I/O.

状态后缀是从该状态出发的所有迁移路径上的I/O序列的集合,其代表着该状态对不同的输入序列所响应的输出序列,是该状态可能具有的不同行为的集合.

定义3.两个状态之间的相似度为其最长共同后缀的长度.

根据定义2和定义3,状态后缀描述了一个状态在协议系统中后续可能出现的所有行为特征.相似度就是两个不同状态最长的相同后续I/O序列的长度值,描述了两个状态后续行为特征集合中最为相似的行为路径的相似程度.例如图9所示,S1与S2的最长共同后缀为I4/O4|I5/O5(“|”表示序列符号之间的连接关系),相似度为2.

Fig.9 Example of similarity calculation图9 相似度计算示例

根据定义3可知:相似度可以作为一种衡量标准,表明两个不同状态后续行为的近似程度.相似度越高,两个状态后续的行为集合中就具有越相似的行为.因此,本文考虑压缩协议状态机在时间轴上的近似等价行为,提出时间压缩算法.设定相似度阈值变量depth反映对近似等价状态合并的严苛程度,depth值越大,满足合并条件的状态数越少,说明要求能够合并的状态近似等价程度越高;反之,近似程度越低.

算法1.时间压缩算法.

输入:推断得到的状态机模型SM,相似度阈值depth;

输出:经过状态融合后得到的SM*.

在该算法中需要注意:

·S0为起始状态,不考虑与其他状态的压缩;

· 因状态机存在循环,因此在计算共同后缀时,若遇到已经计算过的状态节点,则其后缀长度不再增加;

· 当两个不同状态经过相同的路径长度后转移到同一状态时,计算的共同后缀长度不再增加;

· 该算法旨在针对状态机时间特性进行压缩,在每轮融合当前状态后,处理后缀迁移路径及状态节点时,只根据输入符号判断是否可合并,从而可能存在一条状态迁移上输入相同输出不同的情况,因此最后得到的是类状态机模型而非严格的Mealy机;

· 虽然depth值越高,合并后不改变其他状态机特性的可能性越大,但由于协议实现过程中的行为路径往往与期望行为路径存在一定差异,depth值过高会导致对特别行为的容忍度降低,可能会出现合并不完全的情况.基于以上考虑,本文取depth值为3.

以本文第2.3节中推演化简得到的状态机作为初始状态机SM,按照算法1对化简状态机进行时间压缩后的模型如图10所示.

Fig.10 Model of the simplified state machine after time compression图10 对化简状态机时间压缩后的模型

3 OpenVPN状态机脆弱性分析

基于模型学习的状态机推断方法通过主动询问的方式,确保了推断结果的正确性,并且基于主动学习型算法L*[15]可以保证推断的状态机是最小且完备的[1].在此基础上,我们对化简状态机与经过时间压缩后的模型进行进一步分析.

3.1 对化简后状态机分析

我们将状态机中的状态变迁称为OpenVPN系统的行为.由图8可以看出,推演并化简后的OpenVPN系统状态机中除了期望的正常行为外,还存在一些比较特别的状态与行为.

· 期望的行为

状态迁移路径:S0→S1→S4→S6→S9→S12→S14→S16,如图8中的虚线所示.

可以发现,S16→S18→S5→S8→S11→S13→S15→S17也是一条成功的加密隧道建立路径.

· 特别的行为

(1) 服务器在收到两次PHRCV2连接请求后,从第3次开始不再回应PHRSV2消息,而是基于OpenVPN协议的确认机制返回PACK消息,因此会形成自循环,如S3,S7,S18,图8中双圆节点.这是由于SSL握手协议需要一个可靠的下层,从而采用确认机制;

(2) 由S7→S5这个状态迁移的过程可以看出:在完成两次加密隧道建立的情况下,发送TLS握手消息都转移到状态S5,此状态可继续顺利完成握手,但双方不再需要进行TLS握手的ClientHello,ServerHello等消息交换;

(3)S1(或S4,S6,S9,S12,S14)→S3→S5→S8→S11→S13→S15→S17也是成功的隧道连接路径,这正是由于特别行为1允许服务器端在收到重复的客户端连接请求PHRCV2后,对服务器端响应两次PHRSV2以确保可靠传输;

(4) 在非正常数据流中,服务器端会对客户端的乱序数据包给予一定程度的确认响应,如经过PCH/PACK,PF/PACK,PCCS/PACK,PCV/PACK,PCKE/PACK等消息对的交互,但当前状态并未发生改变,如S10;

(5) 由于网络传输数据包大小有一定的限制,因此存在消息拆分与组装问题,这就造成了出现类似PCC/PACK|PACK这样的消息对,即,客户端发送的证书被拆分为两个数据包,相应地也就得到了两个服务器端的响应消息;

(6)S18→S5的状态迁移上出现了PCH/DecryptError,这是因为在S18的前一个状态S16已经完成了隧道建立,此时再次发送PHRCV2时会重新请求协商加密隧道,但test harness认为仍在加密隧道中而进行解密,从而出现解密失败.

综合以上分析可以看出,OpenVPN系统实现状态机的特别行为可能导致攻击路径的存在.例如,依据RFC 2246可知:传统的ClientHello,ServerHello消息格式中分别包含了客户端和服务器端产生的随机数random,而在特别行为2中,完成两次加密隧道建立后,再次握手重连时不再进行ClientHello,ServerHello消息交互,这与规范的TLS握手过程不同,导致至少通信双方的随机数没有更新.另一方面,由于OpenVPN缺乏详细的官方规范,前期Novickis[11]在2016年做过相关研究,但其最终也并未实现推断出OpenVPN实现状态机的目标,因此本文推断状态机发现的期望行为和特殊行为,为OpenVPN安全研究提供了参考依据.

3.2 与期望的状态机对比

与第1节基础知识中借鉴的Novickis给出的期望的状态机[14]作比较可以发现:本文测试得到的OpenVPN实现的状态机具有18个不同状态,与期望的状态机相比更为复杂;真实实现的状态机完成隧道建立的路径不止一条,而期望的状态机未考虑OpenVPN确认机制带来的影响;真实实现的状态机在任何时候都接受PHRCV2消息重新建立连接,但期望的状态机只在起始状态接受该连接请求并相应;由于本文测试目标为OpenVPN协议的客户端实现,无法测得服务器端发送P_CONTROL_SOFT_ RESET_V1消息请求与客户端进行重协商的过程,因此不存在期望的状态机中S7→S8的状态迁移.

综上所述,虽然真实测得的状态机较为复杂,但其完整显示了协议实现的重要过程,且根据状态机路径能够得到一些协议实现的具体细节,如服务器端对OpenVPN连接请求响应两次后转为ACK确认.这对于类似缺少协议规范但应用广泛的安全协议的分析具有重要的参考意义.

3.3 与TLS状态机比对

由于OpenVPN安全性是以SSL/TLS加密隧道为基础的,因此将推断得到的OpenVPN 2.0.9系统状态机与其对应的OpenSSL 1.0.2g系统状态机进行对比分析.基于Statelearner开源框架推断出OpenSSL 1.0.2g的状态机如图11所示.由于SSL/TLS协议是基于TCP的可靠连接,握手过程不需要确认机制,因此会出现在发送ClientKeyExchange,ChangeCipherSpec消息时没有收到服务器端的响应(记为Empty),但状态已发生迁移的情况.另一方面,由于TLS协议中用于检测连接是否保持的心跳请求数据包只有在握手阶段完成后才会得到响应,且其会导致出现无限状态机模型[4],会对本文的协议脆弱性分析工作造成困难,且对安全连接阶段的检测分析没有影响,因此在输入表中将其删除.

Fig.11 Server side state machine of OpenSSL 1.0.2g图11 OpenSSL 1.0.2g服务器端状态机

由图8与图11对比可知:虽然OpenVPN基于OpenSSL建立加密隧道进行安全传输,但其由于特有的确认机制以及开发者对于重链接的具体实现,导致其具体实现的状态机较为复杂,且拥有不止一条成功路径,这使得OpenVPN通信双方在后续的数据加密密钥协商及数据加密过程中都存在一定的安全隐患.

由图10与图11对比可知:通过对OpenVPN实现状态机进行时间压缩,期望中应该是相对应版本OpenSSL实现状态机的扩充(如增加OpenVPN连接请求与响应等),且能很清晰地看出不同轮次连接建立中的差异.如S1/S3自循环与S16/S17→S10/S18,这两条状态迁移就是由于加密隧道建立过程中因为连接请求次数不同而响应不同,符合第3.1节中描述的特别行为1.除此之外,还存在S7这样特殊的状态,其产生的原因正是OpenVPN协议对消息拆分产生多次响应,与分析的特别行为5一致.

3.4 对时间压缩模型分析

图10显示了对化简状态机进行时间压缩后的模型中共有11个状态节点、36条不同的状态迁移.与图8化简状态机18个状态节点、50条迁移相比更加精简.但需要注意的是,采用时间压缩算法得到的模型并不是Mealy机.这是由于在时间轴上进行了压缩,可能出现某一状态的状态迁移上输入相同、输出不同,却迁移至同一状态的情况.如图10中的由原状态S1和S3合并得到的节点,其输入PHRCV2消息后,在不同时间点可能得到的响应为PHRSV2或PACK.

· 时间压缩模型对期望的系统行为的刻画

图10中虚线所示路径即为期望中的加密隧道建立路径:

S0→S1/S3→S4/S5→S6/S8→S9/S11→S12/S13→S14/S15→S16/S17,说明该时间压缩模型能够表示推断并化简得到的状态机图中的期望路径.

· 时间压缩模型对系统特别行为的刻画

(1) 对于不同轮次的连接请求PHRCV2,时间压缩模型通过状态合并以及采用集合{PHRSV2,PACK}表示可能收到的响应消息,可以清楚地展示出OpenVPN系统服务器端对PHRCV2消息在不同时间点响应是具有差异性的;

(2) 双圆节点的自循环行为以及S10/S18节点反映了OpenVPN系统的确认机制;

(3)S7,S10,S18等具有特别行为的状态经过时间压缩算法后仍能够很好地保持其特征.

由上面的分析可以看出来:经过时间压缩后的状态机模型合并了对协议进行安全性分析没有影响的近似等价的迁移路径与状态,与原状态机相比更加清晰且能够充分反映出原模型的各种特征——期望的路径与特殊的路径.因此,通过对状态机时间压缩模型所进行的分析,是寻找协议实现中可能存在的攻击路径的一种简单可行的方法.

4 结语

本文主要研究了对网络安全协议的实现逻辑脆弱性进行自动化分析的问题.基于模型学习的方法,对OpenVPN系统实现逻辑进行黑盒测试分析,自动推演出系统的实现状态机,发现了多条期望路径外的特别路径及可能的安全隐患,为目标系统的脆弱性分析和攻击路径发现提供依据,提出了针对协议实现状态机的时间压缩模型及算法,提高了脆弱性分析和攻击路径发现的效率.本文研究成果为大型应用的安全协议的脆弱性分析提供了理论和技术支持.

附录1.