English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

With the advent of Industry 4.0, industrial facilities and criticalinfrastructures are transforming into an ecosystem of heterogeneous physicaland cyber components, such as programmable logic controllers, increasinglyinterconnected and therefore exposed to cyber-physical attacks, i.e., securitybreaches in cyberspace that may adversely affect the physical processesunderlying industrial control systems. In this paper, we propose a formalapproach based on runtime enforcement to ensure specification compliance innetworks of controllers, possibly compromised by colluding malware that maytamper with actuator commands, sensor readings, and inter-controllercommunications. Our approach relies on an ad-hoc sub-class of Ligatti et al.'sedit automata to enforce controllers represented in Hennessy and Regan's TimedProcess Language. We define a synthesis algorithm that, given an alphabet $P$of observable actions and a timed correctness property $e$, returns a monitorthat enforces the property $e$ during the execution of any (potentiallycorrupted) controller with alphabet $P$, and complying with the property $e$.Our monitors correct and suppress incorrect actions coming from corruptedcontrollers and emit actions in full autonomy when the controller underscrutiny is not able to do so in a correct manner. Besides classicalrequirements, such as transparency and soundness, the proposed enforcementenjoys deadlock- and diverge-freedom of monitored controllers, together withscalability when dealing with networks of controllers. Finally, we test theproposed enforcement mechanism on a non-trivial case study, taken from thecontext of industrial water treatment systems, in which the controllers areinjected with different malware with different malicious goals.

Runtime Enforcement of Programmable Logic Controllers