该论文针对流控制传输协议（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 还输出结构化攻击计划，记录利用流程、量化潜在资产损失，并可作为静态分析工具的语义误报过滤器。该工作为蓝队和审计人员提供了自动化验证漏洞可利用性的能力，有助于区分真实威胁与误报。