RINGS: Accelerating the NextG Protocols Definition to Code Generation with an Automatic and Secure Verification-Compilation Tool-Chain

network infrastructure such as the 5G have become more complicated, and their developments will take larger effort and longer time. In order to reduce the dependence of cellular infrastructure on foreign providers, and thus to improve the security of national information framework, it is necessary to facilitate the rapid development of open-source and secure software for new generations of cellular networks such as the 5G. A big challenge in these efforts is how to quickly generate secure open-source code according to the changing NextG protocol standards. The goal of this proposal is to develop an automatic, secure, and scalable tool-chain to accelerate the translation of NextG protocol documents into executable code. The project leverages technical advancements in formal language for protocol extraction and intermediate representation generation, formal verification for security analysis, and program synthesis for code generation. These three components will be tightly integrated to explore a radical and game-changing approach to the protocol software synthesis. The output of the research will be a sequence of tools that can directly read in the NextG standard documents, produce I/O Automata representation of the protocols, and finally generate secure open-source code. Formal security analysis will also be conducted on the I/O Automata representation to identify and remove vulnerabilities.