Formal analysis and improvement of the state transition model for intrusion tolerant system

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. © Springer-Verlag Berlin Heidelberg 2005.