面向设备级网络攻击的嵌入式网络物理系统形式化弹性框架

大家读完觉得有帮助记得关注和点赞！！！

摘要​

在网络物理系统（CPS）中，容错通常通过传感器与执行器输出来实现，即检测渐进漂移或突发故障，并启动相应的容错机制。这种方法在一般故障模型下是合理的，但无法捕捉网络攻击造成的细微扰动——攻击者往往采用隐蔽策略。这在嵌入式CPS中尤为关键，因为其中的计算与物理设备不仅在任务完成中发挥主动作用，还承担着形态保持（即维持系统物理完整性）的职责。为防止结构性物理损坏，嵌入式CPS需要一个能主动响应网络攻击的框架。本文提出一种形式化可靠性框架，将入侵检测系统（IDS）信息纳入弹性评估谓词，从而支持对扰动容忍度与性能退化程度的评估。该框架支持对网络攻击如何影响任务执行与形态保持，以及是否需要部署缓解策略进行结构化推理。通过解析示例，本文验证了该框架的分析能力与合理性，为可靠、安全的嵌入式CPS奠定了理论基础。

索引术语：网络物理系统（CPS）、嵌入式CPS、网络安全、机器人、物联网、形态完整性、框架、可靠性、形式化方法、入侵检测、弹性建模、安全保证。

---

I. 引言

网络物理系统（CPS）​ 是指软件、计算设备与物理组件（如传感器、执行器）紧密耦合以实现一组目标的系统 [1]。CPS涵盖广泛领域，包括车辆、制造工厂、医疗设备、过程控制、发电配电、水务管理系统及分布式机器人 [2]。

CPS的容错围绕一个核心理念：构建一个能够检测、诊断、隔离并从故障中恢复的系统​ [3]。传统的故障检测策略基于一个基本假设：故障代表组件的物理异常，因此可通过异常输出来观测 [4, 5, 6]。原则上，故障检测方法可用于检测某些类别的网络攻击——即那些明显影响设备可用性或性能的攻击 [7]，例如拒绝服务（DoS）攻击。

然而，许多网络攻击不同于故障，因为它们是由旨在保持隐蔽的对手策划的 [5]，这使得传统故障检测失效。此类攻击包括重放攻击或时序异常攻击。CPS中最著名的隐蔽网络攻击案例是震网（Stuxnet），被视为现代网络战的里程碑。在其最终版本中，震网针对伊朗铀浓缩离心机的一个弱点——转子壁压耐受性——进行攻击。通过每月仅将转子速度操控约30分钟，震网就能缓慢损坏多台离心机。后来人们发现，该恶意软件本可造成灾难性破坏，但其设计初衷是制造缓慢、难以检测的扰动，以削弱伊朗工程师的信心 [8]。震网凸显了仅靠故障检测对CPS是不够的。

近年来，人工智能与机器人技术的进步催生了一类新型CPS：嵌入式CPS。这类系统设计为完全自主，能够更新自身目标，并与周围动态环境（包括人类用户）交互 [9]。嵌入式CPS与传统CPS的区别在于：其计算与物理组件不仅是紧密耦合的，而且是功能上相互依存的。因此，系统解释环境并采取有意义行动的能力，取决于其自身物理结构的完整性。

在传统CPS中，网络攻击可能损害可用性或功能，但形态本身并不面临固有风险。而在嵌入式CPS中，一个受损组件不仅可能禁用某项功能，还可能扭曲感知或控制，从而危及任务完成与物理完整性。形态不仅是执行手段，更是必须作为系统关键资产加以保护。

我们认为，相较于传统CPS，嵌入式CPS对网络安全弹性提出了更高要求。从可靠性角度看，嵌入式CPS必须在存在受损设备的情况下，仍能维持可用性与结构完整性。从网络安全角度看，这些系统必须将入侵检测信息整合到其弹性推理过程中。为解决这一相互作用，本研究在一个统一的弹性推理形式化框架内，架起了可靠性建模与网络安全分析的桥梁。

