Abstract
Telephony Denial of Service (TDoS) attacks target telephony services, such as Voice over IP, 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 recent work, we proposed to use selective strategies for mitigating HTTP Application-Layer DDoS Attacks demonstrating their effectiveness in mitigating different types of attacks. This paper demonstrates that selective strategies can also be successfully used to mitigate TDoS attacks, in particular, two attacks: the Coordinated Call Attack and the Prank Call attack. We formalize a novel selective strategy for mitigating these attacks in the computational tool Maude and verify these defenses using the statistical model checker PVeStA. When compared to our experimental results (reported elsewhere), the results obtained by using formal methods were very similar. This 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
This can be easily done for many VoIP services.
- 2.
Notice that although our experiments on the network were controlled experiments, they used off-the-shelf tools, such as Apache web-servers, which implement a number of optimizations, and our experiments suffered from interferences that cannot be controlled, such as network latency.
- 3.
In fact, we omit some steps carried out by the server to find Bob in the network. This step can lead to DDoS amplification attacks [13] for which known solutions exists. Such amplification attacks are not, however, the main topic of this paper.
- 4.
Or alternatively two honest users that have been infected to be zombies by some attacker.
- 5.
The value of \(t_M\) can be obtained by the history of a VoIP provider’s usage.
- 6.
We used a Poisson distribution because such distributions are normally used for modeling telephone calls arrival.
- 7.
For the sake of presentation, we simplified here some aspects such as the use of the scheduler appearing in the complete model which can be found in [11].
- 8.
Note that there is a value delay inserted when a message is sent in order to have a more realistic model.
References
Cyber threat bulletin: boston hospital TDoS attack. http://voipsecurityblog.typepad.com/files/cyber-threat-bulletin-13-06-boston-hospital-telephony-denial-of-service-attack.pdf. Accessed 27 Sep 2015
TDoS- extortionists jam phone lines of public services including hospitals. https://nakedsecurity.sophos.com/pt/2014/01/22/tdos-extortionists-jam-phone-lines-of-public-services-including-hospitals/. Accessed 27 Sep 2015
Situational advisory: recent telephony denial of services (TDoS) attacks. http://voipsecurityblog.typepad.com/files/ky-fusion_tdos_3-29-13-2.pdf/. Accessed 27 Sep 2015
Dantas, Y.G., Nigam, V., Fonseca, I.E.: A selective defense for application layer DDoS attacks. In: JISIC 2014, pp. 75–82 (2014)
The Surging Threat of Telephony Denial of Service Attacks. http://voipsecurityblog.typepad.com/files/tdos_paper_4-11-13.pdf. Accessed 28 Sep 2015
TDoS extortionists jam phone lines of public services, including hospitals. https://nakedsecurity.sophos.com/2014/01/22/tdos-extortionists-jam-phone-lines-of-public-services-including-hospitals/. Accessed 28 Nov 2015
Zargar, S.T., Joshi, J., Tipper, D.: A survey of defense mechanisms against distributed denial of service (DDoS) flooding attacks. IEEE Commun. Surv. Tutorials 15(4), 2046–2069 (2013)
Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005)
AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011)
Lemos, M.O.O., Dantas, Y.G., Fonseca, I.E., Nigam, V.: A selective defense for mitigating coordinated call attacks (submitted)
ygdantas. Seven: repository (2013). https://github.com/ygdantas/SeVen.git
SIP: Session initiation protocol. http://www.ietf.org/rfc/rfc3261.txt
Shankesi, R., AlTurki, M., Sasse, R., Gunter, C.A., Meseguer, J.: Model-checking DoS amplification for VoIP session initiation. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 390–405. Springer, Heidelberg (2009)
Khanna, S., Venkatesh, S.S., Fatemieh, O., Khan, F., Gunter, C.A.: Adaptive selective verification. In: INFOCOM, pp. 529–537 (2008)
Eckhardt, J., Mühlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable availability under denial of service attacks through formal patterns. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 78–93. Springer, Heidelberg (2012)
Eckhardt, J., Mühlbauer, T., Meseguer, J., Wirsing, M.: Statistical model checking for composite actor systems. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 143–160. Springer, Heidelberg (2013)
Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci. 153(2), 213–239 (2006)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)
Huici, F., Niccolini, S., D’Heureuse, N.: Protecting SIP against very large flooding DoS attacks. In: GLOBECOM 2009, pp. 1369–1374. IEEE Press, Piscataway (2009)
Yu-Sung, W., Bagchi, S., Garg, S., Singh, N., Tsai, T.: SCIDIVE: a stateful and cross protocol intrusion detection architecture for voice-over-IP environments. In: DSN 2004, p. 433. IEEE Computer Society, Washington, DC (2004)
Meadows, C.: A formal framework and evaluation method for network denial of service. In: CSFW, pp. 4–13 (1999)
Mahimkar, A., Shmatikov, V.: Game-based analysis of denial-of-service prevention protocols. In: CSFW, pp. 287–301 (2005)
AlTurki, M., Meseguer, J., Gunter, C.A.: Probabilistic modeling and analysis of DoS protection for the ASV protocol. Electr. Notes Theor. Comput. Sci. 234, 3–18 (2009)
Henrique, J., Fonseca, I.E., Nigam, V.: Mitigating high-rate application layer DDoS attacks in software defined networks (submitted)
Acknowledgments
This work was supported by the Hessian excellence initiative LOEWE at the Center for Advanced Security Research Darmstadt (CASED), by RNP, by Capes and CNPq.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Dantas, Y.G., Lemos, M.O.O., Fonseca, I.E., Nigam, V. (2016). Formal Specification and Verification of a Selective Defense for TDoS Attacks. In: Lucanu, D. (eds) Rewriting Logic and Its Applications. WRLA 2016. Lecture Notes in Computer Science(), vol 9942. Springer, Cham. https://doi.org/10.1007/978-3-319-44802-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-44802-2_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-44801-5
Online ISBN: 978-3-319-44802-2
eBook Packages: Computer ScienceComputer Science (R0)