2021 Research Review / DAY 2
Towards Incremental and Compositionally Verifiable Security for CHIC-Centric Cyber Physical Systems
DoD cyber-physical Systems (CPS) employ commodity heterogeneous interconnected computing (CHIC) platforms and associated software stacks (e.g., ARM/Linux) to deliver capabilities at the speed of relevance [Osborn 2020; Krazit 2019; Keller 2019; Villarreal 2019]. However, the DoD faces a challenge achieving assurance in CHIC-centric CPS implementation security, because such systems employ multiple hardware platforms and multiple, large, layered software. What’s more, these systems are frequently produced by disparate developers. A recent U.S. Government Accountability Office (GAO) report highlights security issues in CHIC-centric CPS implementations [GAO 2018].
Our solution focuses on development-compatible, implementation-level, protected, and verifiable execution building blocks that retrofit with existing code, incrementally, at a fine granularity, with composability across multiple CHIC stack implementation layers.
In this project, we draw from our published broad vision and strategy [Vasudevan 2020]. We explore the viability of provable, cost-effective, and innocuous (applicable on existing software and preserve existing functionality, such as NASA innocuity) CHIC-centric CPS implementation security [Halloway 2019]. Our solution focuses on development-compatible, implementation-level, protected, and verifiable execution building blocks that retrofit with existing code, incrementally, at a fine granularity, with composability across multiple CHIC stack implementation layers. Our scope in this project is the design, implementation, and verification of a critical execution path for CPS: secure on-platform sensor access that protects the integrity of the existing CPS application and sensor hardware/driver with trusted control and the data path between them. There are three high-level pieces to our approach (see Figure 1):
- Interface confined implementation-level object abstractions (überobjects or üobjects): implementation-level building blocks that form fine-grained monitors around a system-level resource (e.g., data memory and I/O area) towards a security property
- Runtime protected set of üobjects (üobject collections): a set of üobjects within a given address space at runtime, bootstrapped by a platform root-of-trust entity that endows memory protection and secure call routings
- An implementation-level assume-guarantee reasoning framework that allow us to formally reason about interleaved executions of üobjects in the presence of unverified (and unavoidable) legacy components [Vasudevan 2016]
Among the planned outputs of this project is a demonstration of our approach on an off-the-shelf rover CPS platform with secure sensor access protection via üobjects that allows immunity against an entire class of memory integrity attacks. This will serve to showcase the viability of our approach to DoD and DoD industrial establishments. We will also make open source our associated prototype artifacts, code, and documentation (e.g., release via GitHub). This will enable DoD and DoD industrial establishments to start experimenting with üobjects within relevant application domains.
This FY2021 project
- aligns with the CMU SEI technical objective to bring capabilities that make new missions possible or improve the likelihood of success of existing ones
- aligns with the CMU SEI technical objective to Be Trustworthy in construction and implementation, and resilient in the face of operational uncertainties including known and yet unseen adversary capabilities
Mentioned in this Article
United States Government Accountability Office. Weapon Systems Cybersecurity: DoD Just Beginning to Grapple with Scale of Vulnerabilities. October 2018. https://www.gao.gov/assets/700/694913.pdf
Halloway, Michael C. Understanding the Overarching properties. NASA/TM–2019–220292. National Aeronautics and Space Administration. July 1, 2019. https://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20190029284.pdf
Keller, John. Navy chooses Open Architecture Shipboard computers and Self Defense Systems. Military Aerospace. January 16, 2019. https://www.militaryaerospace.com/computers/article/16722033/navy-chooses-openarchitecture-watercooled-shipboard-computers-from-gts-for-sewip-and-self-defense-systems
Krazit, Tom. How the US Airforce deployed Kubernetes and Istio on an F-16 in 45 days. The New Stack. Decmber 24, 2019. https://thenewstack.io/how-the-u-s-air-force-deployed-kubernetes-and-istio-on-an-f-16-in-45-days/
Osborn, Kris. New Air Force B-21 stealth bomber takes key technology step toward war readiness. Fox News. June 2, 2020 https://www.foxnews.com/tech/new-air-force-b-21-stealth-bomber-takes-key-technology-step-toward-war-readiness
Vasudevan, Amit ; Chaki, Sagar; Maniatis, Petros; Jia, Limin; & Datta, Anupam. überSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor. Pages 87-104. In proceedings of USENIX Security Symposium. Austin, Texas. August 2016.
Vasudevan, Amit; Maniatis, Petros; & Martins, Ruben. überSpark: Practical, Provable, End-to-End Guarantees on Commodity Heterogenous Interconnected Computing Platforms. ACM SIGOPS Operating Systems Review Journal – Special Issue on Formal Methods & Verification. Volume 54. Number 1. July 2020. Pages 8-22. https://doi.org/10.1145/3421473.3421476
Villarreal, Jennifer. GE Aviation and Auterion provide All-in-one hardware and software platform for commercial drones. GE Aviation. https://www.geaviation.com/press-release/systems/ge-aviation-and-auterion-team-provide-all-one-hardware-and-software-platform