Visible to the public Resource-Bounded Intruders in Denial of Service Attacks

TitleResource-Bounded Intruders in Denial of Service Attacks
Publication TypeConference Paper
Year of Publication2019
AuthorsAires Urquiza, Abraão, AlTurki, Musab A., Kanovich, Max, Ban Kirigin, Tajana, Nigam, Vivek, Scedrov, Andre, Talcott, Carolyn
Conference Name2019 IEEE 32nd Computer Security Foundations Symposium (CSF)
Date Publishedjun
PublisherIEEE
ISBN Number978-1-7281-1407-1
Keywordsamplification DoS attacks, Analytical models, Bandwidth, Collaboration, Complexity, composability, compositionality, computational complexity, Computer crime, computer network security, DDoS, Denial of Service attacks, Dolev-Yao intruder, DoS problem, existing resource-conscious protocol verification models, formal methods, formal protocol verification, formal specification, formal verification, formal verification model, Policy Based Governance, policy-based governance, powerful intruders, privacy, protocol execution, protocol theories, protocol verification, Protocols, PSPACE-complete, pubcrawl, reachability analysis, Real-time Systems, refined intruder model, resource-bounded intruders, rewriting modulo SMT, rewriting systems, serious security concern, Servers, service resource usage, service unavailable, Tools, unlimited resources
Abstract

Denial of Service (DoS) attacks have been a serious security concern, as no service is, in principle, protected against them. Although a Dolev-Yao intruder with unlimited resources can trivially render any service unavailable, DoS attacks do not necessarily have to be carried out by such (extremely) powerful intruders. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable even to resource-bounded intruders that cannot generate or intercept arbitrary large volumes of traffic. This paper proposes a novel, more refined intruder model where the intruder can only consume at most some specified amount of resources in any given time window. Additionally, we propose protocol theories that may contain timeouts and specify service resource usage during protocol execution. In contrast to the existing resource-conscious protocol verification models, our model allows finer and more subtle analysis of DoS problems. We illustrate the power of our approach by representing a number of classes of DoS attacks, such as, Slow, Asymmetric and Amplification DoS attacks, exhausting different types of resources of the target, such as, number of workers, processing power, memory, and network bandwidth. We show that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems. Finally, we implemented our formal verification model in the rewriting logic tool Maude and analyzed a number of DoS attacks in Maude using Rewriting Modulo SMT in an automated fashion.

URLhttps://ieeexplore.ieee.org/document/8823756
DOI10.1109/CSF.2019.00033
Citation Keyaires_urquiza_resource-bounded_2019