A Formal Analysis of SCTP: Attack Synthesis and Patch Verification

SCTP是一种传输协议，具有多宿主、多流和面向消息的传递等功能。使用PacketDrill工具对其两个主要实现进行了符合性测试。符合性测试并不是穷尽性的，最近的漏洞(CVE-2021-3772)表明SCTP并不免疫攻击。已经实施了解决漏洞的变更，但问题在于协议设计中是否可能仍存在其他漏洞。 我们采用基于形式化方法的严格方法研究SCTP设计的安全性。我们创建了一个SCTP的正式Promela模型，并根据其RFC规范和与主要RFC作者的磋商定义了10个捕捉基本协议功能的属性。然后我们使用Spin模型检查器展示了我们的模型满足这些属性。我们定义了4个攻击者模型——Off-Path，攻击者是一个可以欺骗对等方端口和IP的外部人员；Evil-Server，攻击者是恶意对等方；Replay，攻击者可以捕获和重放但不能修改数据包；On-Path，攻击者控制对等方之间的通道。我们修改了一个专为传输协议设计的攻击合成工具Korg，以支持我们的SCTP模型和四个攻击者模型。 我们使用攻击者模型合成了14种独特的攻击，包括Off-Path攻击模型中的CVE漏洞、Evil-Server攻击模型中的4种攻击、Replay攻击模型中的机会主义ABORT攻击以及On-Path攻击模型中的8种连接操纵攻击。我们展示了所提出的补丁消除了漏洞，并且根据我们的模型和协议属性没有引入新的漏洞。最后，我们确定并分析了RFC中的歧义，我们展示了它可以被不安全地解释。我们提出了勘误，并展示了它消除了歧义。

该论文旨在研究SCTP协议的安全性，特别是在面对四种不同类型的攻击模型时是否存在漏洞。

论文采用形式化方法，使用Promela模型和Spin模型检查器对SCTP协议进行建模和验证，并定义了10个关键属性以捕捉协议的基本功能。同时，修改了一个攻击合成工具Korg来支持SCTP模型和四种攻击模型，并合成了14个攻击，包括CVE漏洞、恶意服务器攻击、重放攻击和路径上攻击等。最后，论文还发现了SCTP协议标准中的歧义，提出了一个修正方案。

论文使用了形式化方法进行建模和验证，提出了四种攻击模型，并合成了14个攻击。研究发现SCTP协议标准中存在歧义，并提出了修正方案。实验结果表明，论文提出的修正方案可以消除漏洞而不引入新漏洞。

最近的相关研究包括对SCTP协议的漏洞分析和安全性研究，如《SCTP协议的安全性研究：漏洞分析与防范》、《基于时间自动机的SCTP协议建模与验证》等。