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.