CPS: Small: Collaborative Research: Towards Secure, Privacy-Preserving, Verifiable Cyberphysical Systems

Abstract: Cyber-physical and Internet-of-Things (CPS/IoT) systems offer dramatic potential for revolutionizing many aspects of modern life by facilitating collection, analysis, and action on fine-grained sensor data. In both consumer-facing systems (e.g. smart locks, cameras, and thermostats) as well as infrastructure and industrial settings (e.g. devices to monitor factories or electricity distribution systems), CPS/IoT systems are already responsible for a wide range of safety-critical functions with significant security implications. CPS/IoT systems' correctness and security shortcomings have implications both for device users themselves, and more broadly across the Internet, due to malware attacks hosted by these devices. This project attacks the problem of verifying the correctness and security of CPS/IoT systems by developing design-time verification techniques to be used prior to deployment, as well as run-time verification techniques for systems in use. The project includes components to engage undergraduate students in research, and to improve the diversity of the computing workforce. The proposed research has two main thrusts. The first develops efficient, formal verification techniques for CPS/IoT Systems. These can be employed statically at design time or compile-time to comprehensively assess that state updates will occur in correct orderings based on design specifications provided by the designer or gleaned automatically from hardware design languages and software. The second explores hardware support for formal, dynamic IoT system verification. In particular, so-called ``lifeguard'' techniques can be employed to watch state updates in real-time and react to them with hardware or software error handlers as needed. This allows systems to maintain oversight over arbitrary CPS/IoT applications and help ensure their appropriate operation. A set of CPS/IoT verification tools to support design-time and compile-time verification and all hardware support designs and techniques developed will be released for broad open-source use.