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

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.