Abstract
Availability is an important security property for Internet services and a key ingredient of most service level agreements. It can be compromised by distributed Denial of Service (DoS) attacks. In this work we propose a formal pattern-based approach to study defense mechanisms against DoS attacks. We enhance pattern descriptions with formal models that allow the designer to give guarantees on the behavior of the proposed solution. The underlying executable specification formalism we use is the rewriting logic language Maude and its real-time and probabilistic extensions. We introduce the notion of stable availability, which means that with very high probability service quality remains very close to a threshold, regardless of how bad the DoS attack can get. Then we present two formal patterns which can serve as defenses against DoS attacks: the Adaptive Selective Verification (ASV) pattern, which enhances a communication protocol with a defense mechanism, and the Server Replicator (SR) pattern, which provisions additional resources on demand. However, ASV achieves availability without stability, and SR cannot achieve stable availability at a reasonable cost. As a main result we show, by statistical model checking with the PVeStA tool, that the composition of both patterns yields a new improved pattern which guarantees stable availability at a reasonable cost.
This work has been partially sponsored by the Software Engineering Elite Graduate Program, the EU-funded projects FP7-257414 ASCENS and FP7-256980 NESSoS, and AFOSR Grant FA8750-11-2-0084. The fourth author was also partially supported by the “Programa de Apoyo a la Investigación y Desarrollo” (PAID-02-11) of the Universitat Politècnica de València.
Chapter PDF
Similar content being viewed by others
Keywords
References
Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the Pi Calculus. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 340–354. Springer, Heidelberg (2004)
Agha, G., Frolund, S., Panwar, R., Sturman, D.: A linguistic framework for dynamic composition of dependability protocols. IFIP, pp. 345–363 (1993)
Agha, G., Gunter, C., Greenwald, M., Khanna, S., Meseguer, J., Sen, K., Thati, P.: Formal modeling and analysis of DoS using probabilistic rewrite theories. In: FCS (2005)
Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. ENTCS 153(2), 213–239 (2006)
AlTurki, M.: Rewriting-based formal modeling, analysis and implementation of real-time distributed services. PhD thesis, University of Illinois (2011)
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)
AlTurki, M., Meseguer, J., Gunter, C.: Probabilistic modeling and analysis of DoS protection for the ASV protocol. ENTCS 234, 3–18 (2009)
Chadha, R., Gunter, C.A., Meseguer, J., Shankesi, R., Viswanathan, M.: Modular Preservation of Safety Properties by Cookie-Based DoS-Protection Wrappers. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 39–58. Springer, Heidelberg (2008)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Dong, J., Alencar, P.S.C., Cowan, D.D., Yang, S.: Composing pattern-based components and verifying correctness. JSS 80, 1755–1769 (2007)
Eckhardt, J.: A Formal Analysis of Security Properties in Cloud Computing. Master’s thesis, LMU Munich (2011)
Erl, T.: SOA Design Patterns. Prentice Hall (2008)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley (1995)
Gunter, C., Khanna, S., Tan, K., Venkatesh, S.: DoS Protection for Reliably Authenticated Broadcast. In: NDSS (2004)
Khanna, S., Venkatesh, S., Fatemieh, O., Khan, F., Gunter, C.: Adaptive Selective Verification. In: IEEE INFOCOM, pp. 529–537 (2008)
Lafrance, S., Mullins, J.: An Information Flow Method to Detect Denial of Service Vulnerabilities. JUCS 9(11), 1350–1369 (2003)
Wirsing, M., et al.: Sensoria Patterns: Augmenting Service Engineering. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 170–190. Springer, Heidelberg (2008)
Mahimkar, A., Shmatikov, V.: Game-based Analysis of Denial-of-Service Prevention Protocols. In: IEEE CSFW, pp. 287–301 (2005)
MasterCard. MasterCard Statement (September 2011), http://www.businesswire.com/news/home/20101208005866/en/MasterCard-Statement
Meadows, C.: A Formal Framework and Evaluation Method for Network Denial of Service. In: IEEE CSFW (1999)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. TCS 96(1), 73–155 (1992)
Meseguer, J., Talcott, C.: Semantic Models for Distributed Object Reflection. In: Deng, T. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 1–36. Springer, Heidelberg (2002)
Mühlbauer, T.: Formal Specification and Analysis of Cloud Computing Management. Master’s thesis, LMU Munich (2011)
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. HOSC 20(1–2), 161–196 (2007)
Schumacher, M., Fernandez-Buglioni, E., Hybertson, D., Buschmann, F., Sommerlad, P.: Security Patterns. Wiley (2005)
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)
W3C. Request-Response Message Exchange Pattern (September 2011), http://www.w3.org/TR/2003/PR-soap12-part2-20030507/#singlereqrespmep
Walfish, M., Vutukuru, M., Balakrishnan, H., Karger, D.R., Shenker, S.: DDoS defense by offense. In: ACM SIGCOMM, pp. 303–314 (2006)
Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. JIC 204(9), 1368–1409 (2006)
Yu, C.-F., Gligor, V.: A Specification and Verification Method for Preventing Denial of Service. IEEE T-SE 16(6), 581–592 (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eckhardt, J., Mühlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M. (2012). Stable Availability under Denial of Service Attacks through Formal Patterns. In: de Lara, J., Zisman, A. (eds) Fundamental Approaches to Software Engineering. FASE 2012. Lecture Notes in Computer Science, vol 7212. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28872-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-28872-2_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28871-5
Online ISBN: 978-3-642-28872-2
eBook Packages: Computer ScienceComputer Science (R0)