由于连通性的增强，现代车辆堪比台式计算机，这一事实也延伸到了潜在的网络攻击问题。空中下载（OTA）更新是一种用于防范和缓解网络攻击的解决方案，该方案也已应用于台式机和移动电话。当前汽车领域事实上的 OTA 安全系统是 Uptane，它是为解决车辆面临的独特问题而开发的。Uptane系统需要有一种安全的更新方法，否则攻击者将会对其加以利用。为此，我们通过将 Uptane 和我们的攻击模型转换为通信顺序进程（CSP）中的形式化模型，开发了一种全面的、基于模型的安全性测试方法。将这些模型结合起来并进行验证，以生成详尽的测试用例列表，从而确定 Uptane 可能易受哪些攻击。然后，基于这些生成的测试用例，在运行 Uptane 实现的测试平台上进行安全性测试。安全性测试结果使我们能够验证 Uptane 的安全设计以及它所面临的一些漏洞。

现代车辆已经成为物联网（IoT）的一部分，将它们与用户、制造商以及世界其他部分连接起来。因此，车辆的连通性引入了网络攻击的威胁。针对联网车辆，已经发现了许多攻击方式。例如，对轮胎压力监测系统（TPMS）的攻击、对电子控制单元（ECUs）、控制器局域网（CAN 总线）的攻击、对娱乐系统（磁盘、USB 等）的攻击以及其他许多攻击。众所周知，吉普切诺基曾经存在漏洞，远程攻击者能够完全接管用户的控制权，这导致了 140 万辆车辆的大规模召回。

空中下载（OTA）更新被认为是一种很有前景的解决方案，可用于远程修补安全漏洞，避免使用昂贵且效果不佳的召回方式。传统的更新方法可以得到安全保障，因为双方都拥有相应的能力和资源。然而，汽车 OTA 更新面临一个主要挑战，即车辆不具备这些所需的能力和资源。车辆有许多电子控制单元（ECUs），每个都需要更新，但却无法处理必要的加密操作。因此，需要开发替代的软件更新解决方案来解决这个问题。自 2018 年以来，许多汽车制造商已经计划实施 OTA 更新系统。然而，OTA 更新需要具备抗攻击性，否则它将引入新的漏洞。例如，攻击者可能会用恶意软件包和勒索软件破坏固件和软件更新，这将损害车辆控制、功能以及通过跟踪车辆用户活动而损害用户隐私。因此，确保汽车 OTA 的抗攻击性至关重要。Uptane已被提出作为一种安全的汽车 OTA 标准设计，其目的是在向车辆 ECUs 交付 OTA 软件时抵御已知的攻击。尽管如此，文献中关于汽车 OTA 安全评估方法和技术的研究工作有限，特别是针对 Uptane 的研究。据我们所知，最相关的工作来自，其中 Mahmood 等人定义了一个基于半形式化模型的框架来评估 Uptane 参考实现的安全属性。他们提供了 Uptane 的非形式化模型，而攻击者则通过攻击树进行形式化建模。通过使用攻击树，Mahmood 等人生成了测试用例，但是攻击树只能捕获已知的威胁，无法应对零日攻击。此外，如何为 OTA 更新系统构建攻击树仍然是一个悬而未决的问题。

在本文中，我们提出了一种基于模型的方法，通过将 Uptane 和受 Dolev-Yao 启发的攻击模型建模为通信顺序进程（CSP）中的形式化模型。Dolev-Yao 攻击者被假设为完全控制通信，因此有能力违反机密性、真实性和完整性等安全属性。CSP 是一种用于描述并发系统的形式化建模语言。通过对这些模型进行精化检查，我们验证是否存在作为导致安全违规的系统事件轨迹的攻击。我们将每个轨迹视为一个安全测试用例，并将其转换为实际的攻击。通过这种方式，我们可以识别系统中的（甚至是零日）攻击。类似的基于模型的安全测试方法已应用于汽车安全领域，并取得了有前景的结果。他们在 CSP 中对车辆网络 CAN 总线进行了建模。该模型能够生成车辆网络在面对网络攻击时的行为方式。同样，ECU 应用程序代码可以转换为 CSP 中的形式化模型。这种模型使安全分析师能够全面且有效地识别原始代码中是否存在任何潜在漏洞。形式化模型和攻击树也被用于提出一种系统性的安全评估方法。该方法建议使用攻击树来建模攻击者的行为，然后将这些攻击树在 CSP 中形式化以生成测试用例。这展示了这种方法如何应用于汽车蓝牙接口的案例。然而，其局限性包括：（i）攻击树中捕获的所有攻击都是已知的；（ii）没有车辆模型来驱动测试用例生成过程。

1.1 贡献

