Securing future SDN implementations over 5G/NR requires reasoning about network deployments at very large scale. Systems & Technology Research (STR) proposes DATAMASON: an automated SDN analysis system that will identify vulnerabilities and verify the correctness of SDN deployments. STRs key DATAMASON innovation is to solve the problem of automated formal verification of 5G/NR SDN network configurations by preprocessing requirements on the data plane into a condensed, quick-to-verify, set of constraints on the control program, thus enabling rapid development and deployment of verified control programs even when the data plane is large. In addition to data plane requirements for the flow of packets between switches and routers, DATAMASON will enable the specification of cybersecurity requirements, such as confidentiality and integrity, to be specified over a high-level model of entities and information flow which is automatically derived from an annotated low-level model of the network topology. We have recently demonstrated that such high-level information flow models are suitable for encoding cybersecurity requirements as part of STRs work on the DARPA Configuration Security (ConSec) program. For preprocessing the data plane requirements, DATAMASON will use a domain-constrained model-checking approach. The output of the SDN-specific model checking algorithm will provide inputs to a counter example guided inductive synthesis (CEGIS) procedure, in which data plane configurations that violate the requirements will be transformed into constraints on SDN control programs. For example, constraints generated from an information flow requirement to prevent communication from low-integrity systems to high-integrity systems may result in a constraint that every path from low- to high-integrity systems include a switch that drops packets from and to the corresponding hosts. This workflow will guarantee that a control program that satisfies the derived constraints produces configurations which satisfy all modeled requirements in the data plane. DATAMASON will use the constraints derived from the preprocessing step to quickly verify SDN control programs. DATAMASON will achieve this by using a structured language to effectively represent network control programs in terms of finite-state machines (FSMs), treating the derived constraints from the data plane as safety invariants on those FSMs, and verifying the properties via model-checking. Furthermore, standard techniques such as decomposition of independent portions of the control program as well as separation of instantiations of the same FSMs acting on different group of packets, will facilitate scaling to realistic 5G SDNs. Such an approach will allow network operators to verify the dynamic behavior of the controller prior to SDN load and runtime by performing verification during the deployment process.
Benefit: STR anticipates that the outcome of this Phase I SBIR program and a presumptive Phase II follow-on effort may be incorporated within operational SDN systems in the Navy and other services. The capability provided by DATAMASON (once it reaches maturity) will be useful to DoD and IC organizations with a need for formal verification of their network systems. Likely customers include all branches of the military and members of the IC. STR has consistently demonstrated success in technology transition. During its ten-year history, STR has executed 66 Phase I SBIR projects as a prime or subcontractor, from which 40 Phase II contracts have been awarded to STR (62% success rate). We have already received non-SBIR funding augmentation or made product sales for 19 of those efforts and are negotiating transition funding for several more. STRs SBIR- funded technology has attracted $7.5M in additional technology investment outside of the SBIR program, with an additional $9.3M in transition funding. STRs commercialization track record includes delivering enterprise level software solutions for a Fortune 500 company. STR was founded in 2010 and has grown from a five-person company to over 425 employees. Our mission is to be the premier provider of innovative cyber security, sensors, information processing and data analytics tools to address national security challenges. To fulfill our mission, we seek to transition and commercialize technology developed through the DoD SBIR and STTR programs, as well as other programs and funding sources. We strongly believe that SBIR/STTRs are a springboard in our business development strategy and not a business objective in itself. STR is a young company, but its founders and employees have significant experience throughout their careers in transitioning DoD research into DoD applications, and the company explores avenues to commercialize its technology for non-DoD applications. We understand how SBIR/STTR technology can play a critical role in moving ideas from academia to operational use and commercial sales. Our track record in the SBIR/STTR program reflects that commitment and insight.
Keywords: verification, verification, Model checking, Formal methods, software defined networks
