Formal Methods for an Industrial Control System

Abstract:

Over the last year, the Johns Hopkins Applied Physics Laboratory has been pursuing research in verification of cyber-physical industrial control systems. We have successfully applied the hybrid systems theorem prover KeyMaera-X to the analysis of a model of a shipboard chilled water system. The physics of this model is governed by a system of ordinary differential equations that are more complex than those used in previous KeyMaera-X proofs. With assistance from the KeyMaera-X team at Carnegie Mellon University, we were able to demonstrate a safety property that a load in the system would not overheat under a reasonable set of assumptions. Our model included a simple control logic and a set of realistic differential equations that describe the cooling of a load in the presence of chilled water. Following the completion of these proofs, we demonstrated the sharpness of the bounds in the safety property using dReach, a bounded reachability analysis tool for hybrid systems. This work shows a promising approach for formal analysis of real-world cyber-physical industrial control systems, and we are working to expand this work to other problems in this domain.

--

The authors are researchers at the Johns Hopkins Applied Physics Laboratory (JHU/APL) in the Software Assurance Research & Applications (SARA) Lab.

Ian Blumenfeld received his MA in mathematics from the University of Pennsylvania. He is interested in using formal reasoning in a variety of critical domains. His previous work has used formal methods tools in areas from malware analysis to cryptography. Prior to joining APL, Ian worked at CyberPoint, Galois, and in the High Confidence Software and Systems Group at NSA.

Yanni Kouskoulas received his Ph.D. in Electrical Engineering from the University of Michigan, Ann Arbor. His research interests are focused on the analysis and development of rigorous formal guarantees about the properties of cyber-physical system algorithms and software. He has helped to analyze the safety of different components of surgical robots, as well as the FAA's next generation air-traffic collision avoidance system.

Durward McDonell received his Ph.D. in mathematics from the University of Minnesota. His primary interests lie in the areas of formal methods and quantum computing.

Mark Thober received his Ph.D. in Computer Science from the Johns Hopkins University. His interests include automated code analysis, programming language-based security, type theory, and malware analysis.