检测和缓解PLC恶意软件的过程计算方法

原文
A process calculus approach to detection and mitigation of PLC malware
申明
版权归原文作者及出版单位所有，如有侵权请联系删除。

1. 简介

工业控制系统（ICS）是通过连接到传感器和执行器的可编程逻辑控制器（PLC）控制物理过程的分布式系统。PLC有一个临时性的架构来执行被称为扫描周期的简单过程。每个扫描周期包括三个阶段：（i）读取传感器对物理过程的测量值；（ii）推导出指导物理过程演变的命令；（iii）将计算出的命令传输到执行器。

已公布的扫描数据表明，成千上万的PLC是如何从互联网上直接访问的[2]。此外，PLC经常在现场通信网络中相互连接，为蠕虫的传播开辟了道路，如 PLC-Blaster蠕虫[3]或PLC PIN控制攻击[4]。

因此，人们提出了额外的可信硬件组件来增强ICS架构的安全性[5, 6]。在这方面，McLaughlin[5]提议增加一个基于政策的执行机制，以调解PLC传输到物理工厂的执行器命令，而Mohan等人[6]引入了一个架构，其中每个PLC运行如果行为不符合预期，则控制权将移交给安全控制器，该控制器将工厂维持在所需的安全范围内。上述两种结构都是通过基于仿真的技术进行验证的。

本文的目的是验证过程微积分方法的有效性，以正规化地执行被注入恶意软件的PLC网络中的规范，这些恶意软件可能伪造/删除执行器命令和控制器之间的通信。1过程计算代表了并发理论中一种成功而广泛的形式化方法，它依赖于各种行为等价物（例如，跟踪等价物和双相似性）来研究复杂系统，如物联网系统[8-10]和网络物理系统[11,12]，并用于许多领域，包括安全协议的验证[13,14]和网络物理攻击的安全分析[15]。

另一方面，运行时执行[16-18]是一种强大的验证/确认技术，旨在通过一种作为SuS和其环境之间的代理的监控器，纠正受监督系统（SuS）可能的错误执行。在本文中，我们建议通过具有以下特性的特设代理（监视器）来执行PLC。

• 基于观察的监控，也就是说，代理应该只看PLC的可观察数据，而不是其内部执行情况。

• 透明度，即被监控的PLC的语义不能与真正的（即未被监控的）PLC的语义不同。

• 健全受监控的PLC的执行，以防止错误的执行。

• 死锁自由，即注入的恶意软件不能将被监控的PLC拖入死锁状态。

• 及时发现PLC的错误行为，向系统工程师发出警报（他们将重新安装PLC代码的混淆变体）。

• 缓解被监控的PLC内的恶意活动。

显然，如果PLC被破坏了，那么它的正确执行只能借助于一个额外的组件，一个安全的代理，正如McLaughlin[5]和Mohan等人[6]所主张的，它没有任何互联网或USB的访问，并且通过强调安全的通道与被监控的控制器相连。这看起来就像我们只是把问题转移到了保护代理上。然而，情况并非如此，因为代理只需要在运行时执行正确性，而PLC控制其物理过程，依靠的是通过互联网或USB端口的易受恶意软件影响的通信。当然，决不允许在运行时对安全代理进行重新配置。

2. 用于监测的PLC的定时过程计算