基于上述论点，网络安全不应被视为需单独评估的外部因素，而应作为系统运行时推理的内在组成部分。嵌入式CPS必须持续评估网络攻击不仅如何影响任务执行，还如何影响自身形态的保持。为此，本文提出一个形式化理论框架，将功能目标、形态约束、设备级角色与入侵检测系统（IDS）信号整合到一个统一的弹性评估模型中。我们的框架扩展了经典容错推理，纳入了基于IDS的可靠性评估，从而将传统可靠性分析与现代具备入侵感知的弹性建模连接起来。

I-A 贡献

本文的主要贡献如下：

• 我们形式化了嵌入式CPS在网络攻击下的弹性需求。

• 我们引入了一组弹性谓词，基于设备关键性捕捉扰动容忍度、退化阈值与缓解可行性。

• 我们提出了一个形式化理论框架，该框架虽与具体IDS实现无关，但能将IDS信息整合到运行时推理中，以评估并维持功能与形态完整性。

• 我们通过一系列引理与弹性定理，证明了系统级的合理性保证，从而实现结构化、可证明的弹性评估。

---

II. 相关工作

学者们广泛讨论了IDS对CPS的重要性。例如，Han等人 [10] 在2014年综述了将入侵检测机制集成到CPS中的进程，并概述了使IDS在CPS背景下发挥作用的一系列要求。作者认为，用于CPS的IDS应基于异常、分布式且在线（即尽可能接近实时运行）。此外，IDS应具备容错性，并避免在其分析过程中暴露任何隐私敏感数据。

近期，Segovia-Ferreira等人 [11] 综述了CPS网络弹性方法的进展。文中强调的一个重要观点是：可部署的检测方法主要分为两类。第一类是基于数据的传统方法，通过分析设备数据（采用模式识别或机器学习技术）来检测攻击。尽管此类方法能检测网络攻击，但并不适用于所有类型的网络物理攻击，因为它们未考虑底层的CPS控制模型。第二类是基于模型的检测，它考虑系统的物理模型，并将其预期输出与实际输出进行比较；如果系统行为与模型预期不一致，则假定正在进行网络攻击。得益于这种反馈控制，该类方法更适合识别网络物理攻击，但它需要一个可靠的模型。他们的观察为本文奠定了基础。我们认同Segovia-Ferreira等人 [11] 的观点，即关于网络攻击的信息并不能直接转化为CPS关于其网络物理弹性的有意义的洞察。我们的形式化框架正是解决了这一问题，弥合了网络攻击检测与网络物理弹性推理之间的鸿沟。

此后，多项工作研究了CPS中IDS的不同实现，我们列举了一些值得注意的非详尽例子。需要澄清的是，我们的工作不涉及为嵌入式CPS设计或实现IDS。相反，我们提供了一个理论框架，该框架假设IDS输出的可用性，并将其整合到一个针对嵌入式CPS的整体弹性模型中。尽管我们的框架与IDS无关，但仍有必要说明文献中已提出了此类IDS。

例如，Freitas de Araujo-Filho等人 [12] 提出了FID-GAN，一种利用生成对抗网络（GAN）和雾计算架构的无监督IDS。其边缘兼容设计，结合加速重建损失计算的编码器，使FID-GAN能够满足Han等人 [10] 提出的低延迟要求。与基线方法（如MAD-GAN [13] 和ALAD [14]）相比，其检测率也有所提高。Pinto等人 [15] 探讨了物联网（IoT）和边缘/雾计算等现代技术如何重塑网络物理生产系统（CPPS）的设计与开发过程。设备是独立开发后再集成到最终系统中的，这使得CPPS（我们认为也包括CPS）的安全性与经典信息通信技术（ICT）安全性不同。因此，他们提出了一种受生物启发的、基于异常的宿主IDS（A-HIDS），基于增量树突细胞算法（iDCA）技术，证明了其适用于边缘设备。Yan等人 [16] 给出了CPS攻击检测方法的第三个例子，他们提出了一种基于机器学习的攻击检测方案，在物理层对系统行为进行建模和监控。他们的方法基于极限学习机（ELM），使用混合特征集，包括统计描述符、基于物理的残差以及来自传感器数据的深度学习表示。虽然重点在于检测测量层面的攻击，但该工作支持了我们的假设：经过良好校准的物理层IDS可以作为更高级别推理框架的可靠输入。其他工作也提出了替代解决方案，我们建议读者参考该主题的专门综述 [10, 11, 17, 18, 19]。

