Formal Synthesis of Monitoring and Detection Systems for Secure CPS Implementations
This addresses security vulnerabilities in real-world CPS implementations, offering a formal solution to bridge the gap between theoretical guarantees and practical software, though it appears incremental by building on existing detection schemes.
The paper tackles the problem of securing cyber-physical system control loop implementations against Man-in-the-Middle attacks by proposing a formal synthesis method for attack detectors with varying thresholds, which prevents performance-degrading stealthy attacks and minimizes false alarms.
We consider the problem of securing a given control loop implementation of a cyber-physical system (CPS) in the presence of Man-in-the-Middle attacks on data exchange between plant and controller over a compromised network. To this end, there exist various detection schemes that provide mathematical guarantees against such attacks for the theoretical control model. However, such guarantees may not hold for the actual control software implementation. In this article, we propose a formal approach towards synthesizing attack detectors with varying thresholds which can prevent performance degrading stealthy attacks while minimizing false alarms.