分布式协议的自动化攻击者合成

分布式协议应对良性故障（如丢包或延迟）和来自内部或外部对手的攻击（如消息重放）具有鲁棒性。本文采用形式化方法进行攻击者的自动合成，即可能导致协议故障的对抗过程。具体来说，给定一个形式化威胁模型，捕获分布式协议模型和网络拓扑，以及潜在攻击者的位置、目标和接口（输入和输出），我们自动合成一个攻击者。我们形式化了四个攻击者合成问题——针对总是成功的攻击者与有时失败的攻击者，以及永远攻击的攻击者与不永远攻击的攻击者——并提出了其中两个问题的算法解决方案。我们报告了一个名为KORG的原型实现及其在TCP上的案例研究。实验表明，KORG可以在几秒或几分钟内自动生成TCP的已知攻击。