我们在本文中的贡献是：（i）一种用于评估 Uptane 的基于模型的方法；（ii）Uptane 在 CSP 中的形式化模型；（iii）Uptane 模型的一个变体；（iv）受 Dolev-Yao 启发的攻击的形式化模型；（v）一种全面生成安全测试用例的方法；（vi）对 Uptane 参考实现的严格安全评估。尽管这种方法最初被引入，但它在几个方面存在局限性：（i）Uptane 模型是有限的，不包括次级 ECU。通过包含次级 ECU，该模型现在具有完整验证和部分验证，以及攻击者无法控制的内部网络。这提供了更多的攻击点可供发现，并使模型更符合规范。（ii）攻击模型仅包括三种攻击。为了解决这个问题，我们又添加了两种攻击，即欺骗攻击和冻结攻击。欺骗攻击可以向车辆发送恶意图像，而冻结攻击允许攻击者阻止更新。这在规范中被提及为需要防御的内容，但我们将测试该模型并考虑模型变体。（iii）缺乏通过精化检查自动生成测试用例的机制，导致仅生成 3 个测试用例。为了解决这个问题，我们创建了一个 Python 脚本来搜索模型中同一攻击者的更多攻击点，从而更好地发现模型中的攻击。（iv）此外，我们添加了 Uptane 模型的一个变体。这个变体模型移除了对冻结攻击的防御。这使我们能够查看实际的 Uptane 实现是否遵循了规范：如果没有，它可能容易受到这种攻击。

1.2 结构

本文的结构如下。第 2 节概述了 CSP 和攻击模型，它们为所提出的方法提供了基础。此外，还回顾了 Uptane 的结构和逻辑。第 3 节介绍了该方法及其在 Uptane 系统中的应用。第 4 节描述了我们如何在 CSP 中对 Uptane 进行建模。第 5 节介绍了攻击模型、Uptane 的变体模型以及如何使用 FDR 生成详尽的测试用例列表。第 6 节介绍了实验、其实验设置以及我们如何将测试用例转换为实际攻击。最后，第 7 节对本文进行了总结，并强调了有待改进的方面。

在本节中，我们回顾了用于建模和测试用例生成的 CSP 和故障 - 发散精化（FDR）。此外，我们还讨论了攻击模型的使用。

2.1 CSP 和 FDR

我们在这里简要概述本文中使用的 CSP 子集。更完整的介绍可以找到。给定一组事件∑，下面使用的 CSP 进程由以下语法定义：

其中 A，B⊆∑且 aᵢ∈A。为方便起见，通过上述语法定义的 CSP 进程集合表示为 CSP。术语 e!x?y 表示在 e x 的通信中与环境通信，并且变量 y 由环境实例化。进程 Stop 是最基本的进程，它不参与任何事件，代表死锁。RUN (A)=?x:A→RUN (A) 是这样一个进程，对于事件集 A⊆∑，它总是可以通信环境期望的 A 中的任何成员。前缀 e→P 指定一个进程，该进程只愿意参与事件 e，然后表现为 P。外部选择 P₁□P₂表现为 P₁或 P₂。广义外部选择□aᵢ:A@P (aᵢ) 向环境提供 A 中的任何动作，然后表现为 P (aᵢ)。条件 if b then P else Q 在 b 为真时表现为 P，否则表现为 Q。广义并行运算符 P₁||P₂要求 P₁和 P₂在 A∪{√} 中的事件上同步，其中√是用于标记进程终止的特殊事件。所有其他事件独立执行。字母化并行 P₁[A||B] P₂必须在 A∩B 中的任何事件上同步。两个进程都可以参与该交集之外的事件。P (X) 表示递归。CSP 进程有不同的语义模型。就本文而言，我们回顾有限轨迹语义。轨迹是来自∑^√=∑∪{√} 的可能为空的事件序列。通常，进程 P 的轨迹语义是（∑^√）* 的子集 traces (P)，由该进程可能表现出的所有轨迹组成。关于轨迹的更多细节和完整定义可以找到。如果 traces (P)⊆traces (Q)，则称进程 P 轨迹精化进程 Q（记为 Q⊑ᵀP）。故障 - 发散精化 4（FDR4）是 CSP 的精化检查器。FDR4 可用于调试 CSP 脚本，以及从 CSP 模型生成测试用例。

2.2 攻击模型

本文采用的攻击模型受 Dolev-Yao 的启发。Dolev-Yao 攻击模型被认为是最强大的攻击模型之一]。它已被广泛用于提供安全协议的形式化证明，并指导系统实现的安全测试。在 Dolev-Yao 攻击模型中，攻击者控制网络，允许攻击者操纵通过网络发送的所有数据包（如果没有适当的防御措施）。

我们的攻击模型包括五种攻击：编辑攻击、阻塞攻击、监听攻击、欺骗攻击和冻结攻击。编辑攻击可以操纵网络上发送的数据包。阻塞攻击会阻塞网络上的数据包，最终可能导致完全的拒绝服务。监听攻击（即窃听）会监视网络上发送的内容。欺骗攻击模仿合法来源，使受害者认为它正在与预期的接收者进行交互。冻结攻击通过向受害者发送当前安装的更新来阻止其更新，这导致受害者停留在当前更新状态。我们的攻击模型中的这种划分旨在提供每个生成的测试用例的性质。这避免了形式化模型状态空间的爆炸，从而促进 FDR4 中的精化检查并减少生成测试用例的时间。

