RT&L FOCUS AREA(S): Cybersecurity; Autonomy TECHNOLOGY AREA(S): Battlespace Environments; Electronics; Information Systems The technology within this topic is restricted under the International Traffic in Arms Regulation (ITAR), 22 CFR Parts 120-130, which controls the export and import of defense-related material and services, including export of sensitive technical data, or the Export Administration Regulation (EAR), 15 CFR Parts 730-774, which controls dual use items. Offerors must disclose any proposed use of foreign nationals (FNs), their country(ies) of origin, the type of visa or work permit possessed, and the statement of work (SOW) tasks intended for accomplishment by the FN(s) in accordance with section 3.5 of the Announcement. Offerors are advised foreign nationals proposed to perform on this topic may be restricted due to the technical data under US Export Control Laws. OBJECTIVE: Develop an automated tool suite to formally verify correctness of software defined networks (SDNs), from programming to network implementations, subject to Fifth Generation (5G) New Radio (NR) standards and protocols. DESCRIPTION: Cybersecurity vulnerabilities commonly arise from flawed implementations. To minimize attack surfaces while harnessing the full power of Fifth Generation (5G) New Radio networks, innovative solutions that identify flaws and formally verify correctness of underlying SDNs are required. Furthermore, automation will relieve the burden on operators who often validate code empirically, and will facilitate rapid, secure reconfigurability of SDNs. This SBIR topic addresses the challenge of automating formal verification of code and network correctness, which has thus far limited such technology to Industrial Control System applications. The innovative solution sought is an automated tool suite that identifies SDN programming flaws or malicious content and employs formal techniques to prove correctness of network implementations. PHASE I: Define and develop a concept framework for an automated tool suite that will formally verify correctness of complete SDN implementations, ensuring compliance with any applicable NIST and ISO/IEC 27000 standards. Evaluate the type and source of vulnerabilities that could potentially be exploited as a result of faulty SDN implementations from programming flaws and malicious code to the actual network instantiation, considering both accidental and malicious events. Provide measures of effectiveness for such tools, as well as attainable performance characteristics. The framework will need to be flexible and extensible across a set of hardware systems, with a proposed design for the hardware and software architectures that will be incorporated into 5G-enabled cyber physical systems for assured cyber resilience. The design should include a summary of any computing and power requirements for administering these cybersecurity tools. The feasibility of the concept will be established through modeling and simulation. Include, in a Phase II plan, the initial design specifications and capabilities description to build prototype tools in Phase II. PHASE II: Fully develop, verify, and validate prototype automated tools that formally verify correctness of complete SDN implementations subject to applicable standards and protocols (e.g., 5G NR, NIST, and ISO/IEC 27000) for evaluation. Design the prototype tool suite to provide formal verification of code and network functionality prior to instantiation. Demonstrate the design performance through modeling and physical testing over a range of scenarios devised to test network vulnerabilities with and without the cyber resilient layer in place. Use evaluation criteria and results to refine the prototype tool suite into an initial design that can be deployed in relevant and/or operational environment settings, and that support mission requirements in the cyber domain, which ultimately ensures the confidentiality, integrity, and availability of data. Develop a Phase III plan to transition the technology to a system that can be acquired by the Navy. PHASE III DUAL USE APPLICATIONS: Support Navy system integration of the cybersecurity framework, hardware and software, employing any lessons learned from the Phase II evaluation. Incorporate the automated tool suite into security assessments that support both any existing and future SDN implementations. This integration will also include validation testing and demonstration on a representative 5G-networked system. The automated tool suite developed in this SBIR effort would support formal verification of correct SDN applications in 5G networks used by industry, infrastructure, energy, health care, and other applications where cyber attacks due to flawed implementation may be expected to interfere with the integrity or availability of data and analysis from 5G-enabled cyber physical systems. REFERENCES: Ball, T., Bj rner, N., Gember, A., Itzhaky, S. Karbyshev, A. et al. VeriCon: Towards Verifying Controller Programs in Software-Defined Networks. , Proc. 35th ACM SIGPLAN Intl. Conf. Programming Language Design (PLDI'14), 2014, pp.282-293. http://www.cs.technion.ac.il/~shachari/dl/pldi2014.pdf Canini, M., Venzano, D., Pereskini, P., Kostic, D. and Jennifer, R. A Nice Way to Test OpenFlow Applications. Proceedings of the 9th USENIX conference on Networked Systems Design and Implementation (NSDI'12), 2012. https://www2.cs.duke.edu/courses/fall14/compsci590.4/Papers/NICE12.pdf Darvas, D., Majzik, I., Blanco Vi uela, E. Formal verification of safety PLC based control software. E. brah m, M. Huisman (Eds.). Integrated Formal Methods, vol. 9681 (Lecture Notes in Computer Science), Springer, 2016. https://dl.acm.org/doi/10.1007/978-3-319-33693-0_32 Kim, H., Reich,J., Gupta, A., Shahbaz, M., and Feamster, N. et al. Kinetic: Verifiable Dynamic Network Control. Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation (NSDI'15), 2015. https://www.usenix.org/system/files/conference/nsdi15/nsdi15-paper-kim.pdf Schnepf, N., Badonnel, R., Lahmadi, A. and Merz, S. Automated Verification of Security Chains in Software-Defined Networks with Synaptic. NetSoft 2017 - IEEE Conference on Network Softwarization, Bologna, Italy, July 2017. https://ieeexplore.ieee.org/document/8004195
