Geodesic
Formalization and Verification of Kafka Messaging Mechanism Using CSP
Computer Science and Information Systems, Tome 20 (2023) no. 1 Cet article a éte moissonné depuis la source Computer Science and Information Systems website

Voir la notice de l'article

Apache Kafka is an open source distributed messaging system based on the publish-subscribe model, which achieves low latency, high throughput and good load balancing. 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. The formal methods can analyze whether a model is highly credible. Therefore, it is significant to analyze Kafka messaging mechanism which describes the communication process and rules between each module entity in Kafka from the perspective of formal methods. In this paper, we apply the process algebra CSP (Communicating Sequential Processes) and the model checking tool PAT (Process Analysis Toolkit) to analyze Kafka messaging mechanism. The results of verification show that the model caters for its specification and guarantees the reliability of messages in the normal communication process. Moreover, in order to further analyze the security of Kafka messaging mechanism, we add the intruder model and the authentication protocol Kerberos model and compare the verification results of Kafka messaging mechanism with or without the secure protocol Kerberos. The results show that the Kerberos protocol has improved the security of Kafka messaging mechanism in some aspects, but there are still some security loopholes.
Keywords: Distributed Messaging System, Kafka Messaging Mechanism, CSP, Formalization, Verification 
@article{CSIS_2023_20_1_a17,
     author = {Junya Xu and Jiaqi Yin and Huibiao Zhu and Lili Xiao},
     title = {Formalization and {Verification} of {Kafka} {Messaging} {Mechanism} {Using} {CSP}},
     journal = {Computer Science and Information Systems},
     year = {2023},
     volume = {20},
     number = {1},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a17/}
}
TY  - JOUR
AU  - Junya Xu
AU  - Jiaqi Yin
AU  - Huibiao Zhu
AU  - Lili Xiao
TI  - Formalization and Verification of Kafka Messaging Mechanism Using CSP
JO  - Computer Science and Information Systems
PY  - 2023
VL  - 20
IS  - 1
UR  - http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a17/
ID  - CSIS_2023_20_1_a17
ER  - 
%0 Journal Article
%A Junya Xu
%A Jiaqi Yin
%A Huibiao Zhu
%A Lili Xiao
%T Formalization and Verification of Kafka Messaging Mechanism Using CSP
%J Computer Science and Information Systems
%D 2023
%V 20
%N 1
%U http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a17/
%F CSIS_2023_20_1_a17
Junya Xu; Jiaqi Yin; Huibiao Zhu; Lili Xiao. Formalization and Verification of Kafka Messaging Mechanism Using CSP. Computer Science and Information Systems, Tome 20 (2023) no. 1. http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a17/