Phase II Amount
$2,999,388
The proposed Verified Intra-SoC Networking (VISN) program will use the BedRock Systems (BS) Formal Methods (FM) capabilities and Riverside Research (RR) side channel analytic insights to expand and extend the capabilities of the Trusted Integration Framework (TIF) to address the objectives and requirements of the HASH SBIR Request for Proposal. BR along with RR have identified a series of innovative concepts that will increase the abilities of mission systems to Prevent, Mitigate, or Recover from cyber-vulnerabilities by tying together the hardware security and software domains. VISN encompasses four key areas to provide provability and traceability of software, hardware, and programmable logic regarding innovative approaches to FM that in addition to proof of correctness, enhance Confidentiality, Integrity, and Availability (CIA) in the face of nation state hardware reverse engineering. Concurrent System Verification: VISN uses BRs BRiCK concurrent C++ separation logic to scale system verification to SMP and AMP hardware. Open Standards for Verified Interoperability: VISN will leverage and verify open standards to allow both legacy and future aircraft to reuse secure software and hardware co-designed components securely. C++ Verification at Scale: Utilizing the BR automation and verification environment, VISN supports assisted verification of deep properties of complex concurrent programs such as hypervisors and device drivers. Scalable Software and Hardware Security Modules. VISN will leverage RR reusable Universal Composability models to capture side channel attacks that will reduce cost in system security design and secure existing and embedded crypto systems for Anti-Tamper Anticipated Results Identification and implementation of new techniques that can be implemented in FM proven software that mitigate or reduce side channel vulnerabilities in mission critical systems. Enhanced proof the TIF provides sufficient isolation between VMs and processes to achieve Confidentiality and Integrity ratings of at least Medium, without impacting Availability necessary for Real Time Operating Systems. Demonstration of an integrated system that is capable of successfully completing Certification & Accreditation at a TRL-6/7 level. Enhanced Universal Composability Model. The TIF element of the program will benefit from a variety of perspectives; additional functionality and useability of the Open Source elements, insights and mitigations to side-channel attack vectors, demonstrations on avionics hardware, and positioning for Certification and Accreditation activities in the Phase II Option. A Formally Verified TIF that supports current, isolated virtualization, is designed for dual use (military and commercial), and enables future proofing against unknown cyber threats is in line with the mission of DARPA as well as the intent of the HASH program. BS along with our teammate RR highly recommend proceeding with the proposed program.