2.3 Uptane 系统

Uptane系统的结构如图 1 所示。服务器端包括导演服务器、图像仓库服务器和时间服务器。导演服务器检查系统的元数据并持有清单。图像仓库是导演服务器的简化版本。当图像仓库收到角色请求时，它从存储中获取角色元数据，然后将其发送到主 ECU。时间服务器持有当前时间，以更新任何没有时钟的 ECU。在车辆内部（即客户端），Uptane 系统由一个主 ECU 和多个次级 ECU 组成。

图1.Uptane系统。发送的消息有：1和2图像；3签名令牌和时间；4元数据和图像；5车辆宣言；6元数据、图像和宣言

主 ECU 负责与服务器通信以接收时间、固件和元数据。服务器将处理主 ECU 发送的清单，并在有新更新时做出响应。通常，次级 ECU 的计算能力有限，因为它们是为特定任务设计的。因此，在 Uptane 系统中，它们不与服务器直接通信。次级 ECU 与主 ECU 通信以接收新更新。为了验证更新，系统利用元数据。元数据分为四个角色：root、timestamp、snapshot 和 targets。所有角色都遵循相同的结构，包含角色非特定数据（版本和过期时间）、唯一有效负载和签名。Root 的有效负载包含每个角色的公钥。Timestamp 的有效负载包含 snapshot 文件名和 snapshot 版本。Snapshot 的有效负载包含 targets 文件名和 targets 版本。Targets 的有效负载包含图像名称和 ECU ID。对角色进行测试以验证其完整性和合法性。验证方法包括 7 个步骤。如果任何步骤失败，验证系统将停止，并且不会安装更新。这 7 个步骤是：①从存储加载当前元数据；②向服务器（导演或图像仓库）发送角色元数据请求；③使用私钥解密收到的元数据中的签名；④从解密的签名验证有效负载的合法性；⑤确保新元数据版本高于旧元数据版本；⑥检查当前时间是否低于新元数据的过期时间；⑦一旦元数据验证通过，安装新固件。

在本节中，我们介绍用于 Uptane 安全评估的方法。首先，创建汽车 OTA 系统和攻击的形式化模型。然后，我们将这些模型结合起来，通过精化检查生成测试用例。这是形式化建模和渗透测试的结合，创造了一种严谨且更具成本效益的方法来识别系统中的潜在漏洞。该方法包括 7 个步骤，如图 2 所示。步骤①和 ③可以同时进行，而所有其他步骤必须按顺序进行。

图2.Uptane的安全测试方法：1正式化Uptane；2、对Uptane模型进行突变；3模拟攻击；4组合模型；5生成符号测试用例；6翻译符号测试用例；7执行测试用例；8报告测试结果

①Uptane 形式化：我们构建 Uptane 系统的模型。通常采用自底向上的方法，首先对 Uptane 系统的组件进行建模，然后将这些组件组合起来以捕获整个系统的行为。

②Uptane 模型变体：通过移除一些安全特性来改变 Uptane 模型。例如，如第 5.2 节所述，移除防止冻结攻击的时间检查。这些移除允许我们生成可以检查 Uptane 实现中相应安全特性的测试用例。

③攻击建模：然后我们在 CSP 中构建攻击模型。我们对阻塞、窃听、冻结、欺骗和编辑攻击的行为进行建模。

④模型组合：在这一步中，我们将 Uptane 模型和攻击模型结合起来，以表示一个受攻击的系统。通常，这是通过将网络模型替换为攻击模型来完成的。这反映了网络已被攻陷，攻击者完全控制网络。

⑤生成符号测试用例：在这一步中，使用轨迹精化来生成测试用例。然而，我们首先捕获没有攻击的安全行为。我们在 FDR4 中检查它们是否被 Uptane 的受攻击模型精化。如果不是，则生成反例并将其用作符号测试用例。

⑥符号测试用例转换：然后，我们使用 Ettercap  将生成的符号测试用例转换为可执行的测试用例。

⑦执行测试用例：然后在 Uptane 实现上测试转换后的攻击。

⑧测试用例报告：我们获取攻击结果并制定测试报告。

本节描述我们如何使用 CSP 创建 Uptane 系统的模型。由于 Uptane 规范的复杂性，模型的范围限于：导演服务器、图像仓库、主 ECU、次级 ECU、元数据的验证过程以及固件和清单的发送。Uptane 模型分为三个进程：服务器、无线网络和车辆，如图 3 所示。下面我们讨论构成模型基础的数据类型、通信网络模型、包括主 ECU 和次级 ECU 的车辆模型以及包括角色、清单和验证系统的服务器模型。

图3.Uptane模型显示服务器、网络和车辆之间的连接

