Collaborative research: vines: track 1: veriran: securing AI-native o-ran applications via formal invariant verification

The National Science Foundation Division of Information and Intelligent Systems awarded Sri International $252,975 on August 1, 2026, under the Computer and Information Science and Engineering program (CFDA 47.070) to develop formal verification techniques for securing artificial intelligence-native Open Radio Access Network (O-RAN) applications.

The project, titled "VERIRAN: Securing AI-Native O-RAN Applications via Formal Invariant Verification," establishes a framework to automatically evaluate whether network control software applications comply with security, safety, and operational requirements before deployment. The work addresses the increasing reliance of modern wireless systems on programmable software that manages network operations, optimizes performance, and supports automated decision-making, where defects or malicious behavior can disrupt services or trigger widespread failures.

The effort is organized around three technical thrusts: translating O-RAN security and operational requirements into machine-checkable policies; automatically extracting behavioral models from application source code using static and data-flow analysis, including software containing artificial intelligence-based decision logic; and integrating inferred models with formal policy monitors to verify correctness, detect violations, generate counterexamples, and recommend repairs. The project aims to establish a rigorous and scalable approach for connecting high-level policy intent with low-level software behavior in operational wireless networks.

Performance takes place in Menlo Park, California, with a period of performance from August 1, 2026, through July 31, 2029.

Abstract

This collaborative project aims to improve the safety and reliability of future cellular networks. Modern wireless systems increasingly depend on programmable software applications that help manage network operations, optimize performance, reduce energy consumption, and support automated decision making. Because these applications can directly influence critical network functions, software defects or malicious behavior can disrupt services, expose sensitive information, or trigger widespread failures. The project develops a comprehensive framework that automatically evaluates whether such applications comply with important security, safety, and operational requirements before deployment. By providing automated checks for network control software, the project aims to strengthen trust in emerging open radio access network environments that support intelligent and highly adaptable wireless infrastructure. The intellectual merit of the project lies in advancing formal verification techniques for complex, event driven, distributed, and artificial intelligence enabled wireless systems. The work is organized around three technical thrusts: translating open radio access network security and operational requirements into machine checkable policies; automatically extracting behavioral models from application source code using static and data flow analysis, including software that contains artificial intelligence-based decision logic; and integrating inferred models with formal policy monitors to verify correctness, detect violations, generate counterexamples, and recommend repairs. These efforts will establish a rigorous and scalable approach for connecting high level policy intent with low level software behavior in operational wireless networks. The broader impact of the project is the development of more trustworthy, secure, and resilient wireless communication systems that support critical societal applications such as telemedicine, smart transportation, emergency response, and public safety communications. The project will deliver open source tools for evaluating third party open radio access network applications, a collection of benchmark case studies, and formally specified policy monitors informed by industry standards. These resources will assist researchers, software developers, network operators, and government stakeholders in improving the security and reliability of programmable network infrastructure. The project will also provide training opportunities for graduate and undergraduate students in cybersecurity, networking, artificial intelligence, and formal methods, while helping establish best practices for the safe integration of third-party software into next generation wireless systems. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the foundation's intellectual merit and broader impacts review criteria.- subawards are not planned for this award.