该论文提出了一种从协议规范文档（RFC）中自动提取有限状态机（FSM）的数据驱动方法，并将其应用于自动化攻击发现。网络协议的安全验证通常依赖攻击者合成或基于模型的模糊测试，但这些技术需要协议的正式表示，通常为FSM。然而，许多协议仅以英文散文形式描述，手工构建FSM耗时且易出错。为此，作者设计了一个混合流水线，包含三个关键步骤：第一，面向技术语言的大规模词表示学习（如word2vec）；第二，聚焦的零样本学习，将协议文本映射为独立于协议的信息语言（protocol-independent information language）；第三，基于规则将这种信息语言转换为特定协议的FSM。该方法在六个不同协议的RFC上验证了泛化性：BGPv4、DCCP、LTP、PPTP、SCTP和TCP。作者以TCP和DCCP为案例，演示了从RFC提取的FSM如何用于攻击合成。实验表明，仅依靠RFC这样的文本规范就能实现针对协议的自动化攻击者合成，有助于提高协议实现的安全性与鲁棒性。该工作主要面向网络安全研究员、协议开发者以及自动化安全分析工具的建设者，旨在减少协议形式化建模的人工负担，并提升攻击发现技术的可扩展性。

本文针对去中心化金融（DeFi）协议中深度逻辑漏洞的自动化攻击合成问题展开研究。随着区块链应用普及，DeFi 协议管理的数字资产价值巨大，成为攻击者的首要目标。现有智能合约漏洞检测工具在处理 DeFi 协议时面临严峻挑战：这类协议通常涉及多个智能合约之间的复杂金融交互，漏洞往往隐藏在跨合约的深层逻辑中，而非单个合约内部的简单缺陷。已有工具大多只分析单个合约，面对跨合约调用链时采用暴力搜索或穷举方式，导致分析效率低下且难以发现真正的逻辑漏洞。为此，论文提出名为 FORAY 的新方法，目标是高效合成针对 DeFi 协议深度逻辑漏洞的攻击路径。虽然摘要未详细展开 FORAY 的具体技术架构，但其核心思路应是结合程序分析、符号执行或约束求解等手段，对跨合约的金融交互逻辑进行建模，从而自动生成能够触发逻辑缺陷的交易序列或调用序列。论文强调当前工具的效率瓶颈和浅层分析局限，FORAY 试图填补这一空白。主要贡献包括：提出面向 DeFi 协议的逻辑漏洞攻击合成框架，改善跨合约分析的可扩展性，并为智能合约安全检测提供新思路。适合智能合约安全研究员、DeFi 协议开发者、区块链安全审计人员以及关注自动化漏洞挖掘的学术研究者阅读。

该论文针对流控制传输协议（SCTP）开展形式化安全分析。SCTP 是一种提供多宿、多流和消息导向传输的传输协议，其两个主要实现已通过 PacketDrill 工具的一致性测试，但一致性测试并非穷尽，近期漏洞 CVE-2021-3772 表明该协议仍存在安全隐患。尽管已有补丁，但协议设计中是否遗留其他缺陷仍是开放问题。作者采用基于形式化方法的严谨路线：首先创建了 SCTP 的 Promela 模型，并根据 RFC 规范及与 RFC 主要作者的咨询，定义了 10 条刻画协议核心功能属性；随后使用 Spin 模型检查器验证模型满足这些属性。接着定义了四种攻击者模型：Off-Path（外部攻击者，可伪造对端的端口和 IP）、Evil-Server（恶意对等方）、Replay（可捕获和重放但不修改报文）、On-Path（完全控制信道）。他们修改了面向传输协议的攻击合成工具 Korg，以支持 SCTP 模型及上述四种攻击者模型。通过攻击合成，共得到 14 个独特的攻击：Off-Path 模型中包含 CVE 漏洞本身，Evil-Server 模型中有 4 个攻击，Replay 模型中有机会性 ABORT 攻击，On-Path 模型中有 8 个连接操纵攻击。作者进一步证明，针对 CVE 提出的补丁在模型和协议属性下消除了该漏洞，且未引入新漏洞。最后，他们识别并分析了 RFC 中的一处歧义，该歧义可能被不安全地解释；他们提出了勘误并证明其消除了该歧义。这项研究系统化地揭示了 SCTP 协议的多种潜在攻击面，验证了现有补丁的有效性，并提供了协议规范改进建议，对传输层安全研究有重要价值。

本文提出了一种名为 KASS（知识增强攻击合成与仿真）的多智能体框架，旨在解决现有智能合约安全工具仅停留在漏洞检测、无法验证漏洞可利用性及攻击过程的问题。KASS 将自动利用生成分解为规划、生成和测试三个阶段，并融合三种互补机制：基于检索增强的现实审计知识规划、将攻击计划绑定到可执行概念验证测试的形式化生成与验证约束，以及修复代码级错误并在攻击假设失败时触发策略级重规划的分层双循环优化过程。评估在包含 104 个合约的 SmartBugs-Curated 数据集上进行，涵盖四种漏洞类型。结果显示，KASS 对 94.23% 的测试合约成功生成了可执行利用，该比率高于先前 REX 和 AdvSCanner 在类似子集上的报道结果，也高于同等评估协议下复现的 Claude Code 基线。在 11 个真实世界 CVE 标记合约上，KASS 成功验证了 9 例。除生成利用外，KASS 还输出结构化攻击计划，记录利用流程、量化潜在资产损失，并可作为静态分析工具的语义误报过滤器。该工作为蓝队和审计人员提供了自动化验证漏洞可利用性的能力，有助于区分真实威胁与误报。