Kayan等人 [20] 指出，现有文献往往过于关注孤立的IDS，忽视了架构与策略层面的漏洞。我们的工作支持他们的批评，强化了“仅靠IDS对CPS是不够的”这一观点，因为IDS仅提供了系统状态的网络安全视角。但也不应因此抛弃IDS。我们将IDS定位为专为嵌入式CPS设计的弹性框架中的一个要素，其中网络物理的耦合性要求将入侵感知紧密整合到目标关键推理中。

在CPS控制理论领域，人们提出了多种采用形式化方法的方法，用于建模安全性与网络安全 [21]。Lanotte等人 [22] 使用混合过程演算（CCPSA）形式化了网络物理攻击，建模了传感器与执行器篡改如何随时间影响系统行为。然而，他们基于攻击是否导致可观测的偏离（与标称系统相比）来评估容忍度。事实上，他们建模的IDS监控的是物理组件的运行温度。相比之下，我们的方法整合了网络安全IDS的输出，使得在可观测的退化发生之前就能进行主动调整。这使我们能够响应潜伏的或低影响的威胁，例如休眠恶意软件或早期入侵，这些威胁可能尚未影响系统输出。

Mouelhi等人 [23] 提出了一种形式化方法来建模和验证CPS弹性，其精神与我们主动的方法相呼应。使用UPPAAL时间自动机，他们的框架包含一个抽象的攻击检测机制（概念上类似于二值IDS输出），在观测到通信层恶意活动时设置一个入侵标志。该标志被用于形式化驱动向降级运行模式的转换，并包含在安全与活性属性的验证中。这种方法与我们为嵌入式CPS将基于IDS的攻击检测信号整合到网络攻击弹性建模中的做法高度一致。

---

III. 命题

本节提出两个非正式命题，用以框定我们通过形式化框架旨在实现的目标。针对每个命题，我们提供一个相关的用例示例，突显通过该形式化框架可实现的关键属性。

命题1.​ 机器人框架应能意识到它能容忍哪些扰动以及多少性能退化，这基于组件关键性与可接受性阈值。

示例A.​ 假设一个轮式机器人，配备八个摄像头和四个机械臂，设计用于在环境中导航、拾取物体并将其运输到不同目的地。这些组件是现成的物联网设备，由不同制造商分别开发，并通过中间件（例如机器人操作系统2，ROS2）集成到单一形态中。其中一个摄像头和一个机械臂被标记为关键设备，因为它们是机器人完成任务并维持形态完整性所需的最小集合。

假设一次网络攻击袭击了系统，停用了八个摄像头中的两个以及一个机械臂；然而，所有受损设备均未被标记为关键设备。直观来看，尽管机器人已受损，但仍能继续运行。虽然若所有设备正常工作，它能更高效地执行任务，但它仍能使用关键摄像头和其余功能正常的摄像头进行导航和检测物体。一旦检测到物体，机器人可以使用关键机械臂将其拾起，并可能得到其他运作中的机械臂的协助。

鉴于这些观察，尽管部分嵌入式设备已受损且无法使用，系统整体仍具备安全运行的能力。在本文中，我们将此状况称为可容忍扰动：一种形态已遭受影响部分设备的网络攻击，但未影响任何关键设备的场景。正式定义将在第V节引入。

命题2.​ 机器人框架应通过评估是否存在针对所涉受损设备的适当缓解措施并加以应用，来判断扰动与退化是否可被缓解。

示例B.​ 考虑示例A中介绍的同一轮式机器人，配备八个摄像头和四个机械臂，设计用于在环境中导航、拾取物体并将其运输到不同目的地。

假设一次网络攻击破坏了机器人，禁用了标记为关键的摄像头，连同两个非关键摄像头和一个非关键机械臂。在这种情况下，一个必需的设备无法使用，使得扰动不可容忍（δ(S)=0）；即使其他设备仍在工作，系统也无法在此状态下安全运行。

然而，机器人仍有五个功能正常的摄像头，框架判定感知流水线可以重新配置：可以将关键角色重新分配给其中一个功能正常的摄像头，从而恢复机器人的导航与物体检测能力。在此缓解措施实施后，可容忍的扰动与退化得以重建，机器人能够完全恢复任务执行。

