Research Article

Static program analysis for IoT risk mitigation in space-air-ground integrated networks

¹ Beijing Institute of Technology, Beijing, 100081, China
² China Academy of Information and Communications Technology, Beijing, 100191, China
³ Key Laboratory of Mobile Application Innovation and Governance Technology, Beijing, 100191, China
⁴ China University of Political Science and Law, Beijing, 100088, China

^* Corresponding author (email: chuanz@bit.edu.cn (Chuan Zhang); wuhuishu0122@gmail.com (Huishu Wu))

Received: 30 March 2024
Revised: 28 April 2024
Accepted: 29 April 2024

Abstract

The space-air-ground integrated networks (SAGINs) are pivotal for modern communication and surveillance, with a growing number of connected devices. The proliferation of IoT devices within these networks introduces new risks due to potential erroneous synergistic interactions that could compromise system integrity and security. This paper addresses the challenges in coordination, synchronization, and security within SAGINs by introducing a novel static program analysis (SPA) technique using zero-knowledge (ZK) proofs. This approach ensures the detection of risky interactions without compromising sensitive source code, thus safeguarding intellectual property and privacy. The proposed method overcomes the incompatibility between SPA and ZK systems by developing an imperative programming language for SAGINs and a specialized abstract domain for interaction threats. The system translates network control algorithms into arithmetic circuits suitable for ZK analysis, maintaining high accuracy in detecting risks. Evaluations of real-world scenarios demonstrate the system’s efficacy in identifying risky interactions with minimal computational overhead. This research presents the first ZK-based SPA scheme for SAGINs, enhancing security and confidentiality in network analysis while adhering to privacy regulations.