在我们的方法中，我们将 Uptane 模型限制为一个更新周期。这样做的理由是为了管理模型的复杂性。如果没有这个限制，通过向模型添加多个更新周期，生成测试用例所需的运行时间将呈指数增长。完整的 Dolev-Yao 模型将允许所有攻击同时发生，这需要不止一个更新周期。因此，将受 Dolev-Yao 启发的攻击模型拆分为单独的攻击与 Uptane 模型的单更新周期限制相适应。然而，这使我们无法处理组合多个简单攻击的复杂攻击。我们将其留作未来的工作。

4.1 数据类型

我们为模型中的事件和进程定义了以下数据类型：Roles（值为 root、timestamp、snapshot 和 targets）；公钥和私钥（分别标记为 Pkey 和 Skey）；ECU ID（一个主 ECU 和一个次级 ECU）；文件名（用于角色元数据）；图像名称（当前图像、新图像和用于攻击的坏图像，见第 5.1 节）；文件名元数据对，由文件名和版本号组成，用于捕获车辆 ECU 的存储结构；组件（图像仓库、导演、主 ECU、次级 ECU 和攻击者）；消息（元数据请求、包含元数据的响应）。

4.2 角色元数据

角色元数据结构包括其版本、过期时间、有效负载和签名，如图 4 所示。版本和过期时间的范围从 1 到 3，分别代表过去、现在和未来。角色元数据的唯一有效负载通过序列建模以容纳多组元数据。timestamp 是个例外，它只包含一组元数据。Root 的属性是角色和 Pkey。Timestamp 包含 snapshot 文件名、版本和哈希。Snapshot 包含 targets 文件名和版本、targets 属性以及图像名称、ECU ID 和哈希。有效负载只能是一组功能性有效负载，这显著减少了模型输出。有效负载也可以是 “Junk”。如果有效负载是无用信息，更新将被取消。有效负载签名是使用 SKey 和角色的有效负载计算的。

图4.角色元数据内容：固件版本、元数据过期时间、元数据的唯一有效载荷和签名

4.3 通信网络建模

网络包含三个主要部分：发送元数据、发送清单和发送更新状态。每个部分都有一个发送通道和一个接收通道，定义为：“channel Send:Component.Component.Message”“channel Recv:Component.Component.Message”。发送通道的第一个组件是发送者，第二个是目的地。接收通道的第一个组件是接收者，第二个是发送者。网络建模为 “Network (X) = □a1:X,a2:X@Send.a1.a2?m→Recv.a2.a1.m”，它接收发送消息并将其转换为接收消息，同时交换发送和接收组件的位置参数。

4.4 车辆建模

本节描述主 ECU、次级 ECU 的模型及其相关功能。图 5 显示了 Uptane 模型在车辆侧的层次结构。图的左分支显示了为主 ECU 的组件和功能建模的进程。我们在 4.4.1 节中提供更多建模细节。图的右分支显示了为次级 ECU 的组件建模的进程，4.4.2 节中有更多细节。

图5.Uptane模型中的车辆层次结构，显示主ECU和辅助ECU的存储和功能

4.4.1 主 ECU

主 ECU 由一个递归进程建模。图 6 显示了用于主 ECU 的 CSP 代码。首先，该进程基于次级 ECU 的清单和自身的清单创建车辆清单（第 2 和 3 行）。将其发送到导演服务器（第 4 行）。导演服务器的响应通知主 ECU 车辆是否需要更新（第 5 至 6 行）。这开始了 4.4.3 节中描述的角色验证过程，从导演服务器和图像仓库请求并验证所有角色的元数据。完成后，车辆将进行更新。

图6.主ECU功能的CSP模型

4.4.2 次级 ECU

次级 ECU 的建模首先是从次级存储中获取其清单，然后将其发送到主 ECU。这可以在图 7 的第 2 和 3 行中看到。主 ECU 将响应次级 ECU，告知其是否需要更新（第 4 和 5 行）。如果次级 ECU 需要更新，它将请求目标元数据并进行部分验证。部分验证仅检查目标的元数据，如果成功则接受更新（第 8 至 11 行）。

图7.辅助ECU功能的CSP模型

4.4.3 角色验证

每个验证过程都从请求角色元数据开始。这由图 8 第 3 和 4 行的 CSP 代码编码。收到元数据后，验证过程将检查公钥是否与私钥匹配，如第 5 至 7 行所编码。接下来是验证新元数据中的版本号是否高于已安装的版本，如第 9 和 10 行所编码。然后系统将检查当前时间是否小于新元数据的过期时间，如第 12 至 14 行所编码。检查完成后，角色元数据将更新为新版本，如第 16 和 17 行所编码。如果任何验证步骤失败，更新将停止。

图8.Uptane元数据验证的CSP模型

4.5 服务器建模

服务器有两个组件和两个存储系统。为了简化系统，时间服务器已从模型中抽象出来。服务器内的两个主要组件是导演服务器和图像仓库。还有角色元数据存储和清单存储，其中清单存储仅由导演服务器使用。图 9 显示了 Uptane 模型在服务器侧的层次结构。下面，我们更详细地解释 Uptane 模型在服务器侧的情况。

