基于状态机学习算法的TLS实现库安全性分析
2018-12-10唐朝京
毕 兴,唐朝京
(国防科技大学电子科学学院,湖南 长沙 410073)
0 引 言
传输层安全(transport layer security,TLS)协议用于为网络提供安全及数据完整性保障。作为最广泛使用的安全协议之一,其安全性引起了业界的高度关注,各类研究者及攻击者对其进行了细致深入的分析,它经历了从密码学攻击[1-3]到协议实现库漏洞[4-6]等一系列安全威胁。其中TLS协议实现库作为TLS协议的应用载体,也被看作一个实施网络攻击的重点。因此,对其安全性的分析,有着重大而现实的意义。
传统的TLS协议实现库安全性分析大多立足于程序分析的角度,重在寻找实现库的软件脆弱性,该方法无法发现协议实现中存在的逻辑缺陷。另一方面,通过对协议规范的形式化安全分析又不足以保证其实现库的安全性。
为了描述TLS或一般安全协议的实现库,可以使用有限状态机指定发送和接收的消息的可能序列。使用状态机学习技术,能够仅依赖于黑盒测试,不需要知道协议规范,就可以从协议实现库中提取状态机。通过分析这些状态机,可以发现协议的状态迁移中存在的逻辑错误。
协议状态机学习可以分为被动式学习和主动式学习。文献[7]提出了第一个多项式复杂度的摩尔状态机学习算法,称作L*算法。它是最经典的状态机学习算法,用来推断最小化的确定的有限状态机。被动式学习技术通过观测网络中的流量来推断协议的状态机,文献[8]通过被动学习的模型对网络进行了模糊测试。文献[9]通过状态机模型形式化分析了银行卡的安全性。文献[10]利用状态机学习技术对TLS协议实现库进行了主机名验证分析,文献[11]通过模型检测方法分析了TLS协议的状态机。
文献[12]介绍了基于特征集的状态机学习算法W算法,其通过状态机的特征集构造测试序列对目标系统进行测试。文献[13]对W方法进行了改进,提出了Wp方法,该方法通过状态机的部分特征集构造测试序列,通常此测试序列集小于W方法生成的测试序列集。但是此类方法并未考虑目标系统自身的特性。本文通过套接字约简,利用协议连接中交互消息的分类,对多余的测试序列进行了剔除;同时利用检查点算法,构造测试用例的前缀树,加速状态机学习过程。达到了降低测试序列数量,减少状态机学习时间,提高状态机学习效率的目的。最后,对两类TLS实现库进行了测试,并通过学习到的状态机发现了一个协议库的逻辑漏洞。
1 TLS协议
TLS的设计目标是在传输层上构建一个安全传输层,用来确保网络通信中的3种主要安全性质:可靠性,认证用户和服务器,确保数据发送到正确的客户机和服务器;机密性,加密数据以防止数据泄漏;完整性,维护数据的完整性,确保数据在传输过程中不被改变。
握手协议是TLS是最重要的部分,其主要作用是在客户端和服务器之间建立安全的数据传输信道。更改密码规范协议用于发送更改密码规范消息。警告协议的作用是,如果通信中发现连接或传输错误的一方,则通过警告协议向另一方发出警告;此外还可以在数据传输完成后,用于通知另一方断开连接。警告协议由警告消息实现。记录协议是TLS中用于数据传输的协议,其通信的报文及握手协议处理过的数据都由记录协议封装为记录报文并进行传输。
TLS执行步骤如图1所示。
图1 TLS执行过程Fig.1 TLS executing procedure
步骤1客户端向服务端发送服务器握手消息,这个消息里包括客户端生成的随机数、客户端支持的加密套件等信息。
步骤2服务器向客户端发送服务器消息,服务器在客户端支持的密钥组件中里选择一份加密套件,该套件决定了后续加密和生成摘要时采用的算法,另外还会生成一份随机数用于后续认证。同时将服务器的证书发送给客户端验证。
步骤3客户端验证服务器证书通过后取出证书中的公钥,将自身证书发送给服务器,通知服务器开始使用加密方式发送报文和计算消息认证码,并对之前握手的消息用主密钥加密后传输。
步骤4TLS服务器验证客户端证书后,发送更改密码规范消息,确认使用的密码套件。
步骤5通信双方以握手过程中协商好的安全参数,进行安全的应用数据传输。
TLS实现库是由开发者基于TLS协议规范开发的具体使用TLS协议进行操作的标准库或平台。当前应用广泛的TLS协议实现库有OpenSSl,GnuTLS,Botan等。
2 状态机学习算法
状态机学习算法试图学习目标系统的模型。通过选择输入查询目标系统,根据目标系统的响应,最终推断出目标系统的模型。如果模型是正确的,即其与目标系统输出一致,学习算法将认为生成的模型与目标系统的模型相同并停机。另一方面,如果模型不正确,目标系统和模型的输入产生不同的输出,根据这个不同的输出可以构造出反例。学习算法利用反例改进推断所得模型。重复这个流程直到学习算法产生正确的模型。由于协议实现库的输出不仅与其输入有关,同时也与其当前状态有关,因此选择米利状态机描述TLS实现库的状态机模型。
2.1 米利状态机
米利状态机是一类有限状态机,可以形式化地描述为一个六元组M=
λ(q,ε)=ε,λ(q,iσ)=λ(q,i)λ(δ(q,i),σ)
其输出依赖于状态机当前状态和输入。米利状态机的行为可以通过函数来定义,其中AM(σ)=λ(q0,σ)。当且仅当AM=AN时,状态机M和N称为等价的,记做M≈N。
2.2 状态机学习算法
状态机学习算法分为主动学习算法和被动学习算法,本文采用文献[14]中的主动学习算法,学习者(L*)算法。
L*算法用于学习目标系统的有限状态机(finite state machine,FSM),在学习算法中,包括了学习者、指导者、预言机3种角色和成员查询、等价查询两种查询。初始状态下,学习者的初始知识为米利状态机M的输入字母表I以及输出字母表O。指导者的知识为整个状态机,学习者通过两类查询来学习状态机模型。
成员查询:这类查询中,学习者查询一个字符串s以及其输出是否与目标系统一致,即σ∈I*,指导者通过AM(σ)中的输出序列响应。
等价查询:这类查询中,学习者查询一个假设的米利状态机H是否正确,即是否H≈M。如果正确,预言机回答为肯定:如果不正确,它会给出一个反例C,反例C是引起两个状态机不同输出序列的消息σ∈I*,其满足AH(σ)≠AM(σ)。
学习者向指导者提出查询获得状态机的信息,指导者回答学习者的成员查询,预言机响应等价确认查询判断该状态机能否正确代表协议规范中的状态机。通过这三者可以构建一个观测表
2.3 改进的测试序列生成算法
实际分析的目标系统称为被测系统(system under test,SUT)。在状态机推断中,并不知道协议实现库实际的状态机,此时需要构造测试序列作为等价查询对SUT进行测试以得到反例。
2.3.1 测试序列生成算法
利用Wp方法生成测试序列,该方法由两个阶段组成:
第一阶段计算假设模型H的迁移覆盖集P、状态覆盖集S、特征集W以及M的所有状态机识别集Wi。构造检查所有规范M定义的状态在实现库中是否可识别,对每个S中的状态Si,其识别集Wi是确定的,并且W是一组至少包含所有Wi输入序列的集合。设所有识别集Wi的集合为W,通过P,S以及Wi的选择,可以得到不同的测试序列。
第一阶段中的测试序列由S,W生成。每个规范的状态Si由W集检测。如果所有的测试都成功了,则M≈Q.WH,此时协议实现库中的状态数与规范M中的状态数相等。
H检测每个状态sj是否可以由最小识别集Wj识别。同时,对从初始状态到这些状态的迁移进行检查。
第二阶段对所有协议规范所确定的,但在第一阶段中未检测的迁移进行检测。
此时构造测试序列属于P而不属于S,记R=P-S,则此时有
式中,Wj是W中Sj的识别集。这个阶段对剩余的迁移关系进行检测。进行完两个阶段即可生成正确的SUT状态机。
2.3.2 套接字约简方法
通过Wp方法产生测试集的复杂度为O(n2|Σ|(m-n+1)),其中Σ是状态机的输入字母表；m是目标系统的状态数上界；n是状态机的状态数。因此,当Wp方法的状态数n较大时,会造成测试序列数量呈指数性增长,不利于大状态数系统的学习。需要对此算法中的查询数量进行简化。
可以利用协议交互中的消息迹的实际意义对测试序列生成进行约简,通过特定的套接字序列,简化测试序列的生成。
情况1连接中断
在寻找反例时,连接关闭后的追踪是没有意义的,但是在与SUT的交互中,一旦会话结束,SUT仍然会产生连接断开的响应,Wp方法会将此响应作为目标系统的输出构造等价查询寻找反例,而这些是无效的测试序列,需要终止后续测试序列生成。
情况2密钥重协商
在协议的会话中,可以通过发送密钥重协商消息进行密钥更改,这个过程可以看作是将协议状态重新迁移到了握手协议中的更改密码规范状态,二者在其后的测试序列生成一致,是多余的测试序列,因此可以停止生成重协商之后的测试序列的生成。
情况3异常消息警告
异常消息警告包括协议连接断开通知、关键警告以及警告。其中连接断开通知和关键警报会造成连接断开,与情况1中的连接中断类似,终止后续测试序列生成。
该改进算法利用了协议交互中的连接特性,利用特定套接字对测试序列生成进行了约简。
2.3.3 检查点算法
考虑到在构造测试序列时,SUT有时需要处理大量具有相同前缀的查询,从初始状态开始处理查询的话,在对查询的相同前缀进行处理时,SUT进行相同的状态迁移。如果每次都对SUT进行重置,需要大量的重复测试过程,因此需要对测试序列的处理进行优化,在处理SUT时,对其可能遇到的前缀时的状态及测试序列前缀进行记录,称这个记录点为检查点。可以通过构造前缀树用来存储之前执行过的查询,实现检查点算法。
树中每个节点记录一个之前的输入、相应的输出以及当时的状态的相关信息。在树的输出查询中,从根节点开始对每个查询中的输入步骤选择相应的子节点。在这个过程中能够找到对每个输入步骤的相应的输出。一个查询由已知输出的前缀,以及其后缀还未执行过未知其输出的后缀组成。其形式化描述如表1所示。
表1 检查点算法Table 1 Checkpoint algorithm
3 实验及结果分析
本研究分析了两种TLS实现库OpenSSl及网络安全服务(network security service,NSS)的米利状态机模型。
3.1 测试过程设置
为了推断TLS协议实现的米利状态机,本文使用了开源的状态机学习框架LearnLib[15],其使用了L*算法进行学习。SUT对于测试者是黑盒,由于无法得知协议库的实际执行状态。因此必须向LearnLib提供可以发送到SUT的消息列表以及将SUT重置为其初始状态的命令。
通过发送消息和重置命令的序列,利用测试工具将抽象消息从输入字母表转换为可以发送到被测系统的具体消息,LearnLib尝试根据从SUT收到的响应为状态机提出假设。然后检查这些假设是否与实际状态机等效。如果模型不相等,则返回一个反例,LearnLib将使用它来重新修改其假设模型。
3.1.1 检查深度
对于LearnLib,在测试中首先需要指定等价检查的深度:给定状态机的假设H,需要将测试上限设置为找到的状态数加上指定的深度。该算法仅查找其长度最多为设定上限的反例跟踪,如果无法找到,则假定状态机的当前假设与实现的假设等效。如果实际状态机的状态数多于找到的状态数加上指定的深度,则认为此假设是正确的。本文通过实际测试经验,取测试深度为5进行测试。
3.1.2 输入输出字母表
为了使用LearnLib,还需要设定一个可利用的输入字母表,其可以将实际发送和收到的消息抽象为一个字符串作为LearnLib的输入,设定输入输出字母表为:客户端握手、客户端证书、完成、客户端密钥交换、客户端证书验证、更改密码规范、应用数据。由于有警告协议中的消息格式只在响应中,因此在输出表中加入空报文,解密失败以及连接中断。
3.2 测试结果
表2为使用指定检查深度为5的改进Wp方法对输入的常规字母表的协议服务器端进行自动测试的结果。
表2 改进算法在测试深度为5条件下应用输入字母表对服务器端实现的自动测试结果Table 2 Results of the automated analysis of server implementations for the alphabet of inputs using our modified method with depth=5
通过套接字约简方法,生成的等价查询数显著下降,这意味着改进的测试序列生成方法能够有效约简学习状态机过程中所需的测试序列数量。从学习状态机模型所用时间上看,生成模型所用时间显著下降,这意味着该方法通过TLS的特定套接字,极大地减少了测试过程中的冗余信息。
实验结果表明,虽然只应用检查点算法的改进算法无法减少所需的成员查询和等价查询数量,但是可以明显减少状态机学习所用时间。这说明通过检查点算法,能够显著降低SUT在测试过程中对测试序列的响应时间,加速反例生成,提升状态机学习效率。但其效果不如套接字约简明显。
二者结合的改进算法所需时间最少,效率最高,这是由于两种方法从不同的角度对算法效率有提高。
3.3 状态机模型分析
在分析得到的模型时,首先人工查看是否有比预期更多的路径导致应用程序数据的成功交换。其次确定模型是否包含多于必要的状态,并识别意外或多余的过渡状态。还需要检查可以指示异常状态的消息。如果遇到任何异常,那么就要更深入的分析以确定原因及影响。一个明显的观察是服务器端实现库的状态机模型都有所不同,这意味着TLS实现库在实现过程由于开发者对协议规范的理解不同。那么在实际应用中,就存在着潜在的安全威胁。
特别是,协议状态机学习涉及一种被动测试:在状态机学习期间执行的测试包括错误测试,即消息以意外命令发送的测试,人们期望这会导致连接中断,而如果连接并没有按照规范设定的中断的话,则需要深入调查其原因。图2是OpenSSL 1.0.1g服务器端学习到的状态机模型。对此状态机进行分析,可以看到一条可疑路径(状态0,1,6,9,12)。
如图2虚线所示的路径中,当服务器收到更改密码规范消息时,就会开始计算会话密钥,然而此时还没有发送客户端密钥交换消息,因此实际上服务器端用的是一个空的主密钥,这意味着在通信过程中,实际使用的密钥是通过传递的消息计算所得的。攻击者就能轻易计算出接下来的会话所用的密钥。
这意味着攻击者能够在握手初期通过向客户端和服务器发送更改密码规范消息来劫持一段会话。
通过上述分析可以看到,通过状态机学习得到的状态机模型,可以寻找在协议实现库的逻辑缺陷,完成对协议实现库的安全性分析的目的,这证明了通过改进算法提取的协议状态机是有效的。
图2 通过改进算法学习到的OpenSSL 1.0.1 g状态机Fig.2 Learned state machine model for OpenSSL 1.0.1 g
4 结 论
本文提出了一种改进的测试序列构造方法,其利用套接字约简,能够有效减少在对目标系统黑盒测试中所用到的测试序列数量,减少运算量;同时利用检查点算法,降低分析的运行时间,从而提高状态机学习效率,在未知目标系统规范的黑盒测试中具有很好的效果,从而使得分析复杂状态机运行成为可能。实验结果表明,完整改进算法效率最高,既结合了套接字约简的等价查询数减少,又通过检查点算法提高了测试效率。整体上看,套接字约简对学习效率的提升效果好于检查点算法。
本文结合状态机学习的L*算法以及等价查询算法Wp方法,成功地提取了OpenSSH,NSS两类TLS协议实现库的状态机模型。并以此为基础对TLS协议实现库进行深入的分析。通过状态机学习技术来测试协议实现库,能够有效发现其中存在的逻辑缺陷。
