Predictive Detection of Known Security Criticalities in Cyber Physical Systems with Unobservable Variables

A large number of existing Cyber Physical Systems (CPS) in production environments, also employed in critical infrastructures, are severely vulnerable to cyber threats but cannot be modified due to strict availability requirements and nearly impossible change management. Monitoring solutions are increasingly proving to be very effective in such scenarios. Since CPS are typically designed for a precise purpose, their behaviour is predictable to a good extent and often well known, both from the process and the cyber perspective. This work presents a cyber security monitor capable of leveraging such knowledge to detect illicit activities. It uses a formal language to specify critical conditions and an SMT-based engine to detect them through network traffic and log analysis. The framework is predictive, i.e.\ it recognises if the system is approaching a critical state before reaching it. An important novelty of the approach is the capability of dealing with unobservable variables, making the framework much more feasible in real cases. This work presents the formal framework and first experimental results validating the feasibility of the approach.