On the Accuracy of Formal Verification of Selective Defenses for TDoS Attacks

TL;DR

This paper demonstrates that formal verification can effectively assess the accuracy of selective defense strategies against TDoS attacks, reducing experimental effort and increasing confidence in their effectiveness.

Contribution

It introduces a formal verification approach to evaluate selective defenses for TDoS attacks and compares formal results with experimental data for validation.

Findings

Formal verification aligns with experimental results.

Selective strategies are effective against TDoS attacks.

Formal methods can reduce testing effort and improve confidence.

Abstract

Telephony Denial of Service (TDoS) attacks target telephony services, such as Voice over IP (VoIP), not allowing legitimate users to make calls. There are few defenses that attempt to mitigate TDoS attacks, most of them using IP filtering, with limited applicability. In our previous work, we proposed to use selective strategies for mitigating HTTP Application-Layer DDoS Attacks demonstrating their effectiveness in mitigating different types of attacks. Developing such types of defenses is challenging as there are many design options, eg, which dropping functions and selection algorithms to use. Our first contribution is to demonstrate both experimentally and by using formal verification that selective strategies are suitable for mitigating TDoS attacks. We used our formal model to help decide which selective strategies to use with much less effort than carrying out experiments. Our second contribution is a detailed comparison of the results obtained from our formal models and the results obtained by carrying out experiments. We demonstrate that formal methods is a powerful tool for specifying defenses for mitigating Distributed Denial of Service attacks allowing to increase our confidence on the proposed defense before actual implementation.