Formalization and Analysis of Ceph Using Process Algebra
- 1 December 2021
- journal article
- research article
- Published by Institute of Electronics, Information and Communications Engineers (IEICE) in IEICE Transactions on Information and Systems
- Vol. E104.D (12), 2154-2163
- https://doi.org/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.Keywords
This publication has 12 references indexed in Scilit:
- The potential role of exosomes derived from ovarian cancer cells for diagnostic and therapeutic approachesJournal of Cellular Physiology, 2019
- On construction of a network log management system using ELK Stack with CephThe Journal of Supercomputing, 2019
- Modeling and Verifying HDFS Using Process AlgebraMobile Networks and Applications, 2017
- Modeling and Verifying Google File SystemPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2015
- Evaluating the performance and scalability of the Ceph distributed storage systemPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2014
- A Prefetching Mechanism Based on MooseFSCommunications in Computer and Information Science, 2014
- Scalable security for large, high performance storage systemsPublished by Association for Computing Machinery (ACM) ,2006
- Using CSP to detect errors in the TMN protocolIEEE Transactions on Software Engineering, 1997
- The Kerberos Network Authentication Service (V5)Published by RFC Editor ,1993
- Communicating sequential processesCommunications of the ACM, 1978