图9.Uptane模型中的服务器层次结构，显示元数据存储、映像和控制器存储库之间的连接，以及每个存储库的内容功能

4.5.1 角色元数据存储

当主 ECU 请求更新时，导演服务器和图像仓库会调用角色元数据存储。角色元数据存储显示为一个单一实体，但实际上它是四个独立的存储系统，每个角色一个。每个存储系统都包含版本、过期时间、唯一有效负载和签名。

4.5.2 清单存储

服务器清单存储是导演服务器独有的，因为图像仓库不需要调用清单存储。清单存储中包含来自主 ECU 和次级 ECU 的最新 ECU 清单。每个 ECU 清单将包含 ECU ID 和图像名称。这与车辆中的清单存储相同。

4.5.3 导演服务器和图像仓库

图 10 显示了编码导演服务器和图像仓库循环的 CSP 代码。导演服务器循环由第 1 至 15 行的 CSP 代码建模；图像仓库循环由第 17 至 19 行建模。服务器从导演服务器开始。收到主 ECU 的清单后，导演服务器将其与当前持有的清单进行比较，检查是否为最新。这在第 2 至 6 行中编码。导演服务器将向主 ECU 通知其更新状态，是最新的还是过时的，如第 7 行所示。主 ECU 将向导演服务器和图像仓库请求元数据和更新，这些服务器在收到请求后发送数据。满足所有请求后，更新周期完成，导演服务器的第 11 至 16 行和图像仓库的第 18 和 19 行。

图10.控制器和图像存储库主要功能的CSP代码示例

4.6 模型集成

为了正常运行，系统需要同步。通过将两个操作并行运行来实现这一点。通过这种方法，我们连接了服务器、车辆和网络的所有组件。这就得到了我们的同步 Uptane 模型。

本节讨论攻击及其在第 5.1 节中的模型中的实现，在第 5.2 节中通过变异模型生成更多测试用例。第 5.3 节和第 5.4 节涵盖了从这些变异中生成详尽的测试用例列表。

5.1 攻击建模

在本节中，我们对 2.2 节中提到的五种攻击进行建模，并将它们集成到 Uptane 模型中。每个攻击模型都替换了 Uptane 模型中的网络，并从受攻陷网络的外部攻击角度对系统实施攻击。

5.1.1 阻塞攻击

阻塞攻击可以在图 11 的第 1 和 2 行中看到。在第 2 行，阻塞攻击将接收要发送的消息，但不发送它们，因为它调用自身并重新开始进程。阻塞器不使用网络用于传递消息的 “Recv.a2.a1.m”，从而阻止模型发送消息。

图11.CSP攻击模型：阻止、窃听、冻结、欺骗和使用密钥编辑

5.1.2 窃听攻击

窃听攻击将接收每条消息，并将其传递到预期目的地以及攻击者。这在受攻陷的网络上创建了一个一进二出的流程，攻击者接收发送的每条消息。窃听攻击可以在图 11 的第 3 和 4 行中看到。第 4 行是窃听者在将所有流量发送到预期接收者之前发送给攻击者的地方。

5.1.3 冻结攻击

冻结攻击中断更新，并向车辆发送一个签名正确但过时的更新。这会阻止车辆更新，即使存在较新的更新。在图 11 中，冻结攻击在第 5 至 8 行，第 6 和 7 行显示攻击正在查找元数据和更新。找到后，它发送旧更新。如果没有发送元数据，它将像正常网络一样运行，允许消息不受影响地发送，如第 8 行所示。

5.1.4 欺骗攻击

当服务器通知车辆有更新时，欺骗攻击将回复车辆，告知其已经是最新的，从而阻止任何更新。这种攻击可以在图 11 的第 9 至 11 行中看到。在第 10 行，攻击会查找车辆请求是否需要更新，然后通知其已更新（使用专用消息 “Fine”）。“Fine” 用于通知车辆，无论其当前更新状态如何，它都是完全最新的。第 11 行允许攻击在所有其他情况下像正常网络一样运行。

5.1.5 带密钥和不带密钥的编辑攻击

我们将编辑攻击分为两种，一种带密钥，一种不带密钥。两者的过程相似，但带密钥的编辑攻击多一个步骤。编辑攻击可以在图 11 的第 12 至 15 行中看到。在第 13 行，编辑攻击检查消息是否符合其标准，标准是：此消息是否包含更新？如果消息不发送更新，攻击将像网络一样运行，如第 15 行所示。如果消息包含更新，攻击将把消息转换为接收消息。然后，它将更新替换为带有验证恶意更新的密钥（标记为坏密钥）的恶意更新。不带密钥的编辑攻击是相同的，但不替换密钥或签名，保留合法更新的签名和密钥。

5.1.6 受攻击模型

在 4.3 节中，我们讨论了如何连接各个组件。对于 5.1 节中创建的 5 种攻击，组合它们的方法是相同的：用我们的一种攻击替换网络。这形成了 6 个受攻击的 Uptane 模型：窃听 Uptane、阻塞 Uptane、冻结 Uptane、欺骗 Uptane、带密钥的编辑 Uptane 和不带密钥的编辑 Uptane。

