Modular and Provably Secure High-Assurance Hardware and Software Co-design (MPS-HAHSC)

Current generation Cyber Physical Systems (CPS) including aviation systems were not developed with strong computer security requirements. Past cyber threats, Spectre, Meltdown, current cyber threats, and future cyber threats need to be countered. Embedded system designs are typically based on commodity hardware and software optimized exclusively for size, weight, and power – leading to critical cyber vulnerabilities that can have devastating effects on safety and mission effectiveness. This has also led to the unsustainable “Perimeter, Patch, Pray” Information Assurance strategy that is simply impractical for fielded aviation and missile weapons systems. This SBIR proposal focuses on strengthening Army high assurance system such as an Army Aviation or Missile subsystem currently under development or via technology refresh. We propose Modular and Provably Secure high-assurance hardware/software co-design (MPS-HAHSC) based on the open-source RISC-V instruction set architecture and high-assurance (formally proven) kernels such as seL4. We leverage our existing Modular Provably Security (MPS) mathematical reasoning framework (that encompasses both hardware and software layers) and software verification framework to harden the assurance of the formally verified seL4 kernel which by formally verifying seL4 Assembly language code blocks and boot-up firmware functionality that seL4 relies on but is not presently verified. Further, MPS-HAHSC adds support for multi-core execution and DMA capabilities without affecting the existing proofs. Finally, MPS-HAHSC also support executing legacy unverified kernels such as Linux along with the formally verified seL4 kernel all while preserving the formally verified properties of the entire system. MPS-HAHSC thus enables the vision of a Future Vertical Lift (FVL) system architecture that can support robust, mathematically proven end-to-end high-assurance while seamlessly co-existing with unverified components. With the advent of RISC-V this can also be done in a practical and performant manner with all the available tooling to support rich CPS mission applications. Our proposed approach squarely addresses the "Modernization" transformational strategic capabilities of the Army with an emphasis on “Capability Development for Future Vertical Lift and Air and Missile Defense” as identified by the Vision and Strategy for the Army of 2030. MPS-HAHSC provides mathematically backed ironclad cybersecurity properties that, by design, are immune to adversarial impacts and elevates the Army/DoD cybersecurity capabilities to an unprecedented level to protect against great power competitors who are challenging U.S. dominance in all warfighting domains.