Collaborative Research: FMitF: Track I: A Formal Verification and Implementation Stack for Programmable Logic Controllers

对安全至关重要的工业控制系统，如电网或水处理厂，为现代社会提供至关重要的服务。因此，从设计到操作，它们必须在任何时候和所有层面上都是安全的。这尤其具有挑战性，因为工业控制软件在很大程度上是自动化的，可以代表人类做出决策，同时越来越多地成为对抗性网络物理攻击的目标。为了在不安全或不期望的情况发生之前提前采取行动，描述系统物理和潜在安全攻击影响的模型需要成为设计工业控制系统的中心元素。该项目的新颖之处在于基于数学和逻辑的软件开发方法，使工业控制软件意识到现实世界的影响和威胁。该项目的影响是为开发可靠和有弹性的工业控制系统的从业者提供更好的支持，旨在提供工业控制软件开发和执行之间缺失的关键验证链接。该项目的技术方法研究了可编程逻辑控制（PLC）工业控制系统的可证明正确的开发堆栈，预计将提供从高级模型一直到运行代码的完整验证链接链，并附有综合正确性证明。通过验证方法，在运行时分析模型与现实是否一致，并在出现偏差时进行抵消，正确性证明为实际工业控制系统的实施提供了强有力的安全保证。为了达到这个目的，研究人员团队期望改进技术来验证运行时对操作环境的监控，以及验证代码和模型之间的双向转换。该模型结合微分方程与不确定性控制和环境模型来描述物理效应和安全威胁。这样的预测模型、安全证明和验证方法是每个可信实现堆栈的关键元素，以便模型中的证明转移到正在运行的系统中。为了解决工业控制系统规模的设计安全问题，研究人员将网络物理系统的基础和实际验证方面的互补专业知识与工业控制系统安全和安全的嵌入式系统领域的专业知识结合在一起。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Safety-critical industrial control systems, such as the electric power grid or water-treatment plants, provide crucial services in modern societies. Therefore, they must be safe at all times and on all levels, from their design to their operation. This is especially challenging since industrial control software is largely automated to make decisions on behalf of humans while being increasingly targeted by adversarial cyber-physical attacks. In order to act in advance before unsafe or undesired situations occur, models that describe the physics of the system and the effects of potential security attacks need to become a central element in designing industrial control systems. The project's novelties are mathematics- and logic-based software-development methods to make industrial control software aware of real-world effects and threats. The project's impacts are improved support for practitioners in developing trustworthy and resilient industrial control systems, with the aim of providing the crucial missing verification link between industrial control software development and execution.The project's technical approach studies a provably correct development stack for industrial control systems with Programmable Logic Control (PLC) that is expected to provide a chain of fully verified links from high-level models all the way down to the running code, accompanied by synthesized correctness proofs. The correctness proofs entail strong safety guarantees on the actual industrial control system implementation through validation methods to analyze, at runtime, whether models and reality agree and to counteract when deviations occur. To this end, the team of researchers expects to advance techniques for verified runtime monitoring of the operating context and for verified bi-directional translation between code and models. The models combine differential equations with nondeterministic control and environment models to describe physical effects and security threats. Such predictive models, safety proofs, and validation methods are crucial elements of every trustworthy implementation stack so that proofs from models transfer to the running system. To address design safety at the scale of industrial control systems, the investigators bring together complementary expertise in foundations and practical verification for cyber-physical systems, with field expertise in embedded systems for industrial control systems safety and security.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.