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

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.