Formal Specification of the Intrusion-Tolerant System by Using Object-Z

Abstract

Intrusion-tolerance is the technique of using fault-tolerance to achieve security properties. It attempts to maintain acceptable service despite such intrusions, and so is considered as the ultimate defense of the system. To support the engineers in designing and developing a more correct and trustworthy such system, and so improve its quality, it is clear that formalize its safety requirements in a precise and unambiguous way is very necessary. But to our knowledge, such work has not been investigated in the literature. In this paper, with the use of Object Z, a formal language for system specification in an object-oriented style, we take an intrusion-tolerant conference key distributed system as an example to describe the components needed to formalize of an intrusion-tolerant system in the Object Z formalism, and illustrates how these components can be combined via inheritance to produce complete model of intrusion-tolerant system. The specification is useful and helpful not only for improving the quality of intrusion-tolerant system, but also for implementing more strict system testing.