Distributed Just-Ahead-Of-Time Verification of Cyber-Physical Critical Infrastructures

Abstract:

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 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. At the controller level, on a minimal trusted computing base, we will develop and use power systems data analysis techniques to obtain a better understanding and comparison of the physical impacts and potential safety violations of PLC code executions and issued control commands. Maintenance of high quality updated power system model information is crucial to the cyber-physical verification approach, as the quality directly affects its later cyber-physical verification analyses’ accuracy. We will concentrate on modeless approaches, as extensive model-based techniques are unlikely to be practical in real-world dynamic and adversarial PLC environments. We will develop new online data analysis techniques that consider cyber assets to validate and update power system models and assess the potential impact of adversarial PLC execution control flow on the physical components and their safety requirements.  Our goal will be to refine the estimated model into a simplified, and yet functional, mathematical power flow model to be used in subsequent verification analyses. We will investigate how these models and their abilities improve with additional data, particularly by considering information made available by communication with other sensor devices.