在本文中，我们将机器人系统评估并应用此类缓解策略以恢复可容忍性的能力称为缓解可行性。我们将在第V节使用谓词 μ(S)对此概念进行形式化。

---

IV. 威胁模型与假设

我们考虑的嵌入式CPS，其设备可能成为对手通过各种网络攻击进行破坏的目标，这些攻击旨在破坏传感和驱动机制。我们提出的框架与具体的攻击类型无关，而是通过概率入侵检测函数 I(d)（定义3）来抽象地建模其影响。因此，网络攻击被表示为对设备级运行完整性的对抗性操控。

假设对手拥有部分（但非全部）系统知识，足以入侵机载设备，但无法预测后续的缓解策略。所提框架的目标是独立于任何特定的IDS实现或攻击向量，形式化地推理系统级弹性与缓解可行性。

---

V. 形式化定义

尽管第III节提出的命题在概念上直观，但仍需要一个形式化框架来实现精确且无歧义的评估。本节将引入必要的映射与谓词，以实例化命题1和命题2。

V-A 核心定义

我们考虑一个模块化机器人系统 R，由有限设备集 D={d1​,d2​,…,dn​}组成。机器人可执行有限任务集 T={t1​,t2​,…,tp​}，且必须维持有限形态相关目标集 G={g1​,g2​,…,gq​}。每个设备 d∈D通过关键性映射为任务执行与目标维持做出贡献。在以下定义中，我们使用标准符号 2D表示 D的幂集，即所有设备子集的集合。此外，我们假设所有函数和谓词都在当前时刻进行评估。为简化符号，我们在本文余下部分省略显式的时间依赖性。

本节始终遵循以下假设：

• 集合 D、T和 G在评估期间是固定的；

• 所有映射均假定正确且完备；

• 任务 t∈T是可行的，当且仅当至少有一个未受损设备以关键性 ≥1支持它；

• 目标 g∈G在相同条件下是可行的；

• 缓解措施一旦应用，将在下一个控制周期开始前生效。

我们首先引入两个基础映射，表达每个设备相对于任务执行与形态保持的关键性。

定义1（任务关键性映射 τ）。我们将任务关键性映射定义为函数：

τ:D×T→C,

其中 C={0,1,2}表示关键性等级：0表示无，1表示重要，2表示必需。

定义2（目标关键性映射 ε）。我们将目标关键性映射定义为函数：

ε:D×G→C,

其中 C={0,1,2}表示前述关键性等级。

现在我们定义另一个基础谓词，用于建模概率IDS的行为，接着定义一个将概率与置信阈值进行比较的谓词。

定义3（概率IDS函数）。令 D为嵌入式CPS中的设备集。我们将IDS输出定义为函数：

I:D→[0,1],

其中 I(d)表示设备 d∈D当前正遭受网络攻击的置信度（即估计概率）。

定义4（设备特定IDS阈值函数）。令 κbase​,κcrit​∈[0,1]为固定阈值，且满足 κcrit​<κbase​。

我们将设备特定阈值函数 κ:D→[0,1]定义为：

其中 Tactive​⊆T和 Gactive​⊆G分别是当前相关的任务和形态保持目标。

在这最后一个核心定义中，我们基于定义3和4，引入受损设备的无歧义定义。在本文中，当我们提及受损设备集 S时，指的是以下内容。

定义5（具备关键性感知的受损集）。给定IDS函数 I(d)和阈值函数 κ(d)，我们将当前受损设备集 S定义为：

S={d∈D∣I(d)≥κ(d)}

V-B 扩展定义

至此，我们提供了奠定形式化框架基础的核心定义。基于这些定义，我们现在形式化命题1，该命题涉及机器人评估扰动是否损害结构或性能完整性的能力。

定义6（可容忍扰动 δ）。我们将可容忍扰动谓词定义为函数：

δ:2D→{0,1},

该函数评估受损设备集 S⊆D是否包含任何对任务执行或目标维持至关重要的（即严格必需的）设备。

令 Tactive​⊆T和 Gactive​⊆G为当前相关的任务和形态保持目标，如定义4所述。

该谓词定义为：

仅当没有任何受损设备对任何活跃任务或目标是关键的，才满足此条件。

