Formalization and Verification of the Message Delivery Mechanism in Apache Pulsar

Apache Pulsar is a cloud-native, high-performance, and scalable distributed Message-Oriented Middleware (MOM) widely used for processing large-scale real-time data streams. Due to its distributed architecture and multi-tenancy features, Pulsar excels in high-throughput and low-latency scenarios and has been widely applied in fields such as finance, the Internet of Things (IoT), and big data processing. However, as the complexity of application scenarios increases, the requirements for system reliability and data security are also rising. Formal methods, based on rigorous mathematical theories, have been widely used for the verification and analysis of distributed systems. Therefore, exploring how to apply formal methods to the modeling and verification of message delivery mechanism of Apache Pulsar holds important research significance. This paper employs formal methods to model the message delivery mechanism of Apache Pulsar and conducts an in-depth analysis of its reliability and security, aiming to provide theoretical support and technical references for building secure and reliable Message-Oriented Middleware. The specific research content includes: (1) Based on the theory of Communicating Sequential Processes (CSP), this paper formalizes a complete system model of Pulsar. We formalize message-delivery components as concurrent processes to describe their communication behaviors. (2) Utilizing the Process Analysis Toolkit (PAT), the constructed formal model is implemented and verified. It verifies six key properties: deadlock freedom, divergence freedom, data consistency, sequentiality, reliability, and persistent storage. The experimental results indicate that Pulsar successfully meets these critical properties. (3) By constructing an intruder model to simulate attacks in network environments and introducing the Athenz authentication framework into the Pulsar system, the security of its message delivery mechanism is further validated. In unsafe networks, interception attacks remain feasible; however, our intruder-model tests demonstrate that Athenz effectively thwarts impersonation attacks.