5.2 Uptane 模型变异

第 4 节中讨论的 Uptane 模型使我们能够在 Uptane 系统的实际实现上测试攻击。我们的模型假设实现完全合规，即所有检查和验证都已实现。然而，如果实现未完全遵守规范，可能会引入一些漏洞。这意味着 Uptane 模型和攻击模型生成的安全测试用例将无法检测到这一点。原因是我们的模型编码了 Uptane 规范的所有防御措施。如果实现遗漏了其中一项，将没有生成测试用例来检查这些漏洞。为了测试可能因偏离规范而引入的漏洞，我们使用变异模型。

为了测试这一点，我们创建了移除防御措施的模型变体。这会基于变异生成测试用例，使我们有机会检查实现是否存在与每个变异相关的漏洞。Uptane 规范记录了它可以防止的攻击。在我们的 Uptane 模型中找到相关攻击并移除防御措施，就得到了一个变异模型。然后使用相同的攻击模型测试这个变异模型，看看变异是否给我们带来了更多测试用例。然后，我们基于新的测试用例创建新的攻击，并在实现上进行检查。该检查评估合规性以及可能由此引入的任何漏洞。

特别是对于冻结攻击，Uptane 模型已被修改，使其在元数据验证过程中不再检查当前时间。这可以在 4.4.3 节和图 8 的第 12 至 15 行中看到。验证过程通过检查时间来确保更新确实是最新的而不是过时的，以此来检查冻结攻击。这里考虑的变异在每个验证步骤中移除了这个检查，不再需要时间检查。这使得模型容易受到冻结攻击。模型的所有其他方面保持不变。对导演服务器和图像仓库的 root、timestamp、snapshot 和 targets 验证的时间检查是此变异仅有的更改。使用变异模型，我们将生成测试用例，以验证 Uptane 的实现是否确实容易受到冻结攻击。

我们发现的模型的其他变异是进行部分验证而不是完全验证。这意味着即使系统是最新的，它们也只会从导演服务器更新，并进行部分验证和更新。

5.3 使用精化检查生成安全测试用例

为了从受攻击模型生成测试用例，我们首先定义什么是成功的攻击，以便我们能够识别系统何时被攻破。

如果攻击者收到任何消息，则窃听攻击成功，当传输 “Recv.attacker” 消息时就证明了这一点。如果接收者没有收到任何消息，则阻塞攻击成功。这意味着没有 “Send” 消息被转换为 “Recv” 消息。在这种模式下，如果版本保持不变，则冻结和欺骗攻击成功。如果次级 ECU 收到恶意更新，则编辑攻击成功。通过添加检查恶意固件的 if 语句，运行 “do_bad_thing” 行为表示攻击成功。这些定义构成了我们的精化检查：分别为 NoEaves、NoBlock、NoFreeze、NoSpoof 和 NoEdit。

5.3.1 精化检查

FDR4 中的精化检查采用一个进程，在我们的案例中是攻击失败的情况。然后将其与另一个进程（在我们的案例中是受攻击模型）进行比较。FDR4 使用这种比较按顺序探索进程的状态。如果发现反例，精化将停止，然后报告轨迹（或攻击）。

精化检查（即断言）允许我们检查 5.3 节中定义的安全属性是否得到满足。如果系统容易受到攻击，针对受攻击系统的精化检查将失败。在这种情况下，每个失败都有一个反例作为证据，并被视为一个测试用例。我们将使用精化检查来生成安全测试用例。每个精化具有以下形式：“SecurityProperty⊑ᵀCompromisedSystem”，其中 SecurityProperty 和 CompromisedSystem 进程分别对应于每个攻击。特别是，我们使用 FDR4 来检查以下精化，见图 12，以检查 Uptane 系统是否能抵御：1 窃听攻击、2 阻塞攻击、3 带密钥的编辑攻击、4 不带密钥的编辑攻击、5 欺骗攻击和 6 冻结攻击。

图12.攻击细化检查：窃听、阻止、用密钥编辑、不用密钥编辑、欺骗和冻结

例如，在窃听攻击的情况下，SecurityProperty 是 “NoEaves”，CompromisedSystem 是 “Eaves_Uptane”，以检查 Uptane 系统是否能抵御窃听攻击。FDR4 用于生成检查精化的测试用例。

5.4 详尽的测试用例

