Formal Verification of an Intrusion-Tolerant Group Membership Protocol
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E86-D No.12 pp.2612-2622
- Publication Date
- 2003/12/01
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Issue on Dependable Computing)
- Category
- Verification and Dependability Analysis
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
HariGovind V. RAMASAMY, Michel CUKIER, William H. SANDERS, "Formal Verification of an Intrusion-Tolerant Group Membership Protocol" in IEICE TRANSACTIONS on Information,
vol. E86-D, no. 12, pp. 2612-2622, December 2003, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e86-d_12_2612/_p
Copy
@ARTICLE{e86-d_12_2612,
author={HariGovind V. RAMASAMY, Michel CUKIER, William H. SANDERS, },
journal={IEICE TRANSACTIONS on Information},
title={Formal Verification of an Intrusion-Tolerant Group Membership Protocol},
year={2003},
volume={E86-D},
number={12},
pages={2612-2622},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={December},}
Copy
TY - JOUR
TI - Formal Verification of an Intrusion-Tolerant Group Membership Protocol
T2 - IEICE TRANSACTIONS on Information
SP - 2612
EP - 2622
AU - HariGovind V. RAMASAMY
AU - Michel CUKIER
AU - William H. SANDERS
PY - 2003
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E86-D
IS - 12
JA - IEICE TRANSACTIONS on Information
Y1 - December 2003
AB - 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.
ER -
English
