可编程逻辑控制器的运行时强制

随着工业 4.0 的到来，工业设施与关键基础设施正转变为异构物理与网络组件（如可编程逻辑控制器）的生态系统，其互联程度日益加深，因此暴露于网络物理攻击之下，即可能 adversely 影响工业控制系统底层物理过程的网络空间安全 breach。本文提出一种基于运行时强制的形式化方法，以保障控制器网络中的规约合规性，这些网络可能遭到合谋恶意软件破坏，后者可篡改执行器命令、传感器读数及控制器间通信。我们的方法依赖于 Ligatti 等人编辑自动机的一个专用子类，以强制表示为 Hennessy 与 Regan 的定时过程语言的控制器。我们定义了给定可观测动作字母表 $P$ 与定时正确性性质 $e$ 后，返回在任意（可能受损）字母表 $P$ 控制器执行期间强制性质 $e$ 且符合性质 $e$ 的监视器的综合算法。我们的监视器纠正并抑制来自受损控制器的不正确动作，并在受监视控制器无法以正确方式发出动作时自主发出动作。除透明性与可靠性等经典要求外，所提强制机制还具备受监视控制器的无死锁与无发散自由，以及处理控制器网络时的可扩展性。最后，我们在取自工业水处理系统的非平凡案例研究中测试了该强制机制，其中控制器被注入具有不同恶意目标的不同恶意软件。