SoK: Attacks on Industrial Control Logic and Formal Verification-Based Defenses
share
Control logic programs play a critical role in industrial control systems. A vulnerable control logic could lead to devastating consequences in the physical processes, as shown in Stuxnet and similar attacks. Over the years, academic and industrial researchers have investigated various fault injection and modification attacks on control logic as well as formal verification-based defenses. Although formal verification techniques have in general improved the quality of control logic programs, we find a significant gap between the academic research and the industry practices in defending against attacks on control logic. Besides, the future research directions remain unclear as to protect control logic from the ever-expanding attack surface partly caused by the increasing needs for inter-connectivity. This work fills the gap by systematizing the knowledge of control logic modification attacks and the formal verification-based defenses. Our study covers the full chain of developing and deploying control logic programs, from engineering stations to target PLC. The primary goals of the systematization are (1) to explore the evolving technology and security landscape surrounding control logic programs, (2) to investigate newly emerged attack surfaces on PLC systems and the formal verification-based defenses, and (3) to identify the open challenges and needs that existing formal verification based-defenses failed to address. Based on the knowledge systematization, we provide a set of recommendations for both academic researchers and industry practitioners to better focus their work on countering critical and emerging threats.
READ FULL TEXT