Model Checking the Information Flow Security of Real-Time Systems

Cyber-physical systems are processing large amounts of sensitive information, but are increasingly often becoming the target of cyber attacks. Thus, it is essential to verify the absence of unauthorized information flow at design time before the systems get deployed. Our paper addresses this problem by proposing a novel approach to model-check the information flow security of cyber-physical systems represented by timed automata. We describe the transformation into so-called test automata, reducing the verification to a reachability test that is carried out using the off-the-shelf model checker Uppaal. Opposed to related work, we analyze the real-time behavior of systems, allowing software engineers to precisely identify timing channels that would enable attackers to draw conclusions from the system's response times. We illustrate the approach by detecting a timing channel in a simplified model of a cyber-manufacturing system.