每个攻击可能有多个成功渗透系统的点。为了发现模型中的更多攻击点，我们开发了一个 Python 脚本来允许 FDR4 测试第一次成功攻击之外的情况。为了将 FDR4 与 Python 结合使用，我们需要使用 Python 2.7，因为这种集成在 Python 3 中不可用。首先，我们在 Python 中创建一个脚本，在 FDR4 中启动一个会话，该会话被赋予受攻击的 Uptane 模型。FDR4 完成后，如果攻击成功，它将输出轨迹。如果攻击失败，则不会发送轨迹，也不会有更多可能的攻击。对于成功的攻击，Python 脚本将创建一个文件来存储轨迹，然后附加该轨迹以符合 CSP。这是通过在开头添加 “TCn = ''” 来实现的，其中 “n” 随着每个新轨迹而增加。我们还在每个进程的末尾添加前缀 “→”，并在末尾添加 “→RUN (Events)” 进程以实现这种一致性。这个 CSP 轨迹是我们的反例，然后将其添加到 Python 使用的断言中。这阻止了相同的攻击再次被标记，从而允许发现更多攻击。查看 Python 使用的进程，“assert SecurityProperty□TCX⊑ᵀCompromisedSystem”，我们可以看到所使用的攻击显示为 “SecurityProperty”。这表示如果没有攻击或攻击失败，应该发生什么。生成的反例被导入到 “TCX” 所示的断言中，每发现一个反例，就会有一个新的 “TCX”。然后，我们在 “CompromisedSystem” 所代表的受攻击模型上对其进行测试。

使用这种方法，我们从正常的 Uptane 模型中生成了 23 个测试用例：18 个用于窃听、1 个用于阻塞、0 个用于冻结、2 个用于欺骗、2 个用于带密钥的编辑，0 个用于不带密钥的编辑。生成的 23 个测试用例表明 Uptane 系统容易受到其中一些攻击。容易受到列出的攻击可能会阻止车辆更新、逆向工程发送的更新，甚至安装恶意固件以进行破坏性攻击。

在本节中，我们基于上一节生成的测试用例对 Uptane 参考实现进行安全评估。这些测试用例被手动转换为现实世界的攻击，在运行 Uptane 实现的物理测试平台上进行测试。测试（即攻击）首先使用 Ettercap 在网络上执行地址解析协议（ARP） poisoning，使所有数据包都通过测试机（即攻击者）。然后，通过定义合适的 Ettercap 过滤器，使用 Ettercap 来操纵这些数据包。

6.1 测试平台

Uptane 参考实现在物理测试平台中实现，包括：两台运行 Raspbian 的树莓派 4，分别作为主 ECU 和次级 ECU；一台运行 Ubuntu 的笔记本电脑作为服务器；另一台运行 Kali Linux 的笔记本电脑作为测试机。所有组件通过以太网连接到一个路由器，作为允许它们通信的网络。为了监控系统和攻击，服务器和攻击者运行 Wireshark，这是一个 packet sniffing 工具，显示通过给定网络的所有流量。

6.2 测试用例 1 至 18 - 窃听攻击

图 13 显示了窃听测试用例的轨迹。第 3 行显示黑客已收到通过网络发送的消息。这种攻击是成功的，我们可以使用此轨迹将其转换为现实世界的攻击。这些测试用例被转换为一个可执行的测试用例，包括两个步骤：（i）使用 Ettercap 设置一个监听器，以查看发送的所有消息；（ii）从次级 ECU 请求更新。执行这两个步骤后，Ettercap 可以看到在两者之间传递的数据包，包括固件更新。Ettercap 拦截的数据包与主机上 Wireshark 收集的数据包正确对应。因此，攻击成功。

图13.窃听攻击生成的反例跟踪

6.3 测试用例 19 - 阻塞攻击

图 14 将第 2 行标识为与阻塞 Uptane 模型的差异。这表明未收到此消息。使用此轨迹，我们可以将攻击转换为现实世界的攻击。测试用例 19 包括两个步骤：（i）在 Ettercap 中设置一个阻塞过滤器；（ii）请求更新。Ettercap 的过滤器有很多应用，其工作方式与大多数脚本语言非常相似。该过滤器调用两个命令 “kill ();drop ()”。kill 命令结束连接并阻止数据包到达目的地。执行这两个步骤会导致 ECU 看起来没有响应，并最终发送连接超时错误。主机上的 Wireshark 也证实数据包被阻止：尽管仍在发送 TCP 重置数据包以尝试重新建立连接。因此，攻击成功。

图14.块测试用例提供的示例跟踪

6.4 测试用例 20 和 21 - 欺骗攻击

图 15 显示了测试用例 20 的轨迹。第 10 行显示导演服务器发送 “Update” 消息，但在第 11 行，收到的消息显示为 “Fine”。这阻止了车辆更新。使用此轨迹，我们可以将此攻击转换为测试平台的现实世界攻击。欺骗攻击包括以下步骤：（i）记录服务器在车辆最新时的响应；（ii）创建一个过滤器来发送此响应而不是合法响应；（iii）请求更新。然而，这与 6.6 节中的冻结攻击有许多相同之处。攻击未成功，我们发现我们所使用的实现与规范存在差异。

图15.恶搞测试用例提供的示例跟踪

6.5 测试用例 22 和 23 - 带密钥的编辑攻击

