Journal
IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS
Volume 18, Issue 7, Pages 4393-4405Publisher
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TII.2021.3123194
Keywords
Monitoring; Safety; Integrated circuits; Security; Runtime; Semantics; Model checking; Industrial control system (ICS); international electrotechnical commission (IEC) 61131-3 standard; programmable logic controller (PLC); runtime verification (RV); temporal logic
Ask authors/readers for more resources
This article discusses how to enhance the security and safety of running PLC in both developing and deploying stages of ICS. By using a runtime verification method and proposing PLC past linear temporal logic (PPLTL) to specify security and safety properties, monitors are synthesized to improve the security and safety of PLC programs. The empirical results demonstrate the effectiveness of this approach.
Programmable logic controllers (PLC), which are widely applied in modern industrial control systems (ICS), work as the controller of sensors and actuators in ICS. These systems require strict correctness, especially for safety-critical systems. Currently, increasingly ICS move to come online scenarios to enhance cyber-physical features, but it makes them more vulnerable due to acquiring increased interconnection accompanied by weakening physical isolation. Moreover, with the more complex controlling environment, such as hundreds of more I/O points and more diverse field buses, the incorrect executions of PLC might cause the failure of the overall ICS. In this article, we examine how the security and safety of running PLC could be enhanced in both developing and deploying stages of ICS. We propose a novel application of runtime verification to guarantee the security and safety of real-world ICS. As a variant of temporal logic, PLC past linear temporal logic (PPLTL) is proposed to specify the security and safety properties of PLC. Using PPLTL, we synthesize monitors to improve the PLC program's security and safety as a partner of testing and static verification. Our monitors provide twofold processing in a nonintrusive manner: One is filtering abnormal input data before invading the original programs, the other is double-checking the output signals before driving the actuators. We use several case studies and benchmarks to demonstrate the efficiency of the approach. The empirical results show that the time overhead and memory occupation are tiny.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available