SoK: Attacks on Industrial Control Logic and Formal Verification-Based Defenses
SoK: Attacks on Industrial Control Logic and Formal Verification-Based Defenses
复制标题
DOI：
10.1109/eurosp51992.2021.00034
复制
发表时间：
2020-06
期刊：
影响因子：
--
通讯作者：
Ruimin Sun;Alejandro Mera;Long Lu;D. Choffnes
中科院分区：
文献类型：
--
作者：
Ruimin Sun;Alejandro Mera;Long Lu;D. Choffnes
可编程逻辑控制器(PLC)在工业控制系统中起着至关重要的作用。PLC程序中的漏洞可能会导致攻击，对关键基础设施造成毁灭性的后果，如Stuxnet和类似攻击所示。近年来，我们看到PLC控制逻辑报告的漏洞呈指数级增加。回顾过去的研究，我们发现大量的研究探索了控制逻辑修改攻击，以及基于形式化验证的安全解决方案。我们对这些研究进行了系统化的研究，发现了可能危及整个控制链并逃避检测的攻击。然而，大多数正式的验证研究都是针对PLC程序的特别技术。我们在形式化验证的各个方面都发现了挑战，这些挑战来自(1)进化系统设计不断扩大的攻击面，(2)程序执行期间的实时约束，以及(3)在给定专有和供应商对不同技术的依赖的情况下的安全评估障碍。在知识系统化的基础上，我们对未来的研究方向提出了一套建议，并强调了除了安全问题之外，防御安全问题的必要性。
Programmable Logic Controllers (PLCs) play a critical role in the industrial control systems. Vulnerabilities in PLC programs might lead to attacks causing devastating consequences to the critical infrastructure, as shown in Stuxnet and similar attacks. In recent years, we have seen an exponential increase in vulnerabilities reported for PLC control logic. Looking back on past research, we found extensive studies explored control logic modification attacks, as well as formal verification-based security solutions. We performed systematization on these studies, and found attacks that can compromise a full chain of control and evade detection. However, the majority of the formal verification research investigated ad-hoc techniques targeting PLC programs. We discovered challenges in every aspect of formal verification, rising from (1) the ever-expanding attack surface from evolved system design, (2) the real-time constraint during the program execution, and (3) the barrier in security evaluation given proprietary and vendor-specific dependencies on different techniques. Based on the knowledge systematization, we provide a set of recommendations for future research directions, and we highlight the need of defending security issues besides safety issues.