IEICE TRANSACTIONS on Information
Formalization and Analysis of Ceph Using Process Algebra
Summary :
Ceph is an object-based parallel distributed file system that provides excellent performance, reliability, and scalability. Additionally, Ceph provides its Cephx authentication system to authenticate users, so that it can identify users and realize authentication. In this paper, we first model the basic architecture of Ceph using process algebra CSP (Communicating Sequential Processes). With the help of the model checker PAT (Process Analysis Toolkit), we feed the constructed model to PAT and then verify several related properties, including Deadlock Freedom, Data Reachability, Data Write Integrity, Data Consistency and Authentication. The verification results show that the original model cannot cater to the Authentication property. Therefore, we formalize a new model of Ceph where Cephx is adopted. In the light of the new verification results, it can be found that Cephx satisfies all these properties.
- Publication
- IEICE TRANSACTIONS on Information Vol.E104-D No.12 pp.2154-2163
- Publication Date
- 2021/12/01
- Publicized
- 2021/09/28
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2021EDP7070
- Type of Manuscript
- PAPER
- Category
- Software System
Authors
Ran LI
East China Normal University
Huibiao ZHU
East China Normal University
Jiaqi YIN
East China Normal University
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
Ran LI, Huibiao ZHU, Jiaqi YIN, "Formalization and Analysis of Ceph Using Process Algebra" in IEICE TRANSACTIONS on Information,
vol. E104-D, no. 12, pp. 2154-2163, December 2021, doi: 10.1587/transinf.2021EDP7070.
Abstract: Ceph is an object-based parallel distributed file system that provides excellent performance, reliability, and scalability. Additionally, Ceph provides its Cephx authentication system to authenticate users, so that it can identify users and realize authentication. In this paper, we first model the basic architecture of Ceph using process algebra CSP (Communicating Sequential Processes). With the help of the model checker PAT (Process Analysis Toolkit), we feed the constructed model to PAT and then verify several related properties, including Deadlock Freedom, Data Reachability, Data Write Integrity, Data Consistency and Authentication. The verification results show that the original model cannot cater to the Authentication property. Therefore, we formalize a new model of Ceph where Cephx is adopted. In the light of the new verification results, it can be found that Cephx satisfies all these properties.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2021EDP7070/_p
Copy
@ARTICLE{e104-d_12_2154,
author={Ran LI, Huibiao ZHU, Jiaqi YIN, },
journal={IEICE TRANSACTIONS on Information},
title={Formalization and Analysis of Ceph Using Process Algebra},
year={2021},
volume={E104-D},
number={12},
pages={2154-2163},
abstract={Ceph is an object-based parallel distributed file system that provides excellent performance, reliability, and scalability. Additionally, Ceph provides its Cephx authentication system to authenticate users, so that it can identify users and realize authentication. In this paper, we first model the basic architecture of Ceph using process algebra CSP (Communicating Sequential Processes). With the help of the model checker PAT (Process Analysis Toolkit), we feed the constructed model to PAT and then verify several related properties, including Deadlock Freedom, Data Reachability, Data Write Integrity, Data Consistency and Authentication. The verification results show that the original model cannot cater to the Authentication property. Therefore, we formalize a new model of Ceph where Cephx is adopted. In the light of the new verification results, it can be found that Cephx satisfies all these properties.},
keywords={},
doi={10.1587/transinf.2021EDP7070},
ISSN={1745-1361},
month={December},}
Copy
TY - JOUR
TI - Formalization and Analysis of Ceph Using Process Algebra
T2 - IEICE TRANSACTIONS on Information
SP - 2154
EP - 2163
AU - Ran LI
AU - Huibiao ZHU
AU - Jiaqi YIN
PY - 2021
DO - 10.1587/transinf.2021EDP7070
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E104-D
IS - 12
JA - IEICE TRANSACTIONS on Information
Y1 - December 2021
AB - Ceph is an object-based parallel distributed file system that provides excellent performance, reliability, and scalability. Additionally, Ceph provides its Cephx authentication system to authenticate users, so that it can identify users and realize authentication. In this paper, we first model the basic architecture of Ceph using process algebra CSP (Communicating Sequential Processes). With the help of the model checker PAT (Process Analysis Toolkit), we feed the constructed model to PAT and then verify several related properties, including Deadlock Freedom, Data Reachability, Data Write Integrity, Data Consistency and Authentication. The verification results show that the original model cannot cater to the Authentication property. Therefore, we formalize a new model of Ceph where Cephx is adopted. In the light of the new verification results, it can be found that Cephx satisfies all these properties.
ER -
English
