Distributed Just-ahead-of-Time Verification of Cyber-Physical Critical Infrastructures

funded by the National Science Foundation

researchers: Saman A. Zonouz (Rutgers), Kate Davis, Peter W. Sauer

Secure operation of next-generation cyber-physical systems, specifically power grid infrastructures, will require effective, scalable formal verification and predictive situational awareness capabilities. Precise comprehension of a system’s security status and potential upcoming threats will enable operators to prepare against adversarial activities. Current static formal verification methods analyze system models offline, often facing state-space explosion, and hence do not scale up to large-scale cyber-physical infrastructures. On the other hand, existing dynamic monitoring and situational awareness solutions notify operators about incidents that have just occurred or are about to occur, and hence do not leave enough of a time buffer for effective manual or automated response and recovery.

This project is developing a holistic cyber-physical security approach that will result in a system called Cyber-Physical Verifier (CPV), which will be able to model, analyze, predict, and learn how to respond to complex security and safety incidents in cyber-physical infrastructures. Using a hybrid static/dynamic approach, called Just-ahead-of-Time (JAT) verification, CPV will stay ahead of the actual system state by an arbitrary time buffer through efficient analysis and formal safety verification of future potentially upcoming states given the current estimated system state. Consideration of limited future horizons will enable CPV to address state-space explosion while leaving operators enough time to react if an unsafe state is realized. CPV will also be capable of learning about selected tolerance strategies so that it can react automatically upon realization of previously seen similar unsafe states.

The result will be the first mathematically rigorous and practically scalable formal verification solution for cyber-physical systems that models, analyzes, and predicts complex security incidents in real time. The CPV framework will be validated using a real-world power grid testbed infrastructure.