Formal Verification and Security Analysis of Go-based New Simple Queue System

Zhiru Hou, Danyang Wang, Jiaqi Yin, Sini Chen, Huibiao Zhu

科研成果: 期刊稿件文章同行评审

摘要

New Simple Queue (NSQ) is a distributed messaging platform developed in Golang that can handle billions of daily messages. Its distributed architecture ensures high fault tolerance and availability. Given NSQ’s widespread application across various fields, it is crucial to focus on the system’s robustness and data transmission security. Therefore, a rigorous mathematical logic analysis of NSQ’s messaging mechanism is essential for verifying its reliability. This paper formalizes NSQ’s core components using Communicating Sequential Processes (CSP), resulting in a comprehensive formal model of the system. Furthermore, this paper utilizes the Process Analysis Toolkit (PAT) for practical implementation of the model, verifying five critical properties of the NSQ system. And the verification results demonstrate that the NSQ system successfully satisfies these essential properties, highlighting its flexibility, robustness and efficient messaging service capabilities. Moreover, this paper focuses on formalizing and verifying the security mechanisms in NSQ’s data transmission. By integrating the Transport Layer Security (TLS) protocol into the NSQ system and employing a man-in-the-middle model to simulate deception and interception attacks, it is demonstrated that the TLS protocol enhances the security of NSQ data transmission. This paper also proposes upgrading from one-way to two-way certificate authentication to further enhance TLS data security. Experimental results reveal that despite significant security improvements with the TLS protocol, producer and consumer processes remain vulnerable to spoofing attacks under specific insecure network conditions, leading to potential data leaks. Therefore, the TLS protocol can significantly improve the data security of the NSQ system.

源语言英语
文章编号2550145
期刊Journal of Circuits, Systems and Computers
34
6
DOI
出版状态已出版 - 1 4月 2025

指纹

探究 'Formal Verification and Security Analysis of Go-based New Simple Queue System' 的科研主题。它们共同构成独一无二的指纹。

引用此