Modeling and Verifying Identity Authentication Security of HDFS using CSP

As one of the most popular software framework for distributed storage of big data, HDFS has lots of good features, such as high throughput and high fault-tolerance. However, with its rapid development, potential data security risks are exposed and founding security mechanism for HDFS cluster has become an important issue. In this paper, we investigate the identity authentication problem on HDFS and select Kerberos protocol as corresponding security mechanism to deal with the problem. We use the process algebra CSP to model HDFS and HDFS with security mechanism, as well as their security properties. Moreover, we also use a model checking tool PAT to verify these properties. The verification results illustrate the existence of authentication problems on HDFS and Kerberos can effectively solve these problems. Consequently, a better understanding of HDFS and its security properties can be achieved and the establishment of security mechanism for HDFS can benefit from it. Besides, it is also a guide for the formalization of HDFS with security mechanism.