Alessio Coletta^1,2, ¹Bruno Kessler Foundation, Italy and ²University of Trento, Italy

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 work proposes a monitoring framework that leverages the knowledge of the system to monitor in order to specify, check, and predict known critical conditions. This approach is particularly suitable to CPS, as they 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 SMT-based engine that checks observable aspects from network traffic and logs. 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 expressing conditions on the time of the observations and of dealing with unobservable variables. This work presents the formal framework, a prototype, a testbed, and first experimental results that validate the feasibility of the approach.

Security Monitoring, Detection and Prevention Systems, Critical Infrastructures, Cyber Physical Systems, SMT.