我们将我们的过程微积分定义为Hennessy和Regan的定时过程语言（TPL）[19]的扩展，这是一个具有离散时间概念的简单过程微积分。与其他定时进程计算不同，TPL享有五种理想的时间属性。(i) 离散时间：时间以离散的步骤进行，由一个简单的动作tick的发生来代表；(ii) 时间决定论：时间的流逝是决定性的，即，一个进程通过执行定时的动作tick最多可以达到一个新的状态。(瞬时行动：时间不与行动直接相关，而是独立发生；（iv）耐心：进程将无限期地等待，直到它们可以通信；（v）最大进展：数据传输不能延迟，它们必须在通信的可能性出现时立即发生。

在描述我们的微积分之前，我们提供一些初步的符号。我们用s, sk ∈Sens表示传感器信号，a, ak ∈Act表示执行器命令，c, ck ∈Chn为通道名称。

控制器。在我们的设定中，控制器是非确定性的顺序计时过程，通过三个不同的阶段演变：传感器信号的感应、与其他控制器的通信、以及执行。为方便起见，我们使用四个不同的我们用不同的句法类别来区分控制器的四个主要状态。Ctrl表示初始状态，Sens表示感知状态，Com表示通信状态，Act表示执行状态。在其初始状态下，控制器是一个递归过程在感应阶段开始其扫描周期。

请注意，由于控制器的循环行为，过程变量X在语法上可能只出现在最后阶段，即启动阶段。我们假设有时间保护的递归，也就是说，过程变量的出现必须以至少一个定时的动作刻度为前提。这使我们能够避免不希望出现的Zeno行为[23]：两个有时间限制的转换之间的无时间限制的转换数量总是有限制的。

转换之间的无时间限制的转换数量总是有限制的。在感应阶段，控制器等待一定数量的稳定传感器信号。如果这些信号在当前时隙中没有到达，那么控制器将超时移动到下一个时隙（我们采用TPL结构L-J-来超时）。控制器也可以休眠一段时间，等待传感器信号变得稳定。语法如下。

其中
表示非决定性选择的标准构造。一旦感应阶段结束，控制器开始它的计算，这些计算可能依赖于与其他控制器的通信。控制器与彼此之间的通信主要有两个原因：要么接收关于其他物理子过程状态的通知，要么要求对不同的物理过程进行操作，这将对控制器所管理的物理过程产生影响。我们采用基于信道的握手点对点通信模式。由于PLC通常在时间限制下工作，我们的通信总是处于超时状态。通信阶段的语法是。

因此，我们的控制器既可以在一定数量的通信信道上收听，也可以在特定的信道上发送，以传递一些本地信息。一旦通信阶段结束，控制器就进入了执行阶段。

在执行阶段，控制器最终会向一些不同的执行器发送一个有限的命令序列，然后，它发出一个特殊的信号end来表示扫描周期的结束。之后，它通过一个用过程变量X表示的递归调用，重新开始其在感知阶段的周期。为了确保语义的封闭性，我们也有一个结构体end。P，它只在运行时产生，但从不用于编写PLC程序。

表1中给出了控制器的操作语义。在下文中，我们使用元变量α和β来涵盖可能的行动集合。{s, a, a, c, c, τ, tick, end}。这些动作表示：传感器读数、执行器命令、执行器命令的下降、通道传输、通道接收/下降、内部动作、时间的推移和扫描的结束。

表1 控制器的LTS

表2 恶意软件代码的LTS

恶意软件。我们给出了恶意软件代码的形式化，我们认为这些代码可能被注入到控制器中以破坏其运行时的行为。我们希望处理的恶意软件可以执行以下恶意活动。

• 伪造虚假的控制器间通道传输（通过行动c）。

• 丢弃来自其他控制器的传入通信（通过动作c）。

• 伪造假的执行器命令（通过行动A）。

• 掉落由控制器发起的执行器指令（通过动作a）。

承认的恶意软件的正式语法如下。

其中序号μi ∈{c, c, a, a}，对于i∈I，表示上面提到的可能的恶意行为。同样，我们假设有时间保护的递归，以避免恶意软件引入不希望有的Zeno行为，也就是说，恶意软件可能永远不会阻止控制器中的时间无限制地流逝。

表2中给出了一个直接的操作语义。

被破坏的控制器。在我们的设置中，被破坏的控制器是一个可能与任意的恶意软件平行运行的控制器。

表3 被破坏控制器的LTS

其中，Z∈ Ctrl ∪Sens ∪Comm ∪Act表示处于任意状态的控制器，|是平行组合的标准过程代数结构。

表3的过渡规则给出了一个被破坏的控制器的操作语义。规则（Ctrl）模拟控制器的真实行为，即使在恶意软件存在的情况下（可能是在等待一个适当的触发）。规则（Inject）表示注入恶意软件制造的恶意行动。规则（DropAct）是指执行器命令a的删除；这样，命令a永远不会到达其预定的执行器设备。规则（TimePar）表示控制器和恶意软件之间的时间同步（我们记得，恶意软件不能表现出齐诺行为）。

受监控的控制器。我们的运行时强制执行的核心依赖于finite-state Ligatti等人的编辑自动机[17]的一个（定时）子类，即一类特殊的自动机，专门用于修改/抑制/插入通用系统中的动作，以保持其正确行为。其语法定义如下。

直观地说，自动机go将承认被监控系统的任何行动，而编辑自动机。Ei 取代了行动 αi 与 β i ，然后继续作为 Ei ，对于任何i∈I，I是有限的。我们的编辑自动机的操作语义是通过以下三个过渡规则来确定。

当编辑自动机执行一个标记为α►β的转换时，α /= τ，β = τ，我们说自动机超压了可观察的动作α。

我们的受监控的控制器，写成E 1-{ J }，由一个（潜在的）被破坏的控制器J和一个根据以下过渡规则强制执行J的行为的编辑automaton E构成，用于纠正或控制。

在一个内部没有恶意软件的受监控的控制器E 1-{ J }中，强制执行永远不会发生，即，在规则（强制）中我们总是有α=β，两个成分E和J以拴住的方式演化，在相关的正确状态中移动。

我们可以很容易地将监控控制器的概念概括为一个由平行监控控制器组成的现场通信网络，每个控制器都作用于不同的执行器，并通过通道交换信息。这些网络通过语法进行了正式的定义。

并通过表4中给出的操作语义进行描述。请注意，被监控的控制器可以通过通道通信相互作用。此外，当没有通信发生时，它们可以及时演变（我们回顾一下，控制器和恶意软件都不承认零星行为）。这确保了我们的最大进展[19]，这是为实时系统建模时的一个理想的时间属性：通信不会被推迟到未来的时间段。

表4 用于检测现场通信网络的LTS

3. 用例：一个简单的输水网络

在这一节中，我们描述了如何在我们的微积分中指定一个非复杂的PLC网络来控制一个输水网络（WTN）。

图1 水运网络的典型结构典型的水网是由以下主要物理元素组成的。(i) 水箱，(ii) 泵站，(iii) 水源（如钻孔），和(iv) 管道。图1代表了几个水务公司的典型构架[28]，同样的结构被复制到更大的基础设施。在这个设置中，借用了[29]，用泵从水源（如井眼或其他水箱）提取水。泵增加水压，将水推入其他水箱，这些水箱可能位于几公里外的高处。每个水箱都配备了一个阀门，用于排除多余的水。表5 用于管理水箱T1的PLC代码

WTNs的有限状态机控制逻辑非常简单。在表5中，我们提供了一个可能的代码Pi 的控制器PLCi ，管理水箱Ti 及其物理设备（传感器和执行器）。在这里，PLC等待一个时隙（以获得稳定的传感器信号），然后检查水箱的水位Ti ，区分三种可能的状态。

如果水位很低（信号l），那么PLC通过通道传输向子系统i-1发送水的请求。turnoni -1，发给PLCi -1，要求打开其水泵。如果该请求被接受，那么PLCi 会在turnoni 和turnoffi 两个通道上监听来自PLCi +1的水请求。根据这些请求是否被接受，PLCi 将打开/关闭它的泵（分别通过命令on或off），关闭阀门（通过命令close），并且它将结束扫描循环。如果没有来自PLCi +1的传入请求，那么PLCi 会超时，关闭阀门，然后结束扫描周期。i同样，如果在当前时隙内，PLCi -1不接受供水请求，那么它就会超时，关闭阀门，最终结束扫描周期。

如果水箱Ti 的水位很高（信号h），那么当检测到低水位（信号l）时，PLCi 的行为就与之前的情况类似。

最后，如果水箱Ti 的水处于l和h之间的某个中间水平（信号m），那么PLCi 就会监听水来自PLC的请求i +1，以打开/关闭泵。如果它在当前时隙中得到其中一个请求，那么它就会做出相应的反应，否则就会超时并结束扫描周期。更准确地说，如果PCLi 得到一个打开i 的请求，那么它就打开泵，让水从Ti 流到Ti +1；否则，如果它得到一个关闭i的请求，它就关闭泵；在这两种情况下，它都结束扫描周期，然后返回。

4. 合成监控

在表6中，我们提供了一个合成函数[-]，给定一个确定性的控制器P∈Ctrl，返回一个语法确定的[21]编辑自动机E∈Edit，强制执行P的正确行为，而不考虑存在一个任意的恶意软件M∈Malw，试图注入和/或放弃执行器命令和通道通信。

表6 合成算法[-]

表7 从第3节的PLCi的代码Pi中合成的编辑自动机

让我们评论一下合成函数的细节，表6的。与倾听有关的编辑自动机在传感器信号允许控制器预期的所有传入信号，加上最终的时间流逝而导致的超时。所有其他行动都被抑制。与通信信道监听相关的编辑自动程序是类似的，除了控制器不允许的通信被抑制，以防止系统信道上的下降和中断，以及在不同PLC中运行的串通恶意软件之间的秘密通信。信道传输只允许以正确的顺序发生在控制器指定的信道上；所有其他行为都被抑制。只有真正的执行器命令（同样，以正确的顺序）才被允许。执行器命令的下降，是发生在真正的控制器和恶意软件之间的唯一可能的控制器内部互动，是允许的，因为我们想要一个基于观察的监控。最后，监控编辑自动机和相关的控制器在每个控制器周期结束时通过动作端进行同步：所有由被破坏的控制器发出的其他动作都被抑制，包括那些来自真正的控制器的动作，由于一些模仿（部分）正确行为的注入攻击而在其执行中被留下。我们回顾一下，只有构造end.X（而不是end.P）被用来编写PLC程序。

作为一个例子，在表7中，我们提供了由我们的综合算法产生的编辑自动机，该算法适用于我们用例中介绍的PLC。为了简单起见，我们使用了参数化的过程，并稍稍滥用了符号。在证明由我们合成的监视器诱导的执行机制的技术特性之前，我们将注意力集中在两个简单的观察上。

5. 缓解：僵局到自由的秘诀

在本节中，我们为受监控的控制器引入了一个额外的过渡规则，以实现缓解，即当控制器与执行者失去联系时，在完全自主的情况下插入由编辑自动机驱动的活动序列。

直观地说，如果被破坏的控制器通过动作端发出扫描周期结束的信号，同时，当前的监视器E不处于相同的状态，那么E将命令执行一个安全跟踪，没有任何控制器的参与，以达到控制器周期的结束。当控制器和编辑自动机对齐时（在周期结束时），它们将通过应用过渡规则（Enforce）在动作端同步，从那时起，它们将以拴住的方式继续。

请注意，在一个被监控的控制器E 1-{ J }中，J被一些恶意软件破坏，两个组件E和J在这种情况下，被破坏的控制器J的当前周期中剩余的可执行动作可能会被错误地排列，因为它们可能会达到不相关的状态。例如，在执行器命令下降的情况下，被破坏的控制器J可能会达到一个不正确的状态，留下其监测编辑自动机E。在这种情况下，被破坏的控制器当前周期中剩余的可服务的行动将被抑制，直到控制器达到扫描周期的终点，由一个结束行动的发射来标志（注意，由于我们的恶意软件是有时间保护的，他们不能引入Zeno行为来阻止控制器达到其扫描周期的终点）。一旦被破坏的控制器，被驱动到其周期的终点，过渡规则（缓解）就会开始行动。

6. 在Simulink中进行模拟

在这一节中，我们使用Simulink[22]（基于MATLAB的图形编程环境）来模拟第3节中给出的WTN系统，当它受到三种不同的攻击时，目标是配备了我们合成的强制监视器的PLC（见表7）。本节的目标是展示当我们监测的PLC实际被注入未知的恶意软件时，执行工作是如何进行的。为了模拟在PLC中注入恶意软件，我们基本上用受损的PLC代码重新安装真正的PLC，其中包含一些额外的逻辑，旨在破坏PLC的正常操作（例如，见梯形逻辑炸弹[20]）。

6.1. 我们的Simulink模型

Simulink是一个仿真框架，它提供了一个图形化的块状图工具和一套定制的块状库的接口，用于建模、仿真和分析网络物理系统。Simulink模型是由块和块之间的互连（称为线）组成的。块是用来模拟逻辑和物理组件的，而线是用来在块之间交换信息的。我们的模型包含三种块：水箱、PLC和监视器（见图2）。特别是，水箱块实现了微分方程，根据从[28]中获得的物理约束，对水箱的流动进行建模。PLC模块包含PLC代码（见图3左侧），其目标是使水箱中的水位保持在低位和高位之间（这两个值是根据经验得出的）。在我们的模拟中，每个扫描周期的持续时间在没有强制执行的情况下被固定为100毫秒，而当PLC配备了我们的强制执行机制时，则为110毫秒。

在图4中，我们提供了一个在PLC指导下的WTN单罐的可接受的运行。最后，关于监控块，我们用Python实现了表6的合成算法。图3的右侧包含了从我们的合成中得到的编辑自动机的部分代码；特别是，我们提供了以下代码的实现表7中定义的自动机ChkLvl、Reqh和C（open）。

我们的 Simulink 模型采用以下物理简化： (i) 泵和阀门的状态变化不消耗时间：它们是瞬时发生的； (ii) 连接不同PLC的网络是通过有线实现的，因此网络不会引入传输延迟； (iii) PLC 总是在每个扫描周期发送一条消息，无论它们是否有要通信的东西：因此，我们假设在没有请求时额外传输 no_reqi-1；因此，在每个扫描周期中，我们模拟的 PLCi 将向 PLCi-1 发送以下三个消息之一：turnoffi-1 或 turnoni-1 以调整相应水箱的水位，而无需调整时为 no_reqi-1。

6.2. 攻击WTN系统的PLC

在模拟注入恶意软件的压力下的执行机制之前，我们回顾一下，在我们的过程计算中，并行过程Ctrl | Malw只是PLC代码Ctrl注入恶意软件Malw的顺序执行的形式抽象。因此，为了模拟PLC中存在一个特定的恶意软件，我们的Simulink PLC块包含一个机制，用从库中选择的恶意软件破坏的代码重新安装PLC。在本节中，我们重点讨论三种不同的恶意软件，以实现不同的目标。

1.一个恶意软件会使受控水箱过流。

2.清空受控水箱的恶意软件。

3.两个串通的恶意软件破坏了相邻的PLC，使一个水箱过流，另一个水箱清空。

在下文中，我们将讨论这三种攻击，说明本文提出的执行机制如何减轻它们的恶意活动，保持受监控PLC的正确行为。第一种攻击通过两种恶意活动损害了PLCi ：(i) 完整性攻击，注入打开水泵的请求，将水引入；(ii) DoS攻击，丢弃打开阀门的真正命令。我们使用我们的微积分来正式确定注入的恶意软件M1

最初，恶意软件保持m个时间瞬间的待命状态；然后无限地重复以下有效载荷：它等待一个时间瞬间，然后注入一个请求turnoni -1，以打开系统i-1的泵，将水从Ti -1抽到Ti ；如果请求被接受，那么它放弃由PLCi 发送的打开阀门的命令。通过这种方式，PLCi -1不会关闭向相邻水箱Ti 送水的泵，同时，Ti 的阀门的打开是被阻止。因此，水箱Ti ，最终会出现溢流。

在没有强制监控的情况下，恶意软件M1 对PLCi 的影响表现在图5的上图中，其中红色区域显示攻击变得活跃。读者可以注意到，阀门从未被打开，被攻击的PLCi 总是发送打开i -1 的请求。另一方面，当PLC的执行被激活时，图5的下图显示，PLCi 的正确行为得到了保证，从而防止了水箱Ti 的溢出。在该图中，绿色突出显示的区域表示监控器检测到攻击并减轻被攻击的PLC的指令i。特别是，当水位高于HIGH时，阀门保持打开状态，而打开i -1 的请求是。(i) 允许，当水位低于LOW时，(ii) 抑制，当水位在LOW和HIGH之间时，(iii) 修正为关闭i -1，当水位高于HIGH时。

我们的第二次攻击通过两种不同的恶意活动损害了PLCi ，与之前的攻击相辅相成：（i）完整性攻击，注入关闭引水的水泵的请求；（ii）DoS攻击，丢弃关闭阀门的真正命令。我们使用我们的微积分来正式确定注入的恶意软件M2 。

同样，恶意软件M2 在最初的 m个时间瞬间保持静止状态。然后，它无限制地重复以下有效载荷：它等待一个时间瞬间，然后注入一个关闭请求i -1，以关闭系统i-1的泵；如果请求被接受，那么它就会放弃由PLCi 发送的关闭阀门的命令。通过这种方式，PLCi -1将不会打开给相邻水箱Ti 送水的泵，同时，Ti 的阀门关闭也被阻止了。其结果是。水箱Ti ，最终将被清空。

在没有强制监控的情况下，恶意软件M2 对PLCi 的影响显示在图6的上图。同样，红色区域表示攻击变得活跃的时间。读者可以注意到，阀门从未关闭，而妥协的PLCi 始终发送关机请求i -1。另一方面，当PLC的监控被激活时，图6的下图显示，PLC的正确行为被强制执行，防止水箱Ti的耗尽。在该图中，绿色突出显示的区域显示了当监控器检测到攻击并减轻指令时的情况。

我们的第三次攻击针对两个连续的 PLC，PLCi 和 PLCi+1，目标是溢出储罐 Ti 并清空储罐 Ti+1。注入两台受感染 PLC 的共谋恶意软件 Mi3 和 Mi3+1 必须首先同步以避免相互干扰。同步后，恶意软件 Mi3 会执行以下活动：（i）通过注入请求以打开将水输送到水箱 Ti 的泵的完整性攻击，（ii）通过丢弃关闭将水从 Ti 输送到水的泵的请求的 Dos 攻击 Ti+1，以及 (iii) 通过丢弃 PLC 命令打开阀门的另一次 Dos 攻击。共谋恶意软件 Mi3+1 具有更简单的有效负载，因为它通过对用于关闭阀门的 PLC 命令的 DoS 攻击来防止阀门关闭。我们将恶意软件 Mi3 和 Mi3+1 形式化，如下所示：

恶意软件M3 ，最初保持m个时间段的待命状态，然后无限期地重复以下有效载荷。(i) 它等待一个时间瞬间，然后与M3 同步；如果同步失败，在一个时间后再次重试。i+1 瞬间；(ii)如果同步成功，那么它就会注入一个打开i -1 的请求；(iii)丢弃一个传入的关闭i 的请求；(iv)丢弃PLC发送的命令来打开阀门。在前 n个时间段，恶意软件M3 保持待命状态。然后，它无限制地重复以下的有效载荷。(i) 它等待一个时间瞬间，然后与M3 同步；如果同步失败，那么它在一个时间瞬间后再次重试；(ii) 如果同步成功，那么它放弃从PLC发送的关闭阀门的命令。

串通的恶意软件的联合行动将产生以下影响：（i）PLCi -1永远不会关闭将水从Ti -1带到Ti 的泵，同时，Ti 的阀门被阻止打开；（ii）PLCi 永远不会打开将水从Ti 带到Ti +1的泵，同时，Ti +1的阀门被阻止关闭。因此，水箱Ti 会过流，尽管有大量的水，水箱Ti +1最终会被清空。

在没有强制监控器的情况下，共谋恶意软件的影响如图 2 所示。 7. 攻击开始时红色区域亮起。读者可以注意到，Ti 的阀门永远不会打开，受感染的 PLCi 总是发送 turnoni-1 请求并总是丢弃 turnoni 请求。另一方面，Ti+1 的阀门从不关闭。

图8 对Ti（左）和Ti+1（右）的第三次攻击，使用强制监控器

图 8 显示了两个 PLC 的正确行为被强制执行，防止了水箱 Ti 的溢出和水箱 Ti+1 的耗尽。特别是，当监视器检测到攻击并减轻受感染 PLCi+1 的命令时，绿色突出显示区域：PLCi 同步请求的传输被抑制，因为监视器只允许传输：turnoffi-1，turnoni-1 , 和 no_reqi-1。因此，由于两个受损的 PLC 无法同步，因此攻击失败。

7. 结论和工作

我们已经定义了一种正式的语言来表达受监控的PLC网络，这些网络可能被串通的恶意软件破坏，这些恶意软件可能伪造/删除执行器的命令和控制器之间的通信。我们不处理PLC内传感器信号的改变，因为它们已经可以在网络层面或传感器设备内被改变了[7]。

运行时的执行是通过Ligatti编辑自动机的一个最小状态子类来实现的，该子类配备了一个特殊的操作语义来处理系统的缓解问题，当被监控的控制器不能以正确的方式插入行动时，就完全自主。

然后，我们提供了一种合成算法，给定一个确定的未损坏的控制器，在多项式时间内返回一个句法确定的编辑自动机，以执行控制器的正确性。所提议的执行满足了一些要求：基于观察的监控、透明性、健全性、无死锁，以及在注入恶意软件的情况下检测和缓解被监控的PLC行为的改变。我们已经在Simulink中实现了我们的用例和我们的监测器。然后，我们测试了三种危害我们用例中的PLC的恶意软件，显示了我们的强制监控器在检测和缓解发生在被危害的PLC中的恶意活动的有效性。

**相关工作。**本工作是对出现在[1]中的扩展摘要的修订延伸。在这里，除了完整的证明，我们还提供了关于监测安全代理的异常检测和缓解活动的新结果。特别是，正如命题6和命题8所正式指出的，我们的安全代理能及时检测到异常行为，并通过缓解它们来安全地进行干预。此外，与会议论文相比，在第3节中，我们提供了一个更多的和现实的使用案例，来自输水网络的领域。另一个原创性的贡献是在Simulink中实现了我们的（强制）用例，该用例暴露于针对PLC的三种不同攻击。

在我们的配套论文[37]中，我们对PLC的实现进行了抽象，并提供了一种简单的正则道具语言来表达正确性属性，在完成PLC扫描周期时应该强制执行。作为一个主要的结果，即使在注入的恶意软件完全控制了PLC内的活动，包括通道通信和传感器信号的读取，也能确保正确性属性的执行

运行时执行的概念是由Schneider[16]引入的，用于执行安全策略。这些属性是通过截断自动机来执行的，截断自动机是一种在违反属性的情况下终止被监控系统的自动机。因此，截断自动机只能执行安全属性。Ligatti等人[17]通过提出编辑自动机的概念扩展了Schneider的工作，即一种能够替换、压制甚至插入系统动作的执行机制。编辑自动机能够执行安全和活泼属性的实例，以及其他属性，如更新属性[31,17]。一般来说，Ligatti等人的编辑自动机有无数个状态，而在本文中，我们将自己限制在无状态的编辑自动机。此外，在其原始定义中，行动的插入在任何时候都是可能的，而我们的监测编辑自动机可以通过规则（Mitigation）插入行动。

只有当被检查的PLC达到一个特定的状态，即扫描周期结束时，才会有一个动作。请注意，我们的α ►β形式的行动可以通过插入行动β 然后压制行动α的方式在原始表述中轻松表达。与Schneider和Ligatti等人不同，我们没有为所有可接受的系统（在我们的例子中是控制器）强制执行特定的属性，但我们确保保留一个被破坏的控制器的正确语义。Bielova和Massacci[31,38]通过引入一个可预测性标准来防止监控器以任意的方式转换无效的执行，提供了一个更强大的可执行性概念。直观地说，如果可以预测用于纠正无效执行的转换数量，从而避免不必要的转换，就可以说监控器是可预测的。在我们的案例中，我们从未引入不必要的转换，因为我们的合成是基于控制器的确切知识。Falcone等人[32,18]提出了一种综合算法，依靠Streett自动机，将安全进程中定义的大多数属性类转化为安全进程中的属性。

层次结构[39]变成执行者。Könighofer等人[33]提出了一种综合算法，给定一个安全属性后会返回一个监视器，称为盾牌，该监视器分析反应式系统的输入和输出，以便仅通过修改输出来执行属性。Pinisetty等人[40]为反应式系统，以及更普遍的网络物理系统提出了一种双向的运行时执行机制，以纠正输入和输出。Aceto等人[30]开发了一个操作框架，以强制执行带有递归的HML逻辑（μHML）中的属性，这依赖于抑制。更确切地说，他们通过提供一个线性自动合成算法，从公式中生成正确的抑制监视器，实现了μHML的安全片段的执行。在这里，为了避免死锁，当SuS达到一个状态，在这个状态下监控器不指定任何转换，监控器就会停止活动，充当去监控器（另见[34]）。Martinelli和Matteucci[41]曾通过一种合成算法来解决模态μ-culus（μHML的重述）的可执行性问题，该算法在可执行公式的长度上是指数级的。最近，Cassar[42]定义了一个通用的框架来比较不同的执行模型和不同的正确性标准，包括最优性。他的工作，重点是μHML的安全片段的执行，注意执行的方向性和双向性的概念。

段的执行。在这里，为了避免死锁，当SuS达到一个状态，在这个状态下监控器不指定任何转换，监控器就会停止活动，充当去监控器（另见[34]）。Martinelli和Matteucci[41]曾通过一种合成算法来解决模态μ-culus（μHML的重述）的可执行性问题，该算法在可执行公式的长度上是指数级的。最近，Cassar[42]定义了一个通用的框架来比较不同的执行模型和不同的正确性标准，包括最优性。他的工作，重点是μHML的安全片段的执行，注意执行的方向性和双向性的概念。

最后，我们的工作可能会让读者想起监督控制理论[35,36]，这是一个为离散事件系统自动合成控制器（监督器）的一般理论，给定一个工厂模型和受控行为的规格。Fabian和Hellgren[43]指出了在基于PLC的工业设施中采用监督控制理论时需要解决的一些问题，如因果关系、不正确的同步和替代路径的选择。然而，，在我们的论文中，我们专注于一种完全不同的综合：从控制器到执行监控器。由于我们的合成只涉及逻辑设备（不涉及工厂），所以我们不会受到Fabian和Hellgren提到的类似问题的影响。