Automated Formal Verification of Software Defined Network Implementations

Navy SBIR 21.1 - Topic N211-083
ONR - Office of Naval Research - Ms. Lore-Anne Ponirakis - loreanne.ponirakis@navy.mil
Opens: January 14, 2021 - Closes: February 18, 2021 (12:00pm EDT)

N211-083 TITLE: Automated Formal Verification of Software Defined Network Implementations

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:

  1. 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
  2. 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
  3. 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
  4. 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
  5. 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

KEYWORDS: Software Defined Network; SDN; Automated Tools; Formal Methods; Formal Verification; 5G

** TOPIC NOTICE **

The Navy Topic above is an "unofficial" copy from the overall DoD 21.1 SBIR BAA. Please see the official DoD Topic website at rt.cto.mil/rtl-small-business-resources/sbir-sttr/ for any updates.

The DoD issued its 21.1 SBIR BAA pre-release on December 8, 2020, which opens to receive proposals on January 14, 2021, and closes February 18, 2021 at 12:00 p.m. ET.

Direct Contact with Topic Authors: During the pre-release period (Dec 8, 2020 to January 13, 2021) proposing firms have an opportunity to directly contact the Technical Point of Contact (TPOC) to ask technical questions about the specific BAA topic. Once DoD begins accepting proposals on January 14, 2021 no further direct contact between proposers and topic authors is allowed unless the Topic Author is responding to a question submitted during the Pre-release period.

SITIS Q&A System: After the pre-release period, proposers may submit written questions through SITIS (SBIR/STTR Interactive Topic Information System) at www.dodsbirsttr.mil/topics-app/, login and follow instructions. In SITIS, the questioner and respondent remain anonymous but all questions and answers are posted for general viewing. Topic Q&A will close to new questions on February 4, 2021 at 12:00 p.m. ET

Note: Questions should be limited to specific information related to improving the understanding of a particular topicís requirements. Proposing firms may not ask for advice or guidance on solution approach and you may not submit additional material to the topic author. If information provided during an exchange with the topic author is deemed necessary for proposal preparation, that information will be made available to all parties through SITIS. After the pre-release period, questions must be asked through the SITIS on-line system.

Topics Search Engine: Visit the DoD Topic Search Tool at www.dodsbirsttr.mil/topics-app/ to find topics by keyword across all DoD Components participating in this BAA.

Help: If you have general questions about DoD SBIR program, please contact the DoD SBIR Help Desk at 703-214-1333 or via email at DoDSBIRSupport@reisystems.com

[ Return ]