Specification-based Predictive Continuous Monitoring for Cyber Physical Systems with Unobservables

Cyber Physical Systems (CPS), like IoT and industrial control systems, are typically vulnerable to cyber threats due to a lack of cyber security measures and hard change management. Security monitoring is aimed at improving the situational awareness and the resilience to cyber attacks. Solutions tailored to CPS are required for greater effectiveness. This PhD work proposes a monitoring framework that leverages the knowledge of the CPS in order to specify, check, and predict known critical conditions. This approach is particularly suitable to CPS which are designed for a precise purpose, well documented, and predictable to a good extent. The framework uses a formal logical language to specify quantitative critical conditions and an optimisation linear programming and SMT-based engine. The framework computes a quantitative measure of the criticality of the current CPS system: checking how criticality changes in time enables to predict whether the system is approaching to a critical condition or reaching back a licit state. An important novelty of the approach is the capability of dealing with unobservable variables, for a greater feasibility for real cases, and the possibility to use observation times in critical specifications. This work presents the formal framework, a prototype, a testbed, and first experimental results that validate the feasibility of the approach.