Computer Science and Information Systems 2023 Volume 20, Issue 1, Pages: 277-306
https://doi.org/10.2298/CSIS210707057X
Full text (
1887 KB)
Cited by
Formalization and verification of Kafka messaging mechanism using CSP
Xu Junya (Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China), hbzhu@sei.ecnu.edu.cn
Yin Jiaqi (Northwestern Polytechnical University, Xi’an, China), jqyin@nwpu.edu.cn
Zhu Huibiao (Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China)
Xiao Lili (Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China)
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
Show references
Rabbitmq., https://www.rabbitmq.com/tutorials/amqp-concepts.html
Adams, C.: Kerberos authentication protocol. In: van Tilborg, H.C.A., Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd Ed, pp. 674-675. Springer (2011), https: //doi.org/10.1007/978-1-4419-5906-5_81
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560-599 (1984), https://doi.org/10.1145/828.833
Clarke, E.M., Henzinger, T.A., Veith, H.: Introduction to model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1-26. Springer (2018), https://doi.org/10.1007/978-3-319-10575-8_1
Dobbelaere, P., Esmaili, K.S.: Kafka versus rabbitmq: A comparative study of two industry reference publish/subscribe implementations: Industry paper. In: Proceedings of the 11th ACM International Conference on Distributed and Event-based Systems, DEBS 2017, Barcelona, Spain, June 19-23, 2017. pp. 227-238. ACM (2017), https://doi.org/10.1145/ 3093742.3093908
Eugster, P.T., Felber, P., Guerraoui, R., Kermarrec, A.: The many faces of publish/subscribe. ACM Comput. Surv. 35(2), 114-131 (2003), https://doi.org/10.1145/857076.857078
Fei, Y., Zhu, H.: Modeling and verifying NDN access control using CSP. In: Sun, J., Sun, M. (eds.) Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11232, pp. 143-159. Springer (2018), https://doi.org/10.1007/978-3-030-02450-5_9
Hesse, G., Matthies, C., Uflacker, M.: How fast can we insert? an empirical performance evaluation of apache kafka. In: 26th IEEE International Conference on Parallel and Distributed Systems, ICPADS 2020, Hong Kong, December 2-4, 2020. pp. 641-648. IEEE (2020), https://doi.org/10.1109/ICPADS51040.2020.00089
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666-677 (1978), https://doi.org/10.1145/359576.359585
Lee, V.Y., Liu, Y., Zhang, X., Phua, C., Sim, K., Zhu, J., Biswas, J., Dong, J.S., Mokhtari, M.: ACARP: auto correct activity recognition rules using process analysis toolkit (PAT). In: Donnelly, M.P., Paggetti, C., Nugent, C.D., Mokhtari, M. (eds.) Impact Analysis of Solutions for Chronic Disease Prevention and Management - 10th International Conference on Smart Homes and Health Telematics, ICOST 2012, Artiminio, Italy, June 12-15, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7251, pp. 182-189. Springer (2012), https:// doi.org/10.1007/978-3-642-30779-9_23
Liu, A., Zhu, H., Popovic, M., Xiang, S., Zhang, L.: Formal analysis and verification of the PSTM architecture using CSP. J. Syst. Softw. 165, 110559 (2020), https://doi.org/10.1016/j.jss.2020.110559
Lowe, G., Roscoe, A.W.: Using CSP to detect errors in the TMN protocol. IEEE Trans. Software Eng. 23(10), 659-669 (1997), https://doi.org/10.1109/32.637148
PAT: Process analysis toolkit., http://pat.comp.nus.edu.sg/
Prabhu, C., Gandhi, R.V., Jain, A.K., Lalka, V.S., Thottempudi, S.G., Rao, P.P.: A novel approach to extend KM models with object knowledge model (OKM) and kafka for big data and semantic web with greater semantics. In: Barolli, L., Hussain, F.K., Ikeda, M. (eds.) Complex, Intelligent, and Software Intensive Systems - Proceedings of the 13th International Conference on Complex, Intelligent, and Software Intensive Systems, CISIS 2019, Sydney, NSW, Australia, 3-5 July 2019. Advances in Intelligent Systems and Computing, vol. 993, pp. 544-554. Springer (2019), https://doi.org/10.1007/978-3-030-22354-0_48
Rooney, S., Urbanetz, P., Giblin, C., Bauer, D., Froese, F., Garc´es-Erice, L., Tomic, S.: Kafka: the database inverted, but not garbled or compromised. In: Baru, C., Huan, J., Khan, L., Hu, X., Ak, R., Tian, Y., Barga, R.S., Zaniolo, C., Lee, K., Ye, Y.F. (eds.) 2019 IEEE International Conference on Big Data (Big Data), Los Angeles, CA, USA, December 9-12, 2019. pp. 3874- 3880. IEEE (2019), https://doi.org/10.1109/BigData47090.2019.9005583
Sharvari T, S.N.K.: A study on modern messaging systems- kafka, rabbitmq and NATS streaming. CoRR abs/1912.03715 (2019), http://arxiv.org/abs/1912.03715
Si, Y., Sun, J., Liu, Y., Dong, J.S., Pang, J., Zhang, S.J., Yang, X.: Model checking with fairness assumptions using PAT. Frontiers Comput. Sci. 8(1), 1-16 (2014), https://doi.org/10.1007/s11704-013-3091-5
Skeirik, S., Bobba, R.B., Meseguer, J.: Formal analysis of fault-tolerant group key management using zookeeper. In: 13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013, Delft, Netherlands, May 13-16, 2013. pp. 636-641. IEEE Computer Society (2013), https://doi.org/10.1109/CCGrid.2013.98
Sun, D., Zhu, H., Fei, Y., Xiao, L., Lu, G., Yin, J.: Formalization and verification of TESAC using CSP. Int. J. Softw. Eng. Knowl. Eng. 29(11&12), 1741-1760 (2019), https://doi.org/10.1142/S0218194019400199
Sun, J., Liu, Y., Dong, J.S.: Model checking CSP revisited: Introducing a process analysis toolkit. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation, Third International Symposium, ISoLA 2008, Porto Sani, Greece, October 13-15, 2008. Proceedings. Communications in Computer and Information Science, vol. 17, pp. 307-322. Springer (2008), https://doi.org/10.1007/978-3-540-88479-8_ 22
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 709-714. Springer (2009), https://doi.org/10.1007/978-3-642-02658-4_59
Tbatou, Z., Asimi, A., Asimi, Y., Sadqi, Y., Guezzaz, A.: A new mutuel kerberos authentication protocol for distributed systems. Int. J. Netw. Secur. 19(6), 889- 898 (2017), http://ijns.jalaxy.com.tw/contents/ijns-v19-n6/ijns-2017-v19-n6-p889-898.pdf
Thampibal, L., Vatanawood, W.: Formalizing railway network using hierarchical timed coloured petri nets. In: ICIT 2019 - The 7th International Conference on Information Tech nology: IoT and Smart City, Shanghai, China, December 20-23, 2019. pp. 338-343. ACM (2019), https://doi.org/10.1145/3377170.3377221
Treat, T.: Benchmarking nats streaming and apache kafka., https://dzone.com/articles/benchmarking-nats-streaming-and-apachekafka
Vucnik, M., Svigelj, A., Kandus, G., Mohorcic, M.: Secure hybrid publish-subscribe messaging architecture. In: Begusic, D., Rozic, N., Radic, J., Saric, M. (eds.) 2019 International Conference on Software, Telecommunications and Computer Networks, SoftCOM 2019, Split, Croatia, September 19-21, 2019. pp. 1-5. IEEE (2019), https://doi.org/10.23919/SOFTCOM.2019.8903868
Wang, G., Koshy, J., Subramanian, S., Paramasivam, K., Zadeh, M., Narkhede, N., Rao, J., Kreps, J., Stein, J.: Building a replicated logging system with apache kafka. Proc. VLDB Endow. 8(12), 1654-1655 (2015), http://www.vldb.org/pvldb/vol8/p1654-wang.pdf
Wang, H., Zhu, H., Xiao, L., Fei, Y.: Formalization and verification of the openflow bundle mechanism using CSP. Int. J. Softw. Eng. Knowl. Eng. 28(11-12), 1657-1677 (2018), https: //doi.org/10.1142/S0218194018400223
Wu, H.: Research proposal: Reliability evaluation of the apache kafka streaming system. In: Wolter, K., Schieferdecker, I., Gallina, B., Cukier, M., Natella, R., Ivaki, N.R., Laranjeiro, N. (eds.) IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops 2019, Berlin, Germany, October 27-30, 2019. pp. 112-113. IEEE (2019), https: //doi.org/10.1109/ISSREW.2019.00055
Wu, H., Shang, Z.,Wolter, K.: Performance prediction for the apache kafka messaging system. In: Xiao, Z., Yang, L.T., Balaji, P., Li, T., Li, K., Zomaya, A.Y. (eds.) 21st IEEE International Conference on High Performance Computing and Communications; 17th IEEE International Conference on Smart City; 5th IEEE International Conference on Data Science and Systems, HPCC/SmartCity/DSS 2019, Zhangjiajie, China, August 10-12, 2019. pp. 154-161. IEEE (2019), https://doi.org/10.1109/HPCC/SmartCity/DSS.2019.00036
Wu, H., Shang, Z.,Wolter, K.: TRAK: A testing tool for studying the reliability of data delivery in apache kafka. In: Wolter, K., Schieferdecker, I., Gallina, B., Cukier, M., Natella, R., Ivaki, N.R., Laranjeiro, N. (eds.) IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops 2019, Berlin, Germany, October 27-30, 2019. pp. 394-397. IEEE (2019), https://doi.org/10.1109/ISSREW.2019.00101