通过定义6，我们捕捉了扰动的二元性质，即设备要么功能正常，要么不正常：只有当没有必需设备受损时，任务才是可行的且形态得以保持。然而，仅凭这一点无法反映部分功能丧失下的退化情况。我们需要可容忍退化的概念。

为建模可容忍退化（命题1的第二部分），我们引入一个连续性能评分，并定义反映退化状态在操作上是否可行的可接受阈值。

定义7（可容忍退化 γ）。令 ψ:2D→[0,1]为一个单调退化函数，用于评估在受损设备集 S⊆D下的系统性能，其中1表示满性能，0表示完全故障。我们假设 ψ是单调非增的，这反映了额外扰动不会导致性能改善的事实。令 θcrit​,θbase​∈[0,1]为性能阈值，且 θcrit​>θbase​。

我们将可容忍退化谓词定义为函数：

γ:2D→{0,1},

该函数评估处于扰动下的系统是否仍处于可接受的性能范围内。

该谓词定义为：

γ(S)=1⟺ψ(S)≥θ(S),

其中阈值 θ(S)取决于是否存在关键设备，如下所示：

该条件的组成部分解释如下：

• γ(S)=1：性能在可接受范围内；

• θcrit​：若存在受影响的关键设备，则为严格阈值；

• θbase​：针对非关键设备扰动的宽松阈值。

  此定义捕捉了命题1的第二部分，确保机器人不仅评估其功能的可行性，还评估其在性能损失下的运行质量。值得注意的是，缓解措施在实施时，会在评估 ψ之前减少受损设备的集合。因此，它们并不违反 ψ单调非增的假设。

在我们的框架中，我们假设如果系统在任务分配和目标覆盖方面能够容忍受损集 S，那么它也必须能够满足其全局性能阈值。也就是说，如果一个系统已被归类为扰动可容忍的，那么它也必须被视为退化可容忍的。我们在以下公理中定义此假设。

公理1（扰动-退化一致性）。我们施加以下约束以确保扰动与退化谓词之间的语义连贯性：

δ(S)=1⟹γ(S)=1

我们现在形式化命题2，该命题涉及机器人确定扰动是否能被充分缓解的能力，无论是通过隔离受影响组件，还是通过部署适当的对策。

定义8（缓解可行性 μ）。令 A为符号缓解动作的集合，例如隔离受损设备、重新配置系统逻辑或将关键性重新分配给功能等效的未受损设备。令 M⊆S表示可通过此类缓解措施中和的受损设备子集。

我们将缓解可行性谓词定义为函数：

μ:2D→{0,1},

该函数评估受损集 S⊆D是否至少能被部分缓解，以恢复足够的系统可操作性。具体而言：

如果存在这样一个受损设备的子集，对其应用适当的缓解策略后，扰动与退化均变得可容忍，则该谓词返回真。

在实践中，此类缓解可以通过策略函数 ms​:D→A来实现，其中每个受影响的设备都与一个符号缓解动作相关联，例如隔离、重新配置、角色重分配或其组合。然而，谓词 μ抽象掉了策略的具体实现。它仅验证是否存在一个设备子集，对其缓解足以重建可容忍性。

V-C 正确性引理与弹性定理

我们现在建立一组形式化引理，以验证前文引入的容忍与缓解谓词的正确性。这些结果证明了该框架在扰动影响与系统弹性方面提供了一致的保证。

我们首先形式化关于任务执行的弹性概念。以下引理刻画了机器人何时能在不违反其功能目标的情况下容忍网络攻击。

引理1（δ的合理性）。如果 δ(S)=1，则对于任何任务 t∈Tactive​或目标 g∈Gactive​，S中不包含任何关键设备。

证明概要。根据 δ(S)的定义，我们有：

这意味着对于每个任务 t和目标 g，不存在满足 τ(d,t)=2或 ε(d,g)=2的设备 d包含在 S中。

因此，所有任务和目标的关鍵设备必须位于 S之外，故它们是可运行的。∎

同时，我们根据形态完整性定义弹性。以下引理捕捉了尽管存在组件级受损，机器人仍能保持结构连贯性的条件。

引理2（δ的严格性）。如果存在设备 d∈S和任务 t∈Tactive​使得 τ(d,t)=2，或者存在设备 d∈S和目标 g∈Gactive​使得 ε(d,g)=2，则 δ(S)=0。

