SBIR-STTR Award

In the 5STARS project we aim to develop tools for automatically verifying the security and reliability of software-defined networking (SDN) applications in both commercial and DoD 5G settings. Throughout the project we will implement a prototype verification tool, demonstrate its effective use in 5G settings, integrate its capabilities with existing 5G software ecosystems, and initiate its transition to industry and the DoD. To carry out this work, we leverage our expertise developing SDN verification tools, our access to and experience with 5G testbeds, and our track record in successfully transitioning research prototypes to industry. Our project will provide unique capabilities for developing and maintaining high assurance 5G networks. Software-defined networking has been used to define core components within 5G platforms, as well as for auxiliary capabilities on top of any instantiated 5G platform. When applied to SDN core implementations, automated verification will ensure that SDN logic adheres strictly to specifications for 5G architectures and prevents costly security defects within the inner-most layer of 5G infrastructure. When applied to auxiliary SDN applications, automated verification will ensure that a number of functionality-enabling and security-enabling technologies are free from both unintended deficiencies and unknown security exploits due to programmer error.

Benefit:
If successful, the results of this project have the potential to significantly improve the security of 5G network infrastructure, as used in DoD and commercial settings. Network infrastructure is doubling in complexity year-after-year, and with complexity comes failures and financial liability. Verification is the only technique which fully mitigates complexity-related-risk in software systems, as opposed to ad-hoc bug-finding approaches that do not scale with system complexity. Certain organizations may be hesitant to use SDN technology due to the dynamism, complexity and cost it introduces within an otherwise critical digital infrastructure. Our results will demonstrate both the value and the viability of SDN when deployed with verification capabilities, and offer a catalyst for building more powerful and secure data networks than is possible with current industry practice. These verification results can then be used to address the certification and accreditation controls that more classical network setups address through inflexible configuration. Building on advances in academia in tools like Header Space Analysis (HSA), Anteater, Veriflow, and others, startup companies like Forward Networks, Veriflow Systems (recently acquired by VMware), and Intentionet have started to offer commercial products based on these tools. Large companies like Amazon, Cisco, and Microsoft have also made investments in network verification. Extrapolating from other domains, the potential market opportunity is clear: just as a $10B+ tools (i.e., EDA) industry supports the $300B hardware chip industry, a similar market for network verification tools seems likely to emerge. Our commercialization and DoD transition plan for 5STARS pursues two paths as part of our broader commercialization strategy: incubation and launch of a spin-off company offering a high assurance SDN platform for 5G and general commercial use; and direct licensing of SDN automated verification to networking hardware and software vendors. Our strategy is grounded on the principle of affordable loss: we pursue commercial ventures in a manner that limits risk while knowing precisely what we can afford to lose at each step. This enables us to make rapid, bold decisions that are grounded in real market assessments. In practice, this means we fund and incubate commercial ventures inside Galois with flexible business models that evolve in response to realized market demand. For the DoD, 5STARS will deliver demonstrable capabilities for US Navy applications directly transferable to DoD embedded systems, autonomous vehicles and space systems. DoD transition will be in parallel with our broader commercialization strategy.

Keywords:
Information Security, Information Security, Software Analysis, Formal Verification, Automated Verification, Software defined networking, 5G, Network Security, Critical Infrastructure

5G mobile networks are poised to dramatically enhance communication capabilities for DoD missions, such as those that require high mobility, and/or seamless connectivity between Navy vessels and UAV/USV/UUV/UGVs, each with rapidly changing positions. The network slicing enhancements of 5G will enable increasingly sophisticated network tunneling scenarios, such as allowing a battlefield partner (of varying degrees of trustworthiness) to securely tunnel through Navy networks (and vice versa). Additionally, 5G networks provide streamlined deployment and maintenance of classic network security packages like DDoS protection, botnet defense, moving target defense, and re-provisioning of network resources in resource-constrained environments. In the 5G SDN Tools for Automated and Reliable Security (5STARS) project we focus on securing data/user plane within the 5G Mobile Core and slice isolation case studies. We are developing a network verification tool that is (1) fully automated and therefore easy to use by network technicians with minimal additional training, (2) scalable and therefore applicable to complex network topologies and network applications, (3) general and therefore applicable to a wide range of both industry and government use case scenarios, and (4) high assurance and therefore capable of verifying the absence of bugs (within a restricted class) with a 100% certainty guarantee.

Benefit:
As both the Navy enterprise and ship-board systems increase in complexity and connectedness, the security of configurable networks, which are required to support modern and future mission objectives, becomes paramount and increasingly difficult to assure. These systems must change dynamically to adapt to conditions in the field and respond to threats in real-time. However, the increased agility opens doors to human error and adversaries alike to compromise security. The 5STARS verifier serves as a key component in assuring network security and information integrity in real time, protecting Navy assets. 5STARS will have direct relevance to the US Navy's network operators and potentially support US Fleet Cyber Command (10th Fleet). Where the US Navy operates emerging, trusted 5G networks for shipboard applications, 5STARS will be a foundational technology for Multi-Level Security (MLS) on shipboard networks. Specifically, 5STARS will provide the US Navy with mathematical guarantees of network slice isolation to enable data at multiple classifications to be transmitted securely to and from assets and for distribution within the shipboard network. For OCONUS untrusted networks in contested environments, the 5STARS static analysis and verification capability will provide US Navy Network Operators precise indication of network changes and or modifications that may indicate adversarial effects. As models of untrusted networks are refined, 5STARS will deliver guarantees of network reachability and slice isolation for specific mission use. While network configurations must change in real time in response to evolving real-world conditions, the policies that form the basis of information assurance do not evolve quickly. Those policies will be developed and vetted by experts within the Navy and updated infrequently. These policies can be deployed either by being pushed to the edges of the Navy network whenever they are updated, or asynchronously (e.g., when ships return to port). As the network structure evolves in the field, the evolutions of the network configuration will be verified for safety (as determined by the shared policy) in real time in the field. This field use provides fast feedback, and does not require sailors in the field to have in-depth knowledge of network security. We will work with our partner, Sierra Nevada Corporation, to provide Subject Matter Expertise in both deployment and operational effectiveness of 5STARS. In our early discussions, we have outlined a crawl, walk, run approach for deployment and testing initially in trusted, controlled network settings. When key fundamental capabilities and measures of effectiveness are verified, our plan is to simulate untrusted, gray networks in tactical settings for experiments in simulation. Our transition plan involves a hand off of 5STARS to US Navy and DIB SMEs to deploy and operate 5STARS verified 5G Networks.

Keywords:
Formal Verification, High Assurance, Formal methods, Critical Infrastructure, 5G, Software defined networking, cybersecurity, Network Security