CPS: Synergy: Collaborative Research: Distributed Just-Ahead-Of-Time Verification of Cyber-Physical Critical Infrastructures

下一代复杂电网关键基础设施的可靠运行需要数学和实际的验证解决方案，以保证正确的基础设施功能。该项目为网络物理环境下可编程逻辑控制器(PLC)的形式化和可扩展控制器代码验证器的理论建模、综合和实际部署奠定了基础。PLC广泛应用于工业控制系统中的控制自动化。PLC通常连接到工程工作站，工程师在那里开发控制逻辑来处理来自传感器的输入值，并向执行器发出控制命令。该项目专注于保护基础设施免受针对PLC的恶意控制注入攻击，例如Stuxnet，这些攻击将恶意代码注入到设备上，以将底层物理平台驱动到不安全状态。这项提议的更广泛影响是非常显著的。它为覆盖能源和制造等行业的关键基础设施系统提供了实时安全的潜力。该项目的智力优势是通过集成离线正式方法、在线监控解决方案和电力系统分析，为网络物理系统提供一个数学和实用的验证框架。由于离线正式方法对所有可能的系统状态进行了详尽的安全分析，因此不适用于大型平台，而在线监控报告的结果往往为时已晚，无法采取预防措施。该项目采用混合方法，动态预测下一次可能发生的安全事件，并在遇到不安全状态之前向操作员报告，以便有时间做出反应。该项目的更广泛影响是为一般网络物理安全关键基础设施提供实用的数学分析能力，对我们的国家安全具有潜在的直接影响。研究成果被整合到研究生、本科生和K-12课堂的教育模块中。

Trustworthy operation of next-generation complex power grid critical infrastructures requires mathematical and practical verification solutions to guarantee the correct infrastructural functionalities. This project develops the foundations of theoretical modeling, synthesis and real-world deployment of a formal and scalable controller code verifier for programmable logic controllers (PLCs) in cyber-physical settings. PLCs are widely used for control automation in industrial control systems. A PLC is typically connected to an engineering workstation where engineers develop the control logic to process the input values from sensors and issue control commands to actuators. The project focuses on protecting infrastructures against malicious control injection attacks on PLCs, such as Stuxnet, that inject malicious code on the device to drive the underlying physical platform to an unsafe state. The broader impact of this proposal is highly significant. It offers potential for real-time security for critical infrastructure systems covering sectors such as energy and manufacturing.The project's intellectual merit is in providing a mathematical and practical verification framework for cyber-physical systems through integration of offline formal methods, online monitoring solutions, and power systems analysis. Offline formal methods do not scale for large-scale platforms due to their exhaustive safety analysis of all possible system states, while online monitoring often reports findings too late for preventative action. This project takes a hybrid approach that dynamically predicts the possible next security incidents and reports to operators before an unsafe state is encountered, allowing time for response. The broader impact of this project is in providing practical mathematical analysis capabilities for general cyber-physical safety-critical infrastructure with potential direct impact on our national security. The research outcomes are integrated into education modules for graduate, undergraduate, and K-12 classrooms.