证明概要。根据定义，δ(S)=1成立当且仅当没有任何活跃任务或目标的关键设备包含在受损集 S中。因此，如果存在设备 d∈S对某个任务 t∈Tactive​或目标 g∈Gactive​是关键设备，则 δ(S)=1的条件被破坏。因此，δ(S)=0。∎

引理1和引理2中引入的两种弹性形式并非独立。两者必须同时成立，机器人才能安全运行。下一个引理将它们联系起来，以定义组合的容忍条件。

引理3（γ的阈值跨越）。令 S⊆S′⊆D，并假设 ψ是单调非增的。那么：

如果 ψ(S)≥θ(S)，则 γ(S)=1；

如果 ψ(S′)<θ(S′)，则 γ(S′)=0。

证明概要。假设 S⊆S′⊆D且 ψ是单调非增的。

由于 ψ不会随额外扰动而增加，且 θ是基于关键设备存在性分段定义的，可能出现两种情况：

• ψ(S′)<ψ(S)而 θ(S′)=θ(S)，

• θ(S′)>θ(S)由于在 S′中包含了关键设备。

  在这两种情况下，如果 ψ(S)≥θ(S)且 ψ(S′)<θ(S′)，那么根据定义，γ(S)=1且 γ(S′)=0。∎

在当前受损集 S违反可容忍性约束的场景下，系统必须确定是否仍能通过缓解实现弹性。以下引理定义了存在此类缓解策略的条件，并使前文引入的谓词 μ(S)可操作化。

引理4（安全缓解）。如果 μ(S)=1，则存在一个缓解集 M⊆S使得：

δ(S∖M)=1且γ(S∖M)=1.

证明概要。这直接源于 μ的定义，该定义断言存在一个子集 M⊆S，通过 δ和 γ恢复可容忍性。∎

V-D 定理

我们现在将这些条件推广为系统级保证。以下定理形式化了这样一个概念：当且仅当受损设备集保持在可容忍限度内时，机器人才能安全运行。

定理1（系统弹性保证）。给定受损集 S⊆D，系统是弹性的，如果：

δ(S)=1且γ(S)=1,

或者存在一个子集 M⊆S使得：

δ(S∖M)=1且γ(S∖M)=1.

我们现在陈述主要的弹性保证：一个扰动要么直接可容忍，要么通过对受损设备子集的缓解而变得可容忍。

证明概要。本定理是引理1、2、3和4的直接应用。如果 δ(S)=1且 γ(S)=1，那么尽管存在扰动，系统仍保持结构完整性和可接受性能。如果此条件不成立，但存在一个子集 M⊆S使得 δ(S∖M)=1且 γ(S∖M)=1，则缓解恢复了可容忍性。在任何一种情况下，系统根据定义保持弹性。∎

到目前为止，我们假设机器人知道哪些设备受损。实际上，这一信息并非不言而喻，它必须来自外部来源，例如IDS。以下定理展示了在合理检测假设下，如何仍能保持系统级弹性。

定理2（基于IDS的弹性评估）。令 S为基于IDS输出 I(d)（定义3）和阈值函数 κ(d)（定义4）的当前受损设备集，如定义5所定义。

然后可以根据以下情况评估系统的弹性态势：

• 如果 δ(S)=1且 γ(S)=1，则系统在不退化的情况下容忍了扰动。

• 如果 μ(S)=1，则系统容忍了扰动，但以降级模式运行。

• 如果 δ(S)=0，则扰动不可容忍，系统必须启动安全状态缓解或停机。

证明概要。令 S表示IDS报告的受损设备集。那么我们面临三种可能的情况：

情况1：δ(S)=1且 γ(S)=1。根据定义6和7，系统无需进一步行动即具弹性。

情况2：μ(S)=1。根据定义8，系统可以通过应用缓解措施恢复足够的弹性水平。由于公理1，这意味着 δ(S)=0，因为任何满足 δ(S)=1的系统也必须满足 γ(S)=1，从而归入情况1。

情况3：μ(S)=0。根据定义，不存在可应用的缓解策略来恢复弹性条件，如同情况2，机器人被认为已无可挽回地受损。∎

表I：示例A：轮式机器人的任务与目标关键性映射

