Protocol state machine fuzzing of TLS Implementations
本文发表于Usenix Security 2018，作者：Shankara Pailoor，Andrew Aday，Suman Jana。三位作者均来自于Columbia University。
本文发表在USENIX Security 2015上，作者是来自伯明翰大学的Joeri de Ruite和来自拉德堡德大学的Erik Poll。他们最近几年的研究方向多为通信协议的安全分析，特别是利用自动机来分析协议。
1. 主要内容
现有的对于TLS协议的分析包含：对协议顶层设计的安全性分析，并非具体的协议实现，但是大多数的安全问题存在于协议的具体实现中；对TLS协议的具体实现（例如OpenSSL）的安全分析主要体现在对单个消息的fuzzing（例如证书的fuzzing）；另外还有对协议的配置信息进行分析的工具（例如sslmap）。作者认为自动机可以很好地表现TLS协议具体实现中的消息发送和接收流程，故利用自动机学习技术来构建9种不同的TLS协议实现的状态机。通过人工分析生成的状态机来寻找具体实现中的逻辑漏洞，进而分析其源码找到相应的bug。通过这种简单而快速的方法，作者找到了3中TLS不同的具体实现中的漏洞（GnuTLS，Java Secure Socket Extension和OpenSSL）。
2. TLS协议简要回顾
TLS是安全传输层协议。其握手的过程如下：首先客户端发送ClientHello消息（包含客户端随机数），接着服务器返回3条消息，分别是：ServerHello（包含了服务器随机数），Certificate（服务器证书，包含了服务器公钥），ServerHelloDone。然后客户端收到消息后，根据客户端随机数和服务器随机数生成预主密钥和主密钥，并且发送3条消息给服务器，分别是：ClientKeyExchange（包含了用服务器公钥加密的预主密钥），ChangeCipherSpec（表明客户端发送的下一个消息将加密），Finished（客户端发送的第一个加密的消息）。服务器收到3条消息后，双方共享同一个预主密钥，并且计算出主密钥。服务器返回2条消息，分别是：ChangeCipherSpec（表明服务器发送的下一个消息将加密），Finished（服务器发送的第一个加密消息）。至此，各方对接收到的Finished消息进行解密，如果匹配成功，那么握手成功，否则失败。接下来双方的通信都会采用主密钥生成出的密钥进行加密。握手过程如下图所示。
3. 自动机学习背景
为了理解论文中所提到的state-machine-learning，这里先介绍一下相关的背景知识[1]。有限确定状态机M（FSM）可以用一个六元组来表示M=(S, s_0,δ,λ,X, Y)，其中S表示所有状态的集合，S0是初始状态，X是输入字典，Y是输出字典：
- Delta（δ ）函数是状态转移函数，s_j=δ(s_j,x)表示从状态s_i出发，输入x而转移到状态s_j，x∈X
- Lambda（λ ）函数是输出函数，y=λ(s_i,x)表示从状态s_i出发，输入x而获得的响应y，y∈Y
- 一次完整的状态转移可以表示成一个三元组：(s_i,s_j,x/y)
如何区分不同的状态呢？假设有两个状态s_i和s_j，如果存在一个输入序列∃x∈X^* ，使得λ(s_i, x)≠λ(s_j,x)，那么这两个状态不相等。那么反过来两个状态相等的判定是所有输入序列，它们返回的输出序列是相等的（理想情况下可以穷举所有的输入序列）。
自动机学习的情景之一是对于黑盒系统，我们如何只通过输入并且观察返回的响应来构建目标黑盒系统的状态机？现有几种已有的算法可以构建黑盒系统的状态机，下面介绍Angluin’s L* 算法来构建咖啡机的自动机。
咖啡机的简要工作流程是：首先有一个干净的咖啡机，需要先加咖啡豆（pod）和加水（water），最后按下开始按钮（button），那么最后咖啡机就能生产出咖啡（coffee），如果在加好水和咖啡豆之前按下开始按钮，那么咖啡机会报警（error），正确的操作将返回正确信号（对勾）。下图是正确咖啡机状态转移图，输入字典是X={water, pod, button, clean}，输出字典是Y={正确信号（对勾），coffee（咖啡标志），error（星形）}。
现在的问题是假设状态机是未知的，我们如何用输入/输出来构建上图的正确的状态机？Angluin’s L* 算法采用观察表（Observation Table）来逐步地构建完整的状态机：
-
首先有一个初始状态s0（属于集合Sp），我们输入长度为1的输入序列，并且产生了4个输出响应。那么这4个输入/输出对（对应观察表中的每一行）能够唯一确定初始状态S0。相应地由s0产生4个不确定的状态s1，s2，s3，s4（对应表中的Lp）。我们再次从这4个不确定的状态出发输入长度为1的输入序列，得到它们的输入/输出对。发现有3个状态（s1，s2，s4）的输入/输出对和已有的初始状态s0相同，那么我们现在猜想这3个不确定的状态和s0相同而进行合并。而s3将作为新发现的状态添加到集合Sp中。在这一过程中，通过输入来获得输出的过程是membership queries。现在输入button而到达的状态是新状态，那么我们再次从这个新状态出发输入长度为1的输入序列，观察这个状态所到达的不确定状态是否与已知状态相同。发现由buttton出发的所有状态都和button状态相同，那么本次迭代结束。我们产生了一个闭合的观察表（闭合是指已知的Sp状态的每一行都是独特的，并且由已知状态产生的不确定状态Lp的每一行都能在Sp行中找到），那么Sp集合中表示已找到的不同的状态，我们生成了一个hypothesis，即假设的状态机。
图3 不确定状态s1，s2，s4可以与状态s0合并
图4 第一轮迭代利用观察表生成两个状态的hypothesis 既然我们找到了一个假设的状态机，那么我们需要验证这个状态机是否和实际的状态机相等。验证的过程称为等价查询（equivalence queries），这个过程需要找到一个输入序列c，使得λ_H (s_0,c)≠mq(c),c∈X^*，这个输入序列被称为反例（counterexample）。咖啡机的情况是，等价查询返回一个输入序列c={pod, water, button}，这个输入序列在上步获得的状态机中返回的是一个错误报警消息，但是实际查询却返回了咖啡成功消息。说明上一步中获得的hypothesis状态机与实际状态机不符。我们在找到反例后提取出其中的最小输入后缀water button，并且加入观察表的列中。
-
由反例更新观察表，再次迭代，迭代过程如步骤一。到这里，我们获得了第二张闭合的观察表，可以看到Lp中包含了由Sp引申出的不确定状态，它们的行都能在Sp中找到相同的行。经过相同行的合并，形成了Sp中6种独特的状态。在这次迭代中，我们更新了状态机hypothesis。
图5 第二轮迭代中的闭合观察表和生成的状态机hypothesis 由第二个hypothesis我们再次进行等价查询，并且获得反例（counterexample），提取反例中的最小输入后缀插入观察表中。在第三轮迭代后我们可以获得最终的状态机。如果等价查询找不到反例，即对所有的输入序列（实际上要设置一个最大查询上限），假设的状态机返回的输出与实际的查询相同，说明我们假设的状态机已经符合实际的状态机，迭代便终止。
4. 系统设计与实现
4.1 整体设计
论文工作采用LearnLib框架来进行TLS自动机学习。LearnLib框架集成了各种自动机学习算法，本文工作采用的是前面介绍的Angluin’s L* 算法。SUT（System Under Test）表示需要进行自动机构建的黑盒系统，论文分别对TLS通信的客户端和服务器进行状态机学习。输入字典根据学习的目标有所调整，如果目标是服务器，那么输入字典包含了TLS握手过程中客户端发送的消息类型，输出字典是服务器返回的消息类型。Test harness负责产生具体的消息，它能够将抽象的消息类型转化成具体的消息并且发送给SUT，同时也能够接收SUT返回的消息响应，并且转换成抽象的消息类型。LearnLib能够利用L*算法对SUT进行membership queries，并且生成观察表，进而获得假设的状态机hypothesis。为了验证hypothesis的正确性，需要进行等价查询（equivalence queries）。等价查询尝试找到一个反例，这个反例能够更新观察表，进行下一次的迭代学习过程。论文采用LearnLib内置的Chow’s W-method方法来进行等价查询寻找反例，为了加快等价查询的速度，论文对W-method进行了改进：传统的W-method在目标系统返回错误响应（例如connection closed）后还会尝试从终止状态寻找输入序列。论文改进的W-method在碰到错误响应后不再从对应状态寻找反例，这种改进加快等价查询的速度。整个学习过程图6所示：
4.2 Test harness实现
Test harness根据目标黑盒系统的不同而有所调整。如果测试服务器，那么test harness支持发送的消息类型包括：ClientHello (RSA and DHE), Certificate (RSA and empty), ClientKeyExchange, ClientCertificateVerify, ChangeCipherSpec, Finished, ApplicationData (regular and empty), HeartbeatRequest , HeartbeatResponse. 如果测试客户端，支持发送的消息类型包括：ServerHello (RSA and DHE), Certificate (RSA and empty), CertificateRequest, ServerKeyExchange, ServerHelloDone, ChangeCipherSpec, Finished, ApplicationData (regular and empty), HeartbeatRequest, HeartbeatResponse. 输出字典除了包含常规的消息类型外，还包括：空消息，即在规定的timeout内没有接收到响应；connection closed，即连接出错或者连接正常关闭；decryption failed，解密消息失败时产生。此外，test harness需要记录TLS握手过程中的信息，例如对方返回的随机数，证书公钥，预主密钥等。同时也需要根据状态对消息进行不同的处理，例如ChangeCipherSpec消息发送后或者接收后需要对下一个消息进行加密操作。
5. 实验结果与分析
论文对9种不同的TLS实现进行了自动机的构建，如图7所示，这些实现中最少的状态只有7个，最多的也只有12个。所以通过人工分析能够很快地找到一些错误的状态转移和冗余的状态。状态机构建的时间也由不同的TLS实现而变化，最快可以9分钟之内构建完成，最慢则需要9个小时。论文通过改进的W-method进行等价查询减少了查询的次数，加快了状态机学习的时间，如图8所示，对GnuTLS进行测试时，改进的W-method方法与原来的W-method方法有明显的加快，等价查询的次数大大减少。
5.1 分析方法
对于生成的状态机，论文首先检查到达握手成功的状态路径，分析这些路径是否合乎TLS规则。然后寻找状态机中的冗余状态或者非预期的状态，分析这些状态是否有问题。另外手动检查一些有趣的消息响应，例如有的状态转移返回”bad record mac”消息, 有的状态转移返回”decryption failed”消息等。下面列举出论文中找到的三种TLS具体实现中的漏洞。
GnuTLS
从状态机上可以观察到两条合法到达握手成功的路径（绿色），最终握手成功的状态是状态7. 同时发现了隐藏的路径（红色路径）到达状态8. 这条隐藏的路径是在握手的过程中发送heartbeat消息都会到达状态8，尽管test harness按照顺序发送了TLS协议中的消息，但是却不能到达成功的握手状态。经过分析GnuTLS的具体实现代码，论文发现GnuTLS会把握手过程中的消息都记录在一个buffer中，但是如果收到了heartbeat消息，GnuTLS会清空这个buffer，导致由buffer计算出的hash值与对方发送过来的加密消息中的hash值不再匹配，从而导致握手失败。
JSSE 1.8.0_25
从JSSE TLS实现的状态机中可以找到两条到达握手成功的路径，其中状态6是成功的握手状态。其中一条（绿色的路径）是合法的握手过程。另外一条是客户端跳过发送ChangeCipherSpec消息直接发送Finished消息也能够到达成功的握手状态。由于客户端发送ChangeCipherSpec消息表示客户端接下去发送消息都将用密钥加密，如果没有发送这个消息，那么将导致客户端发送的消息还是明文消息，而服务器发送的消息却是加密的。利用这个漏洞能够泄露客户端的明文消息，导致隐私泄露。这个漏洞报了CVE-2014-6593。
OpenSSL 1.01j
从OpenSSL 1.01j实现的状态机中可以找到一条到达握手成功状态7的路径。但是有一个可疑的状态8，这个状态是在握手成功后再次发送ChangeCipherSpec消息到达状态8后，所有后继的消息发送都会导致”bad record mac”错误消息响应。这通常表明错误的密钥被使用了，作者通过对其具体实现进一步分析发现OpenSSL将客户端的密钥换成了服务器的密钥，这表明双方加密的密钥是相同的（协议规定两个方向的加密密钥不同），如果双方的加密密钥相同，那么可能会被某些攻击利用（例如RC4漏洞）。
6. 评价
论文利用自动机学习的方法首次对TLS协议具体实现进行了状态机的建模。并且通过手动分析生成的状态机来寻找逻辑漏洞。自动机的学习利用了LearnLib框架，作者对其中的W-method等价查询算法进行了改进，使得等价查询次数有效减少，加快了状态机构建的速度。通过这种简单快速的方法可以很快地构建出TLS协议具体实现的状态机，状态机也足够直观，我们可以人工检查这些状态机来找到错误的状态转移或者冗余的状态，并且对照具体的实现源码，可以定位到实现中的bug。但是状态机分析不能够体现出协议实现的其他漏洞，例如后门（例如发送100次消息能够实现握手），消息解析过程中的漏洞（例如溢出漏洞）。
7.参考
文 | BlackMax, DR.XX, Harry
转载于:https://www.jianshu.com/p/9a9e12a588ed