Bridging Dolev-Yao Adversaries and Control Systems with Time-Sensitive Channels

Defining security objectives for industrial control scenarios is a challenging task due to the subtle interactions between system components and because security goals are often far from obvious. Moreover, there is a persistent gap between formal models for channels and adversaries (usually, transition systems) and models for control systems (differential or recurrent equations). To bind these two realms, we translate control systems into transition systems by means of an abstraction with variable time granularity and compose them with a channel model that is controlled by Dolev-Yao adversaries. This opens the road for automatic reasoning about the formal model of a control system using model checkers in a context where the communication channel is tampered with. We address a security objective that has so far largely eluded in models, namely freshness, which is highly relevant for control systems. Beyond the traditional resilience to replay attacks, we point out several flavours of freshness which are often overlooked, e.g., ordering and bounded lifespan. We formalize these notions and show that their absence can lead to attacks that subvert the control system. Finally, we build a proof-of-concept implementation that we use to determine attacks on a simple model which clearly shows that real-world scenarios are within reach.