设备	角色	τ(d,TransportCube)	ε(d,AvoidCollision)	受损	κ(d)
摄像头 C1​	感知（检测、导航）	2	2	否	κcrit​=0.4
摄像头 C3​,C5​	感知（冗余）	1	1	是	κbase​=0.8
摄像头 C2​,C4​,C6​-C8​	感知（冗余）	1	1	否	κbase​=0.8
机械臂 A1​	操作（拾取、放置）	2	1	否	κcrit​=0.4
机械臂 A2​-A3​	操作（冗余）	1	1	否	κbase​=0.8
机械臂 A4​	操作（冗余）	1	1	是	κbase​=0.8

τ,ε∈{0,1,2}（0=无，1=重要，2=必需）。浅红色行表示受损设备；浅绿色行表示未受损设备。

---

VI. 评估

在上一节中，我们详细阐述了构成我们框架基础的形式化组件。在本节中，我们将对这些组件进行形式化的分析评估，首先是扰动可容忍的形态（示例A），然后是扰动不可容忍的形态（示例B）。

VI-A 示例A评估

鉴于定义1和2中关于任务与目标关键性映射的定义，我们必须丰富示例A，至少定义一个任务和一个形态保持目标。

简要回顾一下，机器人配备了八个摄像头和四个机械臂。机器人的任务如下：从点A移动到点B，拾取一个蓝色立方体，并将其带回点A。我们称此任务为 TransportCube，并将一个摄像头和一个机械臂标记为完成该任务的关键设备。作为形态保持目标，机器人必须避免任何形式的碰撞以维持其形态完整性，我们命名此目标为 AvoidCollision。为确保此目标，仅有一个摄像头被标记为关键。

根据定义3和4，我们为每个设备定义IDS阈值，以确定何时设备被视为受损。IDS的灵敏度取决于设备的关键性：它必须对关键设备上的异常反应更迅速。因此，用于关键设备的阈值 κcrit​被设定得低于用于非关键设备的基线 κbase​。表I总结了任务与目标关键性映射及其各自的IDS阈值。

我们现在证明示例A中的机器人对扰动是容忍的。为简洁起见，我们只定义了一个任务和目标，即 TransportCube和 AvoidCollision。因此，Tactive​=(TransportCube)且 Gactive​=(AvoidCollision)。该形态正遭受攻击，两个摄像头 C3​和 C5​以及机械臂 A4​被停用，导致受损设备集 S=(C3​,C5​,A4​)。

只有摄像头 C3​和 C5​涉及目标 AvoidCollision，但 S中的所有三个设备都涉及任务 TransportCube的完成。根据定义6，我们必须验证对于这些设备中的任何一个，既不满足任务关键性映射 τ(d,TransportCube)=2，也不满足目标关键性映射 ε(d,AvoidCollision)=2。从表I我们可以验证，S中每个受损设备的任务和目标关键性映射值均为1。因此，δ(S)=1，形态是扰动可容忍的。根据公理1，它也是退化可容忍的，因为 δ(S)=1⟹γ(S)=1。因此，根据定理1，系统是弹性的，并且根据定理2，它在没有任何可观测退化的情况下容忍了扰动。

VI-B 示例B评估

表II：示例B：轮式机器人的任务与目标关键性映射

设备	角色	τ(d,TransportCube)	ε(d,AvoidCollision)	受损	κ(d)
摄像头 C1​	感知（检测、导航）	2	2	是	κcrit​=0.4
摄像头 C3​,C5​	感知（冗余）	1	1	是	κbase​=0.8
摄像头 C2​,C4​,C6​-C8​	感知（冗余）	1	1	否	κbase​=0.8
机械臂 A1​	操作（拾取、放置）	2	1	否	κcrit​=0.4
机械臂 A2​-A3​	操作（冗余）	1	1	否	κbase​=0.8
机械臂 A4​	操作（冗余）	1	1	是	κbase​=0.8

τ,ε∈{0,1,2}（0=无，1=重要，2=必需）。浅红色行表示受损设备；浅绿色行表示未受损设备。

我们现在转向示例B。任务和目标和示例A中定义的相同，即 TransportCube和 AvoidCollision。受损设备集也保持不变，除了一项新增：摄像头 C1​现在受损了。此修改总结在表II中。

