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

网络物理和物联网（CPS/IoT）系统通过促进对细粒度传感器数据的收集、分析和操作，为现代生活的许多方面带来了巨大的变革潜力。 在面向消费者的系统（例如智能锁、摄像头和恒温器）以及基础设施和工业环境（例如监控工厂或配电系统的设备）中，CPS/物联网系统已经负责广泛的安全关键功能，具有重大的安全意义。CPS/IoT系统的正确性和安全性缺陷对设备用户本身以及更广泛的互联网都有影响，因为这些设备托管的恶意软件攻击。该项目通过开发部署前使用的设计时验证技术以及使用中系统的运行时验证技术来解决验证CPS/IoT系统的正确性和安全性的问题。 该项目包括让本科生参与研究的组成部分，并提高计算劳动力的多样性。 第一个是为CPS/IoT系统开发有效的正式验证技术。这些可以在设计时或编译时静态地采用，以基于设计者提供的设计规范或从硬件设计语言和软件自动收集的设计规范来全面评估状态更新将以正确的顺序发生。 第二部分探讨了对正式、动态物联网系统验证的硬件支持。特别是，可以采用所谓的“救生员”技术来实时监视状态更新，并根据需要使用硬件或软件错误处理程序对其做出反应。这使得系统能够对任意CPS/IoT应用程序进行监督，并帮助确保其正常运行。 一套CPS/物联网验证工具，以支持设计时和编译时验证，以及所有硬件支持设计和开发的技术将被发布用于广泛的开源使用。

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.