关于 TDoS 攻击选择性防御形式化验证的准确性
网络与互联网体系结构
2017-09-14 v1 密码学与安全
计算机科学中的逻辑
摘要
电话拒绝服务（TDoS）攻击针对电话服务（如 Voice over IP (VoIP)），使合法用户无法拨打电话。现有试图缓解 TDoS 攻击的防御很少，其中大多数采用 IP 过滤，适用性有限。在我们之前的工作中，我们提出使用选择性策略来缓解 HTTP 应用层 DDoS 攻击，并证明了其在缓解不同类型攻击上的有效性。开发此类防御具有挑战性，因为存在许多设计选项，例如使用何种丢弃函数与选择算法。我们的第一个贡献是借助实验与形式化验证共同证明选择性策略适用于缓解 TDoS 攻击。我们利用形式化模型以远小于实验的代价来帮助决定采用哪些选择性策略。我们的第二个贡献是对形式化模型所得结果与实验结果进行详细比较。我们证明形式化方法是一种强大的工具，可用于指定缓解分布式拒绝服务攻击的防御，从而在实际实现前增加对我们所提防御的信心。
引用
@article{arxiv.1709.04162,
title = {On the Accuracy of Formal Verification of Selective Defenses for TDoS Attacks},
author = {Marcilio O. O. Lemos and Yuri Gil Dantas and Iguatemi E. Fonseca and Vivek Nigam},
journal= {arXiv preprint arXiv:1709.04162},
year = {2017}
}