Compositional Verification of Trusted Execution Environments and I/O kernels
Abstract
A major problem of Cyber-Physical Systems (CPS) is that their operating system services, which include the I/O channels that control physical devices, cannot be protected from penetrations in current operating systems. This makes critical CPS vulnerable to exploitation by adversaries. The goal of this research is to formally verify the isolation primitives that encapsulate operating system and application services for CPS and provide high-assurance isolated I/O channels for CPS device control. Despite availability of trusted execution environments (TEE) for isolated services, the formal verification of their composition with real CPS applications and I/O services has not been achieved to date. Furthermore, the formal verification of I/O channel separation has not been achieved for CPS devices. In this research we intend to develop a method and illustrate its use in the compositional verification of TEEs for high assurance I/O channel separation in CPS. The results of this research would enable deployment of CPS systems that are highly resilient to attacks; e.g.,malware insertion in commodity operating systems that are pervasively deployed in bot defenses and industrial applications.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Feb 07, 2019
- Source ID
- N629091912028
Entities
People
- Brent Byunghoon Kang
Organizations
- KAIST
- Office of Naval Research
- United States Navy