Abstract
Intrusion tolerance is an emerging network security technique, which enables the victim server systems to continue offering services (or degraded services) after being attacked. A state transition model has been presented to describe the dynamic behaviors of intrusion tolerant systems. In this paper, we build an attack finite state system based on the recent network attacks, and use SMV, a model checking tool, to analyze the intrusion tolerant systems by the interaction of the system model and the attack model. The analysis results demonstrate that not all types of attacks can be mapped to the system model. We improve this state transition model, whose correctness is proved by SMV. In addition, we give two attack instances mapped to our improved model.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Sargor, C., Goseva-Popstojanova, K., Trivedi, K., Wang, F., Gong, F., Jou, F.: Sitar: A scalable intrusion-tolerant architecture for distributed services. In: Proceeding of 2nd Annual IEEE Systems, Man, and Cybernetics Informations Assurance Workshop, West Point, NY, June 2001. IEEE Computer Society Press, Los Alamitos (2001)
Gong, F., Vaidyanathan, K., Trivedi, K., Goseva-Popstojanova, K., Wang, F., Muthusamy, B.: Characterizing intrusion tolerant systems using a state transition model. In: Proceeding of DARPA Information Survivability Conference and Exposition II, DISCEX 2001, June 12-14, vol. 2, pp. 211–221 (2001)
Clarke, E.M., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131. Springer, Heidelberg (1982)
Emerson, E.A., Clarke, E.M., Sistla, A.P.: Automatic verification of finite states concurrent systems using temporal logic specification. ACM Transactions on Programming Languages and Systems 1(2), 244–263 (1986)
Grumberg, O., Clarke, E.M., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
McMillan, K.: SMV documentation postscript versions, http://www.cad.eecs.berkeley.edu/kenmcmil/psdoc.html
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Rocky, C.K.C.: Defending against flooding-based distribute denial-of-service attacks. IEEE Communications Magazine (October 2002)
Voelker, G., Moore, D., Savage, S.: Inferring internet denial-of-service activity. In: Proceeding of 10th USENIX Sevurity Symposium (2001)
Computer Emergency Response Team. Results of distributed systems intruder tools (October 1999), http://www.cert.org/reports/distworkshop-final.html
Partidge, C., Snoeren, A.C., Luis, A.: Hash-based IP traceback. In: Proceedings of ACM SIGCOMM (2001)
http://www.cisco.com/warp/public/707/cisco-sa-20030717-blocked.html
Postel, J.: Transmission control protocol RFC792 (September 1981)
Su, K.: Model checking temporal logics of knowledge in distributed systems. In: Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, pp. 98–103. AAAI Press/The MIT Press (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Su, K., Zhao, C., Lv, G., Lin, H., Chen, Q. (2005). Formal Analysis and Improvement of the State Transition Model for Intrusion Tolerant System. In: Deng, X., Ye, Y. (eds) Internet and Network Economics. WINE 2005. Lecture Notes in Computer Science, vol 3828. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11600930_39
Download citation
DOI: https://doi.org/10.1007/11600930_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30900-0
Online ISBN: 978-3-540-32293-1
eBook Packages: Computer ScienceComputer Science (R0)