在图 17 中，第 3 至 6 行显示导演服务器向主 ECU 发送带有 “Image_new” 的更新有效负载，但在接收端，第 7 至 10 行显示图像已被替换为 “Bad_Image”。利用此轨迹，我们可以将模型理论上的攻击转化为现实世界的攻击。测试用例 22 和 23 包含三个步骤：（i）创建图像仓库和导演服务器的恶意目标元数据二进制文件；（ii）在网络上应用 Ettercap 过滤器以更改传输中的固件图像，见图 16；（iii）请求更新。首先，过滤器检查数据包中是否存在导演服务器和图像仓库加密目标有效负载开头的字符串（第 1 和 3 行）。接下来，我们丢弃数据包中的信息（第 2 和 4 行的第一个语句），然后注入恶意有效负载（第 2 和 4 行的第二个语句）。第 5 行用恶意更新替换良性更新。主 ECU 和次级 ECU 均未显示受到攻击的迹象；次级 ECU 的文件显示 “BadXX 固件图像” 作为当前更新。因此，该攻击在测试用例所识别的两个方面均成功。

图16.Ettercap过滤器实现按键编辑攻击

图17.这是FDR中与按键编辑相关的跟踪

6.6 变异测试用例 24 和 25 - 冻结攻击

将测试用例 24 和测试用例 25 转化为可执行攻击需要 5 个步骤：（i）使用 Ettercap 监听并记录服务器到车辆的元数据和更新；（ii）创建一个过滤器，将此更新注入到新的更新和元数据中，替换预期消息；（iii）在系统下次更新前进行 ARP 毒化；（iv）激活过滤器；（v）执行更新。这种攻击与图 16 中的攻击类似，但它注入的是记录的旧元数据和更新，而不是恶意的。然而，实施此攻击时，攻击失败，并向车辆反馈更新已过期，可能存在潜在攻击。这些测试用例由变异模型和冻结攻击模型生成。测试结果表明，Uptane 的实现确实能够抵御冻结攻击。

在本文中，我们扩展了我们提出的用于系统评估汽车 OTA 更新的基于模型的方法。该方法采用 CSP、FDR4、简化的 Dolev-Yao 攻击者和变异建模来枚举潜在攻击。通过结合 Uptane 和攻击的 CSP 模型，我们测试了 Uptane 对理论攻击的抵御能力。通过这种方法，我们在 Uptane 系统上测试了五种攻击，生成了 25 个测试用例来识别漏洞。我们展示了一种有前景的方法，可以系统地测试 OTA 系统，允许在实际实现上进行大量的安全测试。在模型和攻击的范围内，我们可以得出结论，Uptane 容易受到其中一些攻击。容易受到所列攻击可能会阻止车辆更新、逆向工程发送的更新，甚至安装恶意固件以实施破坏性攻击。

为了帮助防范三种成功的攻击 —— 带密钥的编辑攻击、阻塞攻击和窃听攻击 ——Uptane 可以采取以下措施。（i）带密钥的编辑攻击：为防止此类攻击，我们可以采用更好的密钥管理，防止密钥泄露，并进行定期更新。（ii）阻塞攻击：在这种情况下，无法防止这种攻击。为了更好地应对潜在的阻塞攻击，车辆可以定期与服务器联系。例如，通过每天与服务器联系一次，车辆可以确定失去联系的时间。利用这一点，制造商可以确定在车辆向用户发送无法与服务器联系的消息之前，允许多长时间失去联系。这可以告知用户前往修理厂检查车辆的完整性。（iii）窃听攻击：这种攻击无法阻止，但可以使其几乎无用。通过仅在服务器和主 ECU 之间采用强加密，攻击者无法看到传输的内容，从攻击中获得的信息很少。尽管这需要主 ECU 配备更好的硬件，但制造商可以为其他次级 ECU 保留相同的硬件。Uptane 系统已显示出对某些攻击的抵御能力，但也暴露出各种漏洞。该实现还包含了一些改进规范的变更，防止了原始的简单欺骗攻击的发生。

未来的工作将通过添加更多攻击和相同攻击的变体来扩展模型。我们还计划通过移除和包含原始模型的各个方面来创建更多模型变异。这将生成更多测试用例，并对该汽车 OTA 系统进行更全面的安全评估。除了向模型添加更多内容以生成更多测试用例外，我们还打算测试 Uptane 模型的防御措施。通过向模型添加建议的防御措施，我们可以测试相同的攻击在模型上是否仍然成功，从而使模型能够用于测试建议的防御措施。

Uptane 旨在使汽车行业能够满足新兴标准（如 ISO/DIS 24089 关于道路车辆软件更新工程）和法规（如 UNECE WP29 R155 和 R156 关于汽车系统的 cybersecurity 和软件更新管理）的要求，这些标准和法规最终要求车辆具备安全的 OTA 软件更新系统。我们的贡献提供了一个框架，通过该框架，可以确保 Uptane 的实现（在车辆之间可能在较低级别有所不同）使用有效的测试用例生成。因此，虽然形式化模型足以表示更新系统的逻辑架构，但生成的测试用例最终将测试实现；增加模型变异将确保测试用例有助于进行越来越全面的评估。