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

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

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.