随着信息技术的蓬勃发展,社会已经进入了万物互联的时代。以密码学为基础的安全协议作为保护网络通信的基石,承担着数据加密、身份认证和隐私保护等重要任务,其自身的安全性对维护网络空间安全至关重要。然而受协议设计逻辑复杂、开发人员理解偏差等诸多因素影响,实际的安全协议实现可能存在缺陷,因此有必要进行全面的漏洞检测,以确保其可靠性和安全性。
安全协议实现中的漏洞大致可以分为内存相关的漏洞和逻辑类漏洞两类。内存相关的漏洞通常会导致程序崩溃或内存损坏等显式行为,而逻辑类漏洞则是指迫使协议偏离基本安全性(机密性、完整性、可用性等)和隐私保证的问题
[1],如OpenSSL CCS漏洞、重协商漏洞等。逻辑类漏洞通常不会产生外部可识别的影响,使得从安全协议实现中查找此类错误更加困难。模糊测试是应用最为广泛的漏洞检测技术之一,但现有研究主要关注缓冲区溢出等内存相关的漏洞,基于模糊测试查找协议逻辑漏洞的研究较少,且在黑盒场景下应用受限。模型学习方法可在黑盒条件下检测协议实现中的逻辑问题,其能够基于协议交互数据推断出反应协议实现行为逻辑的状态机模型,但学习代价随消息类型增多而显著提高。
基于以上研究背景,提出一种可检测安全协议实现中逻辑错误的黑盒协议模糊测试方法,并通过实验证明了方法的有效性和优势。
1 相关工作
1.1 模型学习
模型学习方法基于协议交互数据推断协议状态机模型,随后通过分析模型来查找协议实现中的逻辑问题,被广泛应用于各种协议实现分析。文献[
2]用该方法推断多个TLS协议实现的状态机,通过分析模型发现3个新漏洞。考虑到协议的状态机通常比较复杂,手动分析工作量大且容易出错,文献[
3]引入模型检测技术对状态机模型进行自动化验证,使用模型检测工具NuSmv验证模型是否满足预定义的属性,随后将该方法应用于SSH协议、IPsec协议等。文献[
4]通过模型等价性检查来查找LTE实现中的异常行为或互操作性问题。文献[
5]使用形式化分析工具ProVerif对3种MP协议模型进行分析,发现252项属性违规。文献[
6]提出一种自动检测状态机错误的方法,其以一组状态机错误作为输入,并将其编码为自动机的形式,自动检测系统模型是否存在相同问题。尽管模型学习技术在安全协议实现分析领域取得了显著成果,该方法也存在一些局限性:学习代价较高,导致对于复杂的安全协议实现,推导出的状态机通常只是完整模型的一部分;状态机的抽象级别过高,无法对消息执行细粒度的变异,然而现实中很多漏洞都依赖于此。
1.2 有状态模糊测试
模糊测试通过发送大量随机的输入,检测程序中存在的漏洞。安全协议是有状态系统,通常具有复杂的状态空间,传统的模糊测试技术由于难以触及深层次的协议状态,导致效果不佳
[7]。
文献[
8]提出了专用于协议的有状态灰盒模糊测试工具AFLNet,其通过网络接口将变异的消息序列发送至服务器,并收集状态反馈来指导模糊测试过程。随后相关研究者尝试从状态表示
[9]、状态选择算法
[10]和提高测试速率
[11]等角度对AFLNet进行改进。这些方法以代码覆盖作为一个重要的反馈度量,不适用于黑盒场景。文献[
12]提出一种面向消息序列的黑盒协议模糊测试方法,基于系统响应序列收集反馈信息,然而其以中间人方式工作,无法有效处理加密消息。
上述工作主要关注被测系统中代码实现层面的错误,如崩溃和内存损坏等,不具备检测逻辑类错误的能力。为此文献[
13]构建了模糊测试框架LTL-Fuzzer来查找与线性时序逻辑(Linear-time Temporal Logic, LTL)属性有关的违规行为,它首先将LTL属性中的原子命题映射到具体的代码位置,然后通过定向模糊测试技术引导测试进程按特定顺序访问多个目标点。文献[
14]使用项重写的概念描述协议消息,将DY攻击者的抽象DY执行集视为可能的测试用例,并使用基于项的变异方式来探索该集合,最后通过声明判断异常情况,从而排查针对协议实现的潜在逻辑攻击。尽管这些工作取得了不错的效果,但是DYFuzz需要提供从被测程序内部获取关键信息的接口,而LTLFuzzer则需要将LTL属性中的原子命题映射到具体的代码位置,两者都不适用于黑盒测试场景。
现有的黑盒协议逻辑漏洞检测技术多局限于一些特定的应用场景,无法迁移使用,此外也存在检测面单一、效率和扩展性上的不足
[15]。
2 预备知识
2.1 确定有限自动机
确定有限自动机(Deterministic Finite Automaton, DFA)是一种抽象的计算模型,用于描述在给定输入下,能够依据一组规则从一个状态转移到另一个状态的系统。
一个DFA由一个五元组构成。其中:是输入字母表,即有限的输入符号集合;是有限状态集合;是初始状态;是接受状态集合。如果自动机在处理输入序列后最终处于一个接受状态,称输入序列符合自动机所描述的语言规则,否则输入序列不符合规则。是状态转移函数,将当前状态和输入符号映射到下一个状态,用表示在状态下输入转移到的状态,且,。
DFA在任何给定时间点只能处于一个状态,并且对于给定的输入符号,只有一种可能的状态转移。这使得DFA具有确定性,即对于任何输入都可以唯一地确定下一状态。通过以下定义,可以将状态转移函数从符号扩展到符号序列:
其中:表示空序列;。称一个符号序列被DFA接受当且仅当。
2.2 IPsec协议
IPsec协议是工作在IP层的安全协议,由IKE、AH和ESP等3个子协议组成。IKE协议用以实现身份认证、密码算法选择和密钥协商,AH协议和ESP协议用于安全通信。
IKE通过在多方之间安全地维护安全关联(Security Association, SA)来管理IPsec安全通信。通信双方首先建立IKE SA,之后在IKE SA对应的加密通道中协商产生CHILD SA,并用于ESP或AH协议安全通信。
IKE协议有IKEv1和IKEv2两个版本,这里简单介绍IKEv2协议流程。相较于IKEv1复杂的模式组合,IKEv2仅定义了4种消息类型:IKE_SA_INIT、IKE_
AUTH、CREATE_CHILD_SA、INFORMATIONAL。
通信双方首先通过IKE_SA_INIT和IKE_AUTH进行密码参数协商和身份认证,此时双方分别拥有一个IKE SA和CHILD SA,从而可以利用CHILD SA下的参数进行IPsec数据安全通信。双方通信期间可以通过CREATE_CHILD_SA交互更新密钥,最后双方通过INFORMATIONAL交互删除CHILD SA和IKE SA以结束通信。
3 方法介绍
3.1 基本工作流程
图2描述了BDFuzz的整体框架,基于被测系统指具体的安全协议实现。
使用BDFuzz进行模糊测试需要预定义一组预期属性,用于描述安全协议实现应当符合的行为逻辑。通常可以从协议规范和已知安全漏洞中提取这种属性,或依赖专家经验进行定义。随后将每个属性的否定形式编码为一个DFA,如果协议实现存在使DFA转移到接受状态的行为,则认为协议实现违反了相应的规则。
BDFuzz基于网络通信的方式对协议实现进行模糊测试。状态检查器负责维护每个DFA的状态信息,模糊测试引擎根据状态检查器的引导和被测系统反馈来生成测试序列,测试序列由多个抽象输入符号序列组成。映射器模拟协议通信的一端,将抽象输入符号实例化为具体协议消息与被测系统进行交互,并将接受到的系统响应解析为抽象输出符号回传给模糊测试引擎。模糊测试引擎将每个抽象输入输出对反馈给状态检查器,状态检查器据此更新DFA状态。如果存在一个测试序列使得某个DFA到达了接受状态,则认为找到了一个违反该DFA所对应的规则的反例。
3.2 基于属性构建DFA
以IPsec协议规范中的描述为例。在IKEv2标准文档RFC7296中有如下规定:“The response to a request that deletes the IKE SA is an empty INFORMATIONAL response.”这句话描述了系统收到删除IKE SA这个特定的输入消息后应当以一个内容为空的通知消息作为输出响应,基于该规则可以构建如
图3所示的DFA。其中:INFORMATION_DELIKE表示删除IKE SA的通知;INFORMATION_NULL表示内容为空的通知;后缀“_i”和“_r”分别对应输入和输出,即发起方和响应方发送的消息;
表示当前状态的状态转移关系中未显示指示的任何其他转移条件;true则表示任意转移条件;双圆结点表示接受状态。
该DFA基本表达了上述规定的内容,但并不准确,因为该规定成立的前提条件是当前系统内部存在IKE SA。然而由于黑盒条件的限制,无法确定系统内部是否存在IKE SA,也无法获取内部关键信息来构造正确的删除消息。可以考虑通过IKE_SA_INIT和IKE_AUTH交互主动与被测系统建立IKE SA连接。此外,通过INFORMATION_DELIKE和INFORMATION_NULL正常交互完成IKE SA删除后,再次接收到删除消息后系统无需进行响应。由此可以构造如
图4所示的DFA。
采用上述方式构造DFA的另一个优点在于,可以根据DFA当前的状态信息指导模糊测试抽象输入的生成。
3.3 DFA引导的模糊测试算法
为实现更高效的反例搜索,设计了基于DFA引导的模糊测试算法,根据DFA当前状态到接受状态的距离来指导测试用例的生成,算法1描述了该算法的基本流程。
算法1 DFA引导的模糊测试算法
输入:一组表达协议预期属性的DFA ,测试序列最大长度,抽象输入消息集合
输出:反例集合
1.for do
2.
3.repeat
4.
5.
6. while do
7.
8.
9.
10.
11. for do
12. if then
13.
14. if IsU then
15. break
16.until达到测试中止条件
用于保存与DFA 相关的反例,集合中的元素保存了当前的执行序列。具体来说,集合中的元素以二元组序列的形式保存:称s为一个执行序列,其中表示一个抽象输入符号;表示相应的抽象输出。是能够被映射器实例化的所有抽象输入符号的集合。在每轮fuzz循环中,BDFuzz首先基于状态检查器中维护的DFA信息选择一个目标DFA ,同时将其状态重置为初始状态(第4行)。
BDFuzz根据的当前状态从输入字母表中选择下一个抽象输入(第7行)。具体来说,BDFuzz首先计算的当前状态到其接受状态的所有路径,之后以路径长度为标准选择一条路径为目标路径。这里的路径指的是一个序列,其中表示一个抽象输入或者抽象输出符号,路径长度根据路径上的抽象输入符号的数量确定。为增强测试的随机性,算法以一定概率从字母表Σ中随机选择输入,虽然执行该输入不会直接使DFA的状态产生迁移,但是接受该输入后被测系统内部的真实状态可能会产生微妙的变化。
选定抽象输入后,映射器将其实例化为具体的协议消息,通过网络接口发送给被测系统并等待被测系统的响应,之后将具体的响应消息解析为抽象输出(第8行)。状态检查器更新所有DFA的状态(第9行),然后依次对DFA的状态进行检查:如果当前所处状态为接受状态,则认为找到了一个反例,将序列s添加到该DFA所对应的反例集合中(第12~13行)。如果从当前状态出发不存在能到达接受状态的路径,则没有继续执行后续输入的意义,直接跳出本次测试(第14~15行)继续生成新的测试序列进行测试。
3.4 映射器
3.4.1 映射器工作方式
映射器的功能是实现具体的协议消息和抽象的输入输出符号之间的转化。为扩大模糊测试的搜索空间,提高发现漏洞概率,映射器以一定概率对协议消息进行变异。通过变异产生异常的协议消息,被测系统在处理此类消息时可能产生更多的代码覆盖或触发某些边界条件,从而导致意料之外的行为。对于一个抽象输入符号,映射器根据当前会话上下文信息构造正常的明文消息,执行变异操作后,再对明文消息执行加密等密码学相关操作。接收到被测系统的响应消息后,映射器首先对消息进行解密,再对明文进行解析并转化为抽象输出字符。
需要注意的是,BDFuzz旨在查找违反特定属性的反例,抽象符号与具体消息之间映射的准确程度对于异常行为的判别有显著影响。当抽象符号与实际消息内容完全不匹配时,会得到大量的假阳性测试用例。因此与AFLNet等模糊测试工具执行随机变异不同,BDFuzz需执行更为精细的变异操作,使得变异后的消息依然能比较可靠地保持抽象输入符号的含义。
3.4.2 IPsec映射器实现细节
下面以当前已实现的IPsec协议映射器为例,介绍映射器的实现细节。
1)消息构造与解析。如前文所述,映射器首先根据抽象输入构造明文消息,然后执行变异和密码相关操作。IPSec协议映射器将抽象输入转化为明文消息的过程分为两步,首先将输入符号转化为更细粒度的抽象表示:以IKEv2协议为例,在预主密钥(Pre-Shared Key, PSK)认证模式下,IKE_SA_INIT消息的具体内容如
图1所示,除消息头HDR外,还携带了SA、KE和NONCE载荷,因此将其拆解为HDR-SA-KE-NONCE的格式。然后映射器逐项构造消息头和每个载荷,并将其按协议语法拼接起来,得到完整的IKEv2明文消息。IPSec协议映射器解析消息的步骤则正好相反,先将解密后的明文消息抽象为HDR-SA-KE-NONCE的形式,然后进一步抽象为更粗粒度的符号表示IKE_SA_INIT。应用该策略可使映射器处理更多类型的消息,并便于对协议消息执行基于协议语法的变异。
2)变异。IPSec映射器中的变异器支持对IKEv1协议和IKEv2协议消息进行变异,其基于RFC文档中描述的协议语法和语义定制变异操作。基于协议语法进行变异保证变异后的消息仍符合基本的消息格式,基于语义进行变异则进一步保证变异后的消息仍能保持抽象输入符号的含义。对于一个具体的明文消息,变异器会随机选择执行两个不同级别的变异:载荷级别,增删特定载荷或打乱载荷顺序;字段级别,随机选择消息头部或者某个载荷进行变异。更具体地说,变异器会选择消息头部或者载荷中的某个字段进行变异,并根据字段的类型执行不同的操作:数值字段,随机选择取值范围内的异常值替换原始值,或直接将其设置为极值;枚举类型字段,文档中通常规定了枚举字段的有效值及对应的含义,变异器随机选择有效值替换当前值,或以较低概率选择其他值;数据字段,随机对数据进行增加、删除和修改等操作。
4 实验评估
本文从以下3个方面对BDFuzz进行评估:1)BDFuzz是否能够在真实的安全协议实现中发现违反特定属性的异常行为;2)BDFuzz与现有的协议模糊测试工具相比效果如何;3)基于DFA的模糊测试引导算法是否能够提高发现错误的效率。
下面具体描述测试对象和实验设置,并对实验结果进行分析。
4.1 测试对象
选择IPsec安全协议实现作为测试对象,
表1列出了实验中测试的各种软件和硬件设备,及其版本和型号。其中strongSwan和Libreswan是两个应用广泛的IPSec协议开源软件实现;WinServer 2022是操作系统;Cisco和Palo Alto是常用的VPN设备,均实现了IPsec协议相关模块。
4.2 反例检查和漏洞检测
为评估BDFuzz在查找安全协议实现异常逻辑行为方面的效果,依据RFC标准文档为IKEv1协议和IKEv2协议定义了多个属性,并按第3.2节所述方式将其转换为确定有限自动机。本文实验所提取的所有属性及其对应的DFA均已上传至gitte(
https://gitee.com/zhaohuaixu/bdfuzz),在此不再罗列。对于每个测试对象和协议版本,均执行5轮24 h的测试。共发现了7个违反特定属性的反例,以及2个能够导致目标崩溃的漏洞,并申请3个CVE。
表2展示了测试中发现的违反特定属性的反例路径,下面对其做简要分析。
反例1:在反例1给出的路径中,Main_Mode_3_i的exchangetype字段由0x02(Identity Protection)变异为0x05(Aggressive Mode),strongSwan收到该消息后响应一个未加密的消息,导致应当受到加密保护的ID信息以明文形式传输。
反例2:strongSwan允许接受一个载荷顺序错误的Quick_Mode_1消息。
反例3:Libreswan删除CHILD SA后会对IKE SA进行检查,若当前IKE SA下没有维护任何CHILD SA,则主动删除该IKE SA。基于该异常逻辑可构造异常的删除CHILD SA的消息,从而导致Libreswan崩溃,目前该漏洞已被分配CVE编号CVE-2023-38712。
反例4:接收到异常的CREATE_CHILD_SA_i消息之后,strongSwan会发送Invalid_Syntax通知消息,并删除当前IKE SA,但并未通知对端该删除行为。进一步测试发现strongSwan在处理格式错误的SK载荷时会产生上述行为。这允许恶意第三方在不掌握密钥材料的情况下伪造一个带有错误SK载荷的IKEv2协议消息,导致strongSwan主动删除IKE SA。
反例5和反例6:Libreswan和strongSwan以及Cisco管理CHILD SA的逻辑各不相同,收到ESP协议消息后,并不严格按照建立CHILD SA时的串行外设接口(Security Parameter Indexes, SPI)进行匹配和响应,由此可能带来互操作性问题。
反例7:Cisco对于删除IKE SA消息的响应不是载荷为空的通知消息,而是携带了DELETE载荷。尽管该操作可能不存在安全隐患,但仍属于违背了RFC文档中的规定。
此外,BDFuzz还发现了两个导致目标协议实现崩溃的新的漏洞。CVE-2023-38710:在Libreswan IKEv2实现中,将REKEY_CHILD_SA中的RekeySA载荷的协议ID字段变异为2(AH)和3(ESP)之外的异常值,可导致Libreswan崩溃。CVE-2023-38711:在Libreswan IKEv1实现中,当Quick Mode ID类型被配置为ID_IPV4_ADDR或ID_IPV6_ADDR时,将Quick_Mode_1携带的IDcr载荷中的IDType字段值修改为0x02(ID FQDN),会造成Libreswan崩溃。实验结果表明,BDFuzz确实具备检测协议实现中逻辑错误的能力,同时也能够发现传统模糊测试所关注的内存类漏洞。
4.3 与其他协议测试方法对比
本节通过与其他安全协议测试方法进行对比,进一步评估BDFuzz的能力和效率。1)MLMC方法首先通过模型学习技术来推断被测系统的状态机,然后利用模型检测工具NuSmv来验证系统属性。在本节实验中使用与前一节相同的属性对状态机进行验证。通过与该方法进行对比可以验证BDFuzz在逻辑错误查找方面的效果。2)AFLNet是第一个有状态灰盒有状态协议模糊测试工具。实验对AFLNet进行了扩展,使其具备对IPsec协议进行测试的能力。通过与AFLNet进行对比来评估BDFuzz相对于现有灰盒模糊测试工具在漏洞检测和状态空间覆盖方面的效果。3)BDFuzz_r使用随机生成测试序列的方法来代替BDFuzz中基于DFA引导的模糊测试算法,通过与该工具进行对比来评估本文设计的模糊测试算法是否有意义。
本节实验选择strongSwan和Libreswan作为测试对象,以便可以使用灰盒模糊测试工具对其进行测试(AFLNet不具备处理加解密等操作的能力,修改源码将strongSwan和Libreswan的加解密及校验功能屏蔽)。以上一节中发现的反例和漏洞为评估指标,共执行5轮测试时长为24 h的测试。
表3总结了实验结果,√表示至少在某一轮测试中发现问题,×表示5轮测试中均未发现问题。
从实验结果来看,BDFuzz是唯一发现了所有问题的工具。AFLNet不具备检测异常逻辑行为的能力,只可能发现导致目标崩溃的问题。然而即使是这3个漏洞,AFLNet也只发现了其中一个,触发CVE-2023-38711和CVE-2023-38712的条件对于AFLNet来说比较苛刻。以前者为例,首先需要通过主模式交换建立IKE SA,其次需要选中Quick_Mode_1中的IDType字段,并将其值修改为某一个特定值才能触发该漏洞。MLMC方法构造的消息均为正常消息,无法发现那些只有错误消息才能触发的崩溃或者异常逻辑行为。此外,BDFuzz_r发现问题的效率也不如BDFuzz,因为BDFuzz_r只是盲目地生成测试序列,难以有效地探索协议的深层状态。以CVE-2023-38712为例,发现该漏洞首先需要通过完整的主模式和快速模式交互来建立IKE SA和CHILD SA,然后发送异常的删除CHILD SA消息,随机生成的测试序列难以按照特定顺序发送特定消息,而在DFA引导下可快速完成上述流程。
上述实验结果表明,相对于现有的安全协议测试方法,BDFuzz在查找逻辑问题和检测内存漏洞方面都有不俗的效果。另外通过与BDFuzz_r的对比,可以看到本文针对BDFuzz设计的基于DFA引导的模糊测试算法是有效的。
5 结束语
提出一种可用于检测安全协议实现中潜在逻辑错误的黑盒模糊测试方法。将异常的协议交互行为建模为确定有限自动机,并基于自动机驱动测试序列生成,使模糊测试进程更专注于对深层状态的探索,以提高发现错误的效率。基于该方法实现通用的黑盒模糊测试框架BDFuzz以及特定于IPsec协议的测试模块。在多款广泛应用的IPsec协议实现上进行实验,发现多个协议实现中的异常行为和能够导致目标程序崩溃的漏洞。后续研究工作可以从以下几个方面进行:1)自动化的DFA构建方式;2)更高效地模糊测试算法;3)在TLS协议、SSH协议等其他安全协议上的应用。