Cloud communication, as a core component of the cloud computing architecture, relies on the communication mechanism of TCP/UDP protocols. However, with the popularity of cloud communication, the security threats that it faces are also becoming increasingly severe. Graphene is a new cloud communication security architecture that targets both TCP and UDP communication. It provides security assurance during data transmission and authentication for cloud users and cloud service providers, effectively addressing some of the shortcomings of traditional security protocols. In light of Graphene’s advantages, it is gaining increasing attention from industries. Hence, ensuring the reliability of Graphene becomes paramount. In this paper, we first utilize process algebra CSP to model the TCP-based communication processes within the Graphene architecture. Subsequently, we model the UDP-based communication processes as well. Then, we employ the model checker PAT to run the CSP models for both protocols and subsequently verify six properties: Deadlock Freedom, Divergence Freedom, Data Reachability, Cloud User Faking, Cloud Instance Faking, and Central Key Server Faking. According to the verification results, our models for both TCP and UDP satisfy all of the aforementioned properties. Therefore, we can conclude that the communication execution processes for both TCP and UDP in the Graphene architecture fulfill the anticipated security standards, thus indicating the reliability of the system.

Cloud communication, as a core component of the cloud computing architecture, relies on the communication mechanism of TCP/UDP protocols.However, with the popularity of cloud communication, the security threats that it faces are also becoming increasingly severe.Graphene is a new cloud communication security architecture that targets both TCP and UDP communication.It provides security assurance during data transmission and authentication for cloud users and cloud service providers, effectively addressing some of the shortcomings of traditional security protocols.In light of Graphene's advantages, it is gaining increasing attention from industries.Hence, ensuring the reliability of Graphene becomes paramount.In this paper, we first use process algebra CSP to model the TCP-based communication process of the Graphene architecture.Then, we use the model checker PAT to run the CSP model of Graphene and subsequently verify six properties, including Deadlock Freedom, Divergence Freedom, Data Reachability, Cloud User Faking, Cloud Instance Faking, and Central Key Server Faking.According to the verification results, our model satisfies all the above six properties.Therefore, we can conclude that the TCP communication execution process in the Graphene architecture fulfills the anticipated security standards, thus indicating that the system is reliable.

Apache Pulsar is a distributed publish-subscribe messaging system that employs a compute-storage separation architecture, which is well-suited for cloud-native environments.Message delivery mechanism is the core function in Pulsar, mainly for transferring data between different objects.The reliability of the message delivery mechanism of Pulsar raises extensive concerns for better application.In this paper, we use process algebra CSP to model the components of Pulsar.By implementing the model using model checker PAT, we mathematically examine the message delivery mechanism of Pulsar.We verify six properties: deadlock freedom, divergence freedom, data consistency, sequentiality, reliability and persistent storage.The verification results indicate that Pulsar satisfies all these properties, demonstrating that it has good performance and can provide robust message transmission services.

Dubbo is a high-performance, lightweight Java Remote Procedure Call (RPC) framework developed by Alibaba, which provides interface-oriented remote method call, intelligent fault tolerance and automatic service registration.Since Dubbo is extensively applied recently as an excellent representative RPC framework, it is of great significance to formally analyze Dubbo.In this paper, we use Communicating Sequential Processes (CSP) to model and formalize Dubbo.In order to enhance the reliability of the call, we use token authentication mechanism in the modeling process.Moreover, we put the CSP description of the established model into the model checker Process Analysis Toolkit (PAT) for simulation and verification.We verify whether the four properties are valid, including Deadlock Freedom, Connectivity, Robustness and Parallelism.Our final verification results show that the model can satisfy these properties, thus we can conclude the framework can guarantee the highly available remote call.