For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Formal Verification of an Intrusion-Tolerant Group Membership Protocol
HariGovind V. RAMASAMY Michel CUKIER William H. SANDERS
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2003/12/01
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Issue on Dependable Computing)
Category: Verification and Dependability Analysis
intrusion tolerance, group communication systems, validation, formal methods,
Full Text: PDF(538.5KB)>>
The traditional approach for establishing the correctness of group communication protocols is through rigorous arguments. While this is a valid approach, the likelihood of subtle errors in the design and implementation of such complex distributed protocols is not negligible. The use of formal verification methods has been widely advocated to instill confidence in the correctness of protocols. In this paper, we describe how we used the SPIN model checker to formally verify a group membership protocol that is part of an intrusion-tolerant group communication system. We describe how we successfully tackled the state-space explosion problem by determining the right abstraction level for formally specifying the protocol. The verification exercise not only formally showed that the protocol satisfies its correctness claims, but also provided information that will help us make the protocol more efficient without violating correctness.