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

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

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.