Formalization and Analysis of Aeolus-based File System from Process Algebra Perspective

The secure transmission of information is receiving more and more attention nowadays. Aeolus is a novel platform designed to enhance the development of distributed applications by preventing unauthorized disclosure of information. And one of the most representative systems for information transmission is the file system, therefore it is of great significance to formally analyze the Aeolus-based file system. In this paper, we use Communicating Sequential Processes (CSP) to model and formalize the file system based on Aeolus. Moreover, we utilize the Process Analysis Toolkit (PAT) to simulate and verify the CSP description of our established model. We specifically verify the validity of five properties: Deadlock Freedom, Divergence Freedom, Reachability, Secrecy, and Integrity. The verification results demonstrate that the model successfully satisfies these properties, affirming the effectiveness of the framework in ensuring file operations and guaranteeing the secure transmission of information.