Formal Verification of an Intrusion-Tolerant Group Membership Protocol

HariGovind V. RAMASAMY  Michel CUKIER  William H. SANDERS  

IEICE TRANSACTIONS on Information and Systems   Vol.E86-D   No.12   pp.2612-2622
Publication Date: 2003/12/01
Online ISSN: 
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)>>
Buy this Article

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.