Runtime Enforcement for Control System Security (Extended Abstract)

We apply runtime enforcement techniques, based on an ad-hoc sub-class of Ligatti et al.’s edit automata, to enforce specification compliance in networks of potentially compro- mised controllers, formalised in Hennessy and Regan’s Timed Process Language. We define a synthesis algorithm that, given an alphabet P of observable actions and an enforceable regular expression e capturing a timed property for controllers, returns a monitor that enforces the property e during the execution of any (potentially corrupted) controller with alphabet P and complying with the property e. Our monitors correct and suppress in- correct actions coming from corrupted controllers and mitigate malicious actions in full autonomy. Besides classical properties, such as transparency and soundness, the proposed enforcement ensures non-obvious properties, such as polynomial complexity of the syn- thesis, deadlock- and divergence-freedom of monitored controllers, together with scalability when dealing with networks of controllers.