Formalization And Verification Of Kafka Messaging Mechanism Using CSP

Message queue middleware(MQM)is an important component of distributed system,which allows an application to focus on the data rather than the details of data transmission.Thus MQM can solve some problems such as asynchronous transmission of messages,decouping of applications,flow peak-cutting,etc.Kafka is an open source distributed messaging system based on publish-and-subscribe model,which achieves low latency,high throughput and good load balancing.It has been widely used by Internet companies such as Twitter,Yahoo,etc.As a popular messaging system,the transmission of messages between applications is one of the core functions of Kafka.Therefore,the reliability and security of data in the process of message transmission in Kafka have become the focus of attention.Kafka messaging system includes three basic modules: producer,server and con-sumer.And Kafka messaging mechanism describes in detail the communication process and rules between each module entity to ensure the correct transmission of messages in the communication process of the system.At the same time,the formal methods can analyze whether a system is reliable from the perspective of mathematical logic.There-fore,we chooses to use Communicating Sequential Processes(CSP)in formal methods to model and analyze the Kafka messaging mechanism.And we complete the modeling of messaging mechanism by abstracting the entities in the three modules into processes and describing the communication and interaction between processes in a formal way.Then we briefly describe the five properties of Kafka messaging mechanism to ensure data reliability,including Deadlock Freeness,Consistency,Parallelism,Sequentiality and Fault Tolerance.And we complete the coding implementation and property verification of the formal model in the Model Checking tool Process Analysis Toolkit(PAT).From the verification results in PAT,we conclude that Kafka messaging mechanism satisfies the above properties.Thus it is verified that the Kafka messaging mechanism can guarantee the correctness and reliability of messages in the normal communication process.Finally,in order to further analyze the security of Kafka messaging mechanism,we added the intruder model and the authentication protocol Kerberos model on the basis of the original model.By imitating the attack behavior of the intruder in the real network environment,we compare the verification results of Kafka messaging mechanism with or without the secure protocol Kerberos.The results show that the Kerberos protocol can prevent the intruder from disguising the entity process,but it cannot prevent the intruder from intercepting and stealing messages in normal communication.Therefore,we believe that the Kerberos protocol has improved the security of Kafka messaging mechanism in some aspects,but there are still some security loopholes.