Formal verification of an intrusion-tolerant group membership protocol

The traditional approach for establishing thecorrectness of group communication protocols is through rigor-
ous 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 verifi-
cation 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 mem-
bership protocol that is part of an intrusion-tolerant group com-
munication system. We describe how we successfully tackled the
state-space explosion problem by determining the right abstrac-
tion 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.
key words: intrusion tolerance, group communication systems,
validation, formal methods