AI 摘要 · 由英文经 AI 翻译
SeriCrypt: An LLM-Driven Context-Aware Serialization Framework for Cryptographic Protocols
Maosong Chen, Xi Chen, Mengcheng Ju, Dongliang Zhao, Chunxiang Gu
TL;DR
构造密码协议消息既要求跨消息状态一致,也要求密码学计算正确,但现有自动化工作主要聚焦于明文协议。SeriCrypt 使用 LLM 将协议知识提取为 CDSL/PAST,并通过与协议无关的执行引擎计算字段属性并序列化消息。该框架生成了被接受的消息序列,完成了所有受测握手,发现五项安全约束违规,并在相同时间预算内实现了更高的模糊测试覆盖率。
问题
自动构造密码协议消息颇具挑战,因为字段取值依赖先前的会话状态和密码学计算,而现有自动化方法主要针对明文协议。
出处:§II · p. 2方法
SeriCrypt 将基于 LLM 的信息提取与受 CDSL 约束的 Protocol Abstract Syntax Tree 相结合,并使用与协议无关的执行引擎计算字段、执行密码学操作并完成序列化。
出处:§I · pp. 1–2结果
SeriCrypt 在全部 10 种测试配置中完成了握手,发现五项安全约束违规,并在相同时间预算下实现了六种协议中最高的代码覆盖率。
出处:B. RQ1: Interoperability · p. 7, F. RQ5: Protocol Testing Application · p. 9, G. RQ6: Fuzzing Application · p. 9要点与局限
该框架支持互操作性测试、针对性的安全约束测试,以及结构化的密码协议模糊测试。
出处:B. RQ1: Interoperability · p. 7, F. RQ5: Protocol Testing Application · p. 9, G. RQ6: Fuzzing Application · p. 9
Abstract
from arXiv · showhide
Constructing syntactically correct and cryptographically valid message sequences is essential for protocol state machine learning, conformance testing, and fuzzing. Unlike plaintext protocols, cryptographic protocols involve complex cross-message state dependencies and cryptographic computation constraints. Existing automated approaches predominantly target text-based or plaintext protocols, leaving cryptographic message construction largely manual. We present SeriCrypt, an LLM-driven, context-aware serialization framework for cryptographic protocols. It employs a large language model to extract field constraints, state dependencies, and cryptographic computation rules from unstructured protocol specifications into a unified structured intermediate representation, formally characterized by a domain-specific language for cryptographic protocols (CDSL). A protocol-agnostic execution engine parses CDSL declarations, automating field value resolution, cryptographic primitive invocation, and byte-stream serialization. As case studies in protocol security testing, we use the framework to construct violation messages targeting specification-defined security constraints and to support protocol fuzzing, evaluating it on mainstream implementations of TLS 1.2/1.3, IKEv1/v2, SSH, and TLCP. SeriCrypt generated message sequences accepted by all evaluated implementations and completed handshakes in every scenario. Security constraint testing revealed five specification violations, and fuzzing reached deeper protocol states with higher code coverage than mainstream fuzzers under the same time budget, demonstrating the framework's practical value for cryptographic protocol security testing.
I. 引言
SeriCrypt 将基于 LLM 的规范提取与结构化表示、协议无关的执行引擎相结合,解决构造密码学有效协议消息的难题。它支持在多种密码协议中自动序列化并开展安全测试。
研究动机
- 即使规范经过充分验证,实现在规范上的偏离仍可能造成严重漏洞,因此实现安全测试至关重要。文中举例说明了状态机绕过。出处:§I · p. 1
- 构造密码学消息时,必须满足字节级编码要求、跨消息状态依赖关系以及密码学计算约束。这些依赖包括先前生成的随机值、协商参数、临时密钥、密钥派生、认证码和签名。出处:§I · p. 1, §II · p. 2
方法
- SeriCrypt 使用基于 LLM 的提取流程,将非结构化规范转换为受 CDSL 约束的协议抽象语法树。该方法减少了人工整理协议消息及密码学依赖规则的工作。出处:§I · pp. 1–2
- CDSL 以统一方式描述消息结构、字段属性、跨消息引用和密码学规则;执行引擎则计算属性并序列化消息。该引擎调用密码学原语,并将协议特定描述与可复用的执行机制分离。出处:§I · p. 2
设计要求
- 该设计将自动化分解为表示与执行问题,并要求具备结构化、依赖关系处理、密码学计算、可执行性、协议无关性及属性感知等能力。这些要求为形式语言和通用执行引擎的设计提供指导。出处:§II · p. 2
III. 形式化模型与统一属性系统
CA-AGCP 在属性文法基础上扩展了会话知识、运行时上下文和密码学原语,为表示和求值密码协议消息提供形式化基础。
A. 从 CFG+AG 到 CA-AGCP
- CA-AGCP 将经典上下文无关文法和属性文法扩展用于密码协议建模,以表示结构依赖和语义依赖。经典文法描述层次结构,属性文法则通过综合属性和继承属性增加节点求值能力。出处:A. From CFG+AG to CA-AGCP · p. 3, B. Formal Definition of CA-AGCP · p. 3
B. CA-AGCP 的形式化定义
- CA-AGCP 形式化模型是一个 9 元组,分为句法骨架、基本属性系统和动态语义扩展。第一层定义协议拓扑,第二层支持节点级求值,第三层刻画密码协议特有的动态行为。出处:B. Formal Definition of CA-AGCP · p. 3
- 知识空间 K 存储规范常量、本地安全策略和当前测试配置值。例如算法标识符、版本号、固定标签、字节序列和证书。出处:B. Formal Definition of CA-AGCP · p. 3
- 运行时上下文 Γ 存储通过结构化路径或简单标识符寻址的会话值,并支持状态读写。它定位已交换消息中的字段,并为密钥派生的中间结果命名。出处:B. Formal Definition of CA-AGCP · p. 3
- 密码学原语空间 Ω 包含原子库操作,以及由有序规则链构成的复合操作。复合操作表示密钥派生以及加密或解密封装等过程。出处:B. Formal Definition of CA-AGCP · p. 3
- PAST 是根据 CA-AGCP 文法生成、用于表示协议消息的协议抽象语法树。模型将其定义为一个形式化对象。出处:B. Formal Definition of CA-AGCP · p. 3
- 消息结构树和会话计算块通过动态上下文 Γ 关联。计算块包含有序原语链、辅助函数和中间变量,用于生成密钥或复合密码学操作。出处:B. Formal Definition of CA-AGCP · p. 3
C. 统一属性系统(UAS)
统一属性系统将协议字段语义划分为内在、关系和转换属性,从而支持独立取值、基于上下文的引用及密码学计算。
C. 统一属性系统(UAS)
- UAS 根据语义功能和计算方式将属性分为三类。这三类分别对应与上下文无关的数据、历史字段依赖关系和密码学转换。出处:C. Unified Attribute System (UAS) · p. 3
内在属性
- 内在属性描述与上下文无关的原子数据,其取值取决于符号语义或局部编码规则。其求值不依赖运行时上下文 Γ 或密码学操作空间 Ω。出处:C. Unified Attribute System (UAS) · p. 3
关系属性
- 关系属性表示通过协议历史交互形成的字段间依赖关系。其取值通过声明的引用路径,从运行时上下文 Γ 投影获得。出处:C. Unified Attribute System (UAS) · p. 3
转换属性
- 转换属性编码由密码学原语驱动的高阶语义,包括密文生成、哈希验证和密钥派生。根据属性声明,其操作会消耗从 Γ 和知识空间 K 中提取的输入。出处:C. Unified Attribute System (UAS) · p. 4
IV. CDSL:密码协议领域专用语言
CDSL 将 CA-AGCP 实现为一种无歧义、可由机器解析的语言,用于共同描述协议消息结构与密码属性语义。
语言设计
- CDSL 通过三个协同子系统承载 CA-AGCP 的结构与语义两个维度。所给内容将这些子系统介绍为该语言的组织设计。出处:§IV · p. 4
消息结构语法
- CDSL 的结构语法通过 BNF 定义的具名产生式规则,表示 CA-AGCP 的句法骨架。这为协议消息描述提供了形式语法。出处:A. Message Structure Grammar · p. 4
- 原子节点表示具有长度约束和属性注释的不可分割数据单元。引用序列通过规则名称指向产生式,从而拼接子结构。出处:A. Message Structure Grammar · p. 4
- 备选项通过递归产生式和局部控制的终止方式,表示可变长度的同质序列。这种构造对应于递归展开,并以空产生式结束。出处:A. Message Structure Grammar · p. 4
B. 统一属性求值系统
CDSL 将协议字段语义组织为固有、关系和变换属性,每类属性针对取值、依赖关系、长度和密码计算均具有确定的求值行为。
- CDSL 将三类理论属性具体化为六种具有确定求值语义的类型。出处:B. Unified Attribute Evaluation System · p. 4
固有属性
- 固有属性将字段绑定到指定值、密码学安全随机数,或证书和时间戳等本地导入的数据。出处:B. Unified Attribute Evaluation System · p. 4
关系属性
- 关系属性引用先前字段或会话状态;长度属性则根据序列化子树的大小回填。出处:B. Unified Attribute Evaluation System · p. 4
变换属性
- 变换属性封装密码计算,并支持辅助函数、原语算法、复合计算块函数以及带追踪的参数引用。出处:B. Unified Attribute Evaluation System · p. 4
C. 会话级密码计算语法
CDSL 将会话级密码计算表示为有序或参数化的代码块,执行引擎会结合消息属性对其求值。TLS 1.3 Finished 示例展示了这些代码块如何解析依赖关系、派生密钥、计算验证数据并序列化结果。
- TLS 1.3 密钥调度和 IKEv2 prf+ 等会话级派生过程,需要超越单字段表达式的多步计算块。出处:C. Session-Level Cryptographic… · pp. 4–5
流类型计算块
- 流类型代码块将赋值规则组织成按依赖关系排序的链,并依次求值、更新上下文,使后续规则能够引用先前结果。出处:C. Session-Level Cryptographic… · p. 5
参数类型计算块
- 参数类型代码块通过键值对声明算法配置,包括签名算法等操作所需的维度。出处:C. Session-Level Cryptographic… · p. 5
TLS 1.3 Finished 示例
- 在 TLS 1.3 Finished 示例中,当验证数据依赖握手消息和客户端握手流量密钥时,执行引擎会触发密钥派生和 PRF 代码块。出处:D. Comprehensive Example: TLS 1.3… · p. 5
- 执行引擎使用 HKDF-Expand-Label 派生 finished 密钥,使用 HMAC 计算验证数据,随后进行加密封装、长度回填和字节级序列化。出处:D. Comprehensive Example: TLS 1.3… · p. 5
V. 系统设计与实现
SeriCrypt通过CDSL将基于LLM的PAST构建与属性驱动的执行分离,从而实现协议无关的消息生成和PAST层面的安全测试变异。
- SeriCrypt分为两个阶段:LLM驱动的PAST构建和属性驱动的PAST执行,并由CDSL连接二者。出处:A. System Overview · p. 5
PAST构建
- PAST构建采用思维链策略,将规范理解分解为三个阶段和八个连续步骤。出处:B. Phase1: LLM-Driven PAST Construction · p. 6
- 各阶段依次构建消息结构、使用CDSL属性和依赖关系标注字段,并提取密码计算块。出处:B. Phase1: LLM-Driven PAST Construction · p. 6
PAST执行
- 执行引擎实例化树结构,结合密码计算求值独立字段和依赖字段,并完成加密封装与序列化。出处:C. Phase2: Attribute-Driven PAST… · p. 6
协议无关性
- 协议无关性源于将复合算法编码为参数化计算块,因此新增协议时无需修改执行引擎代码。出处:C. Phase2: Attribute-Driven PAST… · p. 6
VI. 实验评估
本节评估 SeriCrypt 的互操作性、表达能力、LLM 生成 PAST 的准确性、直接 LLM 生成、协议测试及模糊测试,覆盖六种密码协议和六种主流实现。
RQ4–RQ6
- 评估分别考察直接使用 LLM 生成消息能否完成握手,以及 SeriCrypt 在协议测试和模糊测试中的表现。这些问题将直接生成客户端消息与 SeriCrypt 的结构化方法进行比较,并评估定向安全测试和模糊测试的应用效果。出处:§VI · p. 7
评估设置
- 在 TLS 1.2/1.3、IKEv1/v2、SSH 和 TLCP 的 10 种协议配置下测试了六种主流实现。配置包括 IKEv1 PSK/证书模式、IKEv2 PSK/证书模式、TLS、SSH 密码认证,以及 TLCP 双证书双向认证。出处:A. Experimental Setup · p. 7
RQ1:互操作性
- 10 种配置均完成了完整握手,生成的消息通过了 Wireshark 字段级解析和服务器验证。被接受的消息包含有效的协商参数、密钥材料、认证字段和加密负载。出处:B. RQ1: Interoperability · p. 7
RQ2:表达能力
- 在 10 种配置中共描述了 52 条客户端消息,每个字段都映射到 CDSL 的六种属性类型之一。这些消息涵盖六种协议,没有字段模式超出 CDSL 属性系统的覆盖范围。出处:C. RQ2: Expressiveness · p. 7
RQ3:LLM 生成质量
- PAST 生成的平均准确率超过 94%,但 TLS 1.3 结构生成和 SSH 计算块提取相对困难。报告的错误涉及条件字段的出现、跨消息状态与 transcript 边界,以及协议特定的计算细节;这些错误均可通过验证发现并修正。出处:D. RQ3: LLM Generation Accuracy for PAST · p. 7
E. RQ4:与直接 LLM 生成的比较
直接提示 LLM 生成完整的密码协议客户端,未能完成完整握手;SeriCrypt 将规范提取与确定性计算分开,从而应对了观察到的失败模式。
E. RQ4:与直接 LLM 生成的比较
- 30 次直接生成实验均未得到 L4 结果,即没有一次完成完整握手。基线使用 Gemini-3-Pro-Preview,对六种目标协议分别重复五次。出处:E. RQ4: Comparison with Direct LLM… · p. 8
- 直接使用 LLM 生成失败的原因包括协议常量与编码错误、难以稳定获取历史协商状态,以及密码计算链条出错。例如,字节序或长度编码错误、遗漏服务器选定的值或随机数,以及混淆 HKDF 标签、PRF 输入顺序和 AEAD 附加认证数据。出处:E. RQ4: Comparison with Direct LLM… · p. 8
- SeriCrypt 让 LLM 负责理解规范和提取知识,由执行引擎完成精确的密码计算与字节级编码。作者指出,这种分工发挥了 LLM 在信息提取方面的优势,并减轻了其密码计算的不稳定性。出处:E. RQ4: Comparison with Direct LLM… · p. 8
F. RQ5:协议测试应用
- 提取的 125 项安全约束生成了 364 个测试用例,并发现五项违规,其中包括四项新发现。在建立正常会话上下文后应用 PAST 变异,同时由执行引擎保证编码在语法上正确。出处:F. RQ5: Protocol Testing Application · pp. 8–9
G. RQ6:模糊测试应用
- 在相同的四小时预算内,SeriCrypt 在评估的六种协议上均取得最高代码覆盖率。基于 PAST 的结构化变异保持了密码有效性,使测试用例能够到达比盲目字节级变异更深的协议状态。出处:G. RQ6: Fuzzing Application · p. 9
VII. 讨论
SeriCrypt 的声明式 CDSL 和可复用执行引擎支持广泛的协议覆盖,并降低了变异工作量;但当前范围仍主要限于客户端消息序列化。
可扩展性
- CDSL 的六种属性类型和计算块能够表达 TLS、IKE、SSH 和 TLCP 协议之间的差异。扩展到新协议时可以复用执行引擎。出处:B. Extensibility · p. 9
- 扩展 SeriCrypt 需要进行配置、编写一个约 120 行的响应解析器,并手动验证或修正生成的 PAST。配置指定会话参数,并包含一个 5–8-field 输出示例。出处:B. Extensibility · p. 9
未来方向
- SeriCrypt 当前专注于序列化客户端消息;自动生成响应解析器和扩大协议验证范围则被列为未来工作。计划支持的目标包括 QUIC、WireGuard 和后量子混合握手。出处:C. Future Directions · p. 9
- 将 PAST 变异策略与结构感知模糊测试结合起来,并以迭代式 agents 取代手动 PAST 验证,是提出的未来方向。论文报告了支持模糊测试方向的初步结果。出处:C. Future Directions · p. 10
比较
- SeriCrypt 的能力边界包括自动化规范提取、跨消息依赖表达、密码学计算表达,以及协议无关的执行引擎。论文在 Table VIII 中将这些维度与代表性方法进行了比较。出处:§VIII · p. 10, Table VIII · p. 10
附录
附录记录了 TLS 1.3 消息与计算模板,以及具体的规范违规测试和观察到的实现行为。
TLS 1.3 构造
- TLS 1.3 Finished Client 由 record、encrypted-block、handshake、message-body 和 verify-data 字段组成,各字段长度均有规定。verify-data 字段依赖 transcript 哈希和派生的密码学值。出处:Example of Message Structure Grammar · p. 12, Figure 3 · p. 12, Figure 4 · p. 12
提示模板
- TLS 1.3 握手密钥派生和签名算法处理通过专门的计算模板与参数配置模板表示。Figures 7–14 展示了结构构造、属性标注和计算块提取。出处:Figure 5 · p. 12, Figure 6 · p. 12, Appendix B · p. 12
安全违规
- 总结了五项语义违规,包括未响应 IKEv2 INFORMATIONAL 请求,以及 TLS 1.3 证书、扩展和签名算法违规。附录指出,每项违规均包含 RFC 依据、测试构造和观察结果。出处:Appendix C · pp. 12–13
- TLSE 接受了由 MD5 签名的证书,却未发送所要求的 bad-certificate 告警。SeriCrypt 向 TLSE 提供了一个使用 MD5 签名的证书。出处:Appendix C · p. 13
- TLSE 收到缺少必需扩展的 ClientHello 消息,以及客户端未提供的服务器所选签名算法后,仍继续进行握手。报告的结果是,未出现缺少扩展或中止行为,且未声明的签名算法被接受。出处:Appendix C · p. 13
- TLSE 忽略了值为 0x02 的非法 ChangeCipherSpec 负载,而未以 unexpected-message 告警中止。合法负载值为 0x01。出处:Appendix C · pp. 13–14
变异任务
- 附录收录了九项变异任务的实现成本表,报告代码行数和修改函数数量。Table IX 比较了所评估工具的实现成本。出处:Table IX · p. 14
附录 D
附录 D 通过代码行数和修改函数数比较九项任务的变异实现成本,结果显示 SeriCrypt 能以显著更少的代码实现相同变异。
实验设置
- 评估采用相互认证的 TLS 1.2,并使用 OpenSSL 的 s_server 作为被测服务器。密码套件为 TLS DHE RSA WITH AES 128 GCM SHA256。出处:Appendix D · p. 14
任务集
- 九项任务涵盖结构字段、跨消息依赖和密码计算,三种工具面临的目标偏差完全相同。任务标记为 S1–S3、D1–D3 和 C1–C3。出处:Appendix D · p. 14
指标
- 变异成本以代码行数和编写或修改的函数数衡量,不计入基线客户端的构建。每个表格单元格报告 LoC / 函数数。出处:Appendix D · p. 14
Results
- 10 lines and 0 function changes let SeriCrypt complete all mutations, versus totals 4.1 and 8.8 times larger for TLS-Attacker and Scapy, respectively.Each SeriCrypt task edits 1–2 declaration lines; dependency-affecting tasks require 3 lines versus 32 and 31.出处:Appendix D · p. 14