SaTC 2.0: RES: Guaranteed Execution of Critical Code

Modern Cyber-Physical Systems (CPS) as well as Embedded and Internet-of-Things (IoT) devices perform a wide range of sensing and actuation functions. Their compromise can violate privacy, security, and even physical safety and health. Commonplace devices, such as smart thermostats, infusion pumps, smoke alarms, emergency lighting systems, meters, automated sprinklers, water sensors, and mainline shutoff valves have all been targets of sophisticated attacks. These increasingly (inter-)connected devices often perform essential services and, ideally, their critical functionality must be preserved even in the presence of (potentially large-scale) compromise. Given the complexity and rapid evolution of IoT/CPS/Embedded software and firmware, complete compromise prevention is optimal, yet unattainable. Instead of prevention, this project follows a fundamentally different strategy: guaranteed execution of critical functionality, even when a device is compromised. The project’s key novelty is to ensure that IoT/CPS devices always remain capable of performing a minimal set of critical tasks even if compromised. Such tasks may include sensing the need for, and administering, insulin for diabetic patients, detecting smoke or CO and sounding alarms, or reporting abnormally high temperatures. The project's broader significance and importance is improved reliability of critical code in IoT/CPS/Embedded devices. The project aims to archive these goals via a novel primitive: Guaranteed Execution Environment (GEE). A GEE is realized using a combination of hardware and firmware, which guarantees the execution of a safety-critical program, called a safelet, based on exact requirements specified at the time of its deployment within a GEE. The project has four thrusts. The first defines an execution model for safelets and provides a formal verification of the safety monitor charged with executing them. The second thrust provides GEE hardware support, either using existing hardware components or new primitives to be developed specifically for GEEs. The third thrust focuses on software support for safelets and provides tools for developers to reason about safelets’ resource requirements. The final thrust involves prototyping of, and experimenting with concrete safelet use-cases (drawn from distinct application domains) in order to demonstrate practicality and benefits of GEEs. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.