SAT-Based Synthesis of Spoofing Attacks in Cyber-Physical Control Systems

We propose an approach to either certify that a given control system is safe under possible cyber-attacks on the measured data used for feedback and/or the commanded control signals, or alternatively synthesise a particular spoofing attack that corrupts the signals to make the closed-loop system unsafe. We assume that a (possibly nonlinear) dynamical model of the physical plant is available along with the control law, but that no on-line diagnosis is in place to detect attacks. After converting the model to a piecewise polynomial discrete-time form, we interpret the synthesis of the spoofing attack as a software verification query by means of an encoding into a Boolean satisfiability problem. Using a prototype implementation of our verification engine, we demonstrate its effectiveness on a case study of cyberattack to a chemical reactor.