该论文针对流控制传输协议（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 协议的多种潜在攻击面，验证了现有补丁的有效性，并提供了协议规范改进建议，对传输层安全研究有重要价值。

本文提出 SDP（Secure Datacenter Protocol），一种为新兴数据中心传输协议（如 NDP 和 Homa）设计传输层加密的协议。SDP 在不改变上层应用的前提下，将加密功能集成到传输层，支持 NIC（网络接口卡）卸载、原生协议号（与 TCP/UDP 并列）以及基于消息的抽象，从而实现低延迟的远程过程调用（RPC）和细粒度并行。实验表明，SDP 在保持高性能的同时提供机密性和完整性保护，适合需要低延迟和高吞吐的数据中心场景。