Page 310 - 《软件学报》2025年第8期
P. 310
袁斌 等: 基于有限状态机引导的网络协议模糊测试方法 3733
数字证书的 Certificate 消息, 其中也包括了服务端的公开密钥. 紧接着进行 KeyExchange 密钥交换阶段, 客户端用
服务器公钥对一个预共享主密钥进行加密发送, 服务端用私钥进行解密, 使双方共享相同的主密钥. 在随后的通信
中, 客户端和服务端基于之前协商的参数计算出一个共同的主密钥, 用以加密通信, 并通过 ChangeCipherSpec 消
息相互通告将启用新的加密参数. 完成这些后, 双方互发 Finished 消息, 含有握手阶段所有消息的哈希值用以确认
握手是否成功完成. 在握手成功后, 客户端和服务端将利用之前约定的密钥与密码套件来加密和解密数据, 进而开
始安全传输应用层的数据 ApplicationData. 为了确保不同密码套件带来的代码路径覆盖差异, 构建有限状态机模
型时应涵盖所有 3 种主要握手情景: RSA 加密、DH 加密以及 ECDHE 加密. 这将导致在 ClientKeyExchange 消息
中会出现 3 种不同的情况, 具体取决于所采用的密钥交换算法, 从而影响该消息的内容和格式.
然而上述只展示了一种理想情况下的握手, 在很多场景下可能会出现错误情况, 这个时候传输的任意一方都
可能发送错误信息并终止消息传输. 通信中的错误分很多种, 比如服务端接收到了非法的字符 (illegal_parameter)、
服务端的记录层溢出 (record_overflow)、服务端接收到了未预料到的消息 (unexpected_message)、客户端遇到错
误需要终止连接 (close_notify) 等. 同样, 论文会将这些错误消息考虑进去. 如果服务端并未回复消息, 会将这种情
况标记为 Empty. 最终得出的用于 TLS 协议有限状态机的字母表如表 1 所示.
表 1 TLS 协议的字母表
输入/输出 字母表
输入 ClientHello, Certificate, ClientKeyExchangeRSA, ClientKeyExchangeDH, ClientKeyExchangeECDH, ChangeCipherSpec,
(客户端) AlertWarningCloseNotify, Finished, ApplicationData
输出 ServerHello, Certificate, ServerKeyExchange, ServerHelloDone, ChangeCipherSpec, Finished, ALERT_FATAL_ILLEGAL_
PARAMETER, ALERT_FATAL_UNEXPECTED_MESSAGE, ALERT_FATAL_DECRYPT_ERROR, ALERT_FATAL_
(服务端)
DECODE_ERROR
依照 Mealy 机模型的原理, 有限状态机的每一次状态转移都是由输入和输出共同决定的, 这里的输入和输出
分别指客户端发送至服务端的数据包以及服务端反馈给客户端的数据包, 这些信息在状态转移图的边上会被标
出. 图 5 展示了一次可能会出现的状态转移, 由状态 1 转移到状态 3, 造成状态转移的原因是客户端发送了
ClientKeyExchange 信息而服务端没有回复数据包.
ClientKeyExchange
Empty
1 2
图 5 一次状态转移的示例
值得注意的是, 使用状态机来描述系统往往存在状态定义的粒度选择问题. 如果对状态粒度过细, 那么很有可
能由于状态空间过大, 导致在进行系统分析时候出现效率过低甚至是状态爆炸的问题; 而如果以较粗粒度来进行
状态的定义, 则可能由于模型未能描述系统的某些关键信息, 而导致系统出现漏报的情况. 为了解决这个问题, 本
文以 TLS 协议的 RFC 文档为参考标准, 从中提取了 TLS 握手过程的关键消息类型, 以构建输入输出字母表, 并以
此来构建 Melay 机. 如表 1 所示, 字母表中一共包含 9 个输入和 10 个输出, 由此, 既能有效避免状态爆炸的问题,
又保证了状态机能够有效捕获和描述 TLS 握手过程的关键信息.
3.3 有限状态机学习
SNETFuzzer 将基于 LearnLib 和 Angluin’s L*算法实现有限状态机学习程序. SNETFuzzer 当中的 Angluin’s L*
伪代码如算法 1 所示. 在算法 1 中, 对于集合 R 中的每个消息 r, 它被用于测试有限状态机中的每个状态. 也就是
说, 对于每对 w=(s, r), 其中 s 是有限状态机中的一个状态, r∈R, 如果从目标协议观察到的输出 o(s, r) 与目标有限
状态机的输出 o'(s, r) 不同, 就将 w 添加到 S 中. 在 Angluin’s L*算法的观察表中, 状态表示为输入字母表 S 中的前
缀字符串. 前缀字符串中的每个输入符号对应于一个实际的 TLS 请求消息. 因此, 如果要导出 o(s, r), 可以将消息 r
附加到前缀字符串, 按顺序发送到目标协议以获得其输出. 然后将此输出与有限状态机的目标有限状态机 o'(s, r)

