形式发现与复现网络协议漏洞
密码学与安全
2025-03-04 v1 形式语言与自动机理论
网络与互联网体系结构
摘要
网络威胁的快速演变增加了发现日益复杂多样网络协议漏洞的需求。这篇论文引入了 Network Attack-centric Compositional Testing（NACT），这是一种新方法，旨在发现网络协议的新型漏洞并通过攻击者模型创建复现这些漏洞的情景。NACT 集成了可组合的攻击者规范、形式规范突变和随机约束求解技术，以生成复杂的攻击情景和测试用例。该方法使单协议和多协议交互的全面测试成为可能。通过针对自定义精简协议（MiniP）和五种广泛使用的 QUIC 实现进行案例研究，NACT 被证明能够有效识别、复现并发现新的实际漏洞，如版本协商滥用。此外，通过比较当前和旧版 QUIC 实现，NACT 展示了其检测持续漏洞和回归的能力。最后，通过在黑盒测试框架内支持跨协议测试，NACT 提供了一种灵活的方法来提高网络协议的安全性。
引用
@article{arxiv.2503.01538,
title = {Formally Discovering and Reproducing Network Protocols Vulnerabilities},
author = {Christophe Crochet and John Aoga and Axel Legay},
journal= {arXiv preprint arXiv:2503.01538},
year = {2025}
}