评估过程与示例A类似，关键区别在于受损设备中包含了一个关键设备。具体来说，摄像头 C1​被标记为对任务和目标保持都是关键的，表示为 τ(C1​,TransportCube)=2和 ε(C1​,AvoidCollision)=2。因此，根据定义6和引理2，δ(S)=0，形态不是扰动可容忍的。因此，我们必须至少评估该形态是否满足定义7中表达的退化容忍条件。

假设扰动下的系统性能为 ψ(S)=0.9，且性能阈值定义如下：θcrit​=0.85>θbase​=0.75。受损设备集 S包含至少一个关键设备，即摄像头 C1​，满足 τ(C1​,TransportCube)=2和 ε(C1​,AvoidCollision)=2。根据定义7，适用的阈值是 θ(S)=θcrit​=0.85，且 ψ(S)=0.9≥θ(S)=0.85，因此 γ(S)=1。

尽管定量性能仍在可接受范围内，但关键设备的受损违反了结构可容忍性，如定理1所示，其弹性定义要求同时满足 δ(S)=1和 γ(S)=1。由于在此场景中 δ(S)=0，我们必须验证是否存在一个缓解集 M⊆S使得 μ(S)=1（定义8），且剩余集 S∖M满足 δ(S∖M)=1。

我们假设系统配备了一种重新配置策略 mreconfig​，能够隔离受损设备并将其任务重新分配给其他类似设备。因此，mreconfig​可以隔离一个受损设备 M⊆S，并将其任务分配给板载的替代设备。在我们的案例中，M={C1​}表示系统执行 mreconfig​的能力，用另一个板载摄像头 Cn​替代关键摄像头 C1​，Cn​选自安全设备子集 {C2​,C4​,C6​,…,C8​}。

用 C2​替代 C1​会导致一种等同于表I（示例A）的情况，即没有关键设备受损。因此，δ(S)=1，并且根据定义8，μ(S)=1。缓解后，同时满足 δ(S)=1和 γ(S)=1，意味着系统成功恢复了弹性。

总之，示例A和示例B的评估共同证明了该框架的内部一致性和推理能力。当没有关键组件受损时，谓词正确地得出扰动和退化可容忍（δ(S)=γ(S)=1）的结论，确认了内在的弹性。当关键组件受到影响时，框架正确地将形态分类为非弹性（δ(S)=0），并随后验证可行的缓解措施（μ(S)=1）是否能恢复可容忍性。这些例子共同说明，所提出的形式化方法能够对设备级网络攻击下的嵌入式CPS的弹性、退化和缓解进行精确、可验证的推理。

---

VII. 未来工作

虽然所提出的框架为推理嵌入式CPS的弹性提供了理论基础，但仍需进一步的实验和评估。

首先，我们将研究如何将该框架部署到真实的嵌入式CPS上，以及这种集成能在多大程度上有效缓解网络攻击。当前框架未对IDS输出的概率性误报或漏报进行建模，我们也尚未验证其运行时可扩展性。未来的工作将通过仿真和实证研究（例如，使用Gazebo和真实机器人平台的ROS 2）来解决这些方面，在实时或模拟的IDS输出下评估谓词 δ、γ和 μ。

其次，我们将研究不同的IDS灵敏度设置和缓解策略如何影响整体弹性结果，旨在确定灵敏度、误报率和运行连续性之间的最佳权衡。

最后，我们打算探索所提出的形式化方法与新兴的安全关键CPS保证和认证标准之间的对齐，从而促进其整合到结构化的可靠性和弹性论证中。

---

VIII. 结论

本文提出了一个形式化框架，用于评估设备级扰动下嵌入式CPS的弹性。所提出的框架将经典容错推理与基于IDS的可靠性评估统一起来，推进了弹性CPS的形式化保证方法，并为未来的实证验证以及与现实机器人系统的集成奠定了基础。

通过引入可容忍扰动（δ）、可容忍退化（γ）和缓解可行性（μ）等谓词，该框架支持对嵌入式系统在存在受损组件的情况下能否继续安全有效地运行进行结构化推理。形式化引理和定理证明了模型的内部合理性，而解析示例则展示了其区分扰动可容忍与不可容忍形态以及验证可行缓解策略的能力。