| Title | Runtime Enforcement for Control System Security |
| Publication Type | Conference Paper |
| Year of Publication | 2020 |
| Authors | Lanotte, R., Merro, M., Munteanu, A. |
| Conference Name | 2020 IEEE 33rd Computer Security Foundations Symposium (CSF) |
| Keywords | actuator security, actuators, ad-hoc sub-class, alphabet P, Automata, classical properties, composability, control system security, controller, corrupted controllers, critical infrastructures, cyber components, cyber-physical attacks, enforceable regular expression e, explosion, external events, formal languages, heterogeneous physical components, Human Behavior, incorrect actions, industrial control, industrial control systems, industrial facilities, Ligatti et al., Metrics, monitored controllers, Monitoring, nonobvious properties, observable actions, physical processes, PLC malware, potentially compromised controllers, Process calculus, process control, program verification, Programmable Logic Controllers, pubcrawl, Regan's Timed Process Language, Resiliency, Runtime, runtime enforcement, runtime enforcement techniques, security, security breaches, security of data, Sensors, smart systems, specification compliance, synthesis algorithm, timed property |
| Abstract | With the explosion of Industry 4.0, industrial facilities and critical infrastructures are transforming into "smart" systems that dynamically adapt to external events. The result is an ecosystem of heterogeneous physical and cyber components, such as programmable logic controllers, which are more and more exposed to cyber-physical attacks, i.e., security breaches in cyberspace that adversely affect the physical processes at the core of industrial control systems. 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 compromised 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 incorrect actions coming from corrupted controllers and emit actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner. Besides classical properties, such as transparency and soundness, the proposed enforcement ensures non-obvious properties, such as polynomial complexity of the synthesis, deadlock- and diverge-freedom of monitored controllers, together with scalability when dealing with networks of controllers. |
| DOI | 10.1109/CSF49147.2020.00025 |
| Citation Key | lanotte_runtime_2020 |
Runtime Enforcement for Control System Security