#! https://zhuanlan.zhihu.com/p/613033567
# 论文阅读：Femto-Containers 轻量级虚拟化和故障隔离，为低功耗物联网微控制器上的小型软件功能提供支持

> 本文来自 eunomia-bpf 社区，我们正在探索 eBPF 和 WebAssembly 相互结合的工具链和运行时: <https://github.com/eunomia-bpf/wasm-bpf> 社区关注于简化 eBPF 程序的编写、分发和动态加载流程，以及探索 eBPF 和 Wasm 相结合的工具链、运行时和运用场景等技术。

在物联网微控制器上使用的低功耗操作系统运行时通常提供基本的API、基本的连接性和（安全的）固件更新机制。相比之下，在不受限制的硬件上，网络软件已进入了无服务器、微服务和敏捷性时代。**为了弥合这一差距**，我们在论文中设计了 Femto-Containers，这是一种新的中间件运行时，可以嵌入到异构低功耗物联网设备中。Femto-Containers 使得**在低功耗物联网设备上通过网络安全地部署、执行和隔离小型虚拟软件功能成为可能**。我们实现了Femto-Containers，并在RIOT中提供了集成，这是一个流行的开源物联网操作系统。我们对我们的实现进行了性能评估，该实现已经经过了故障隔离的正式验证，保证RIOT受到在Femto-Container中加载和执行的逻辑的保护。我们在各种流行的微控制器架构（Arm Cortex-M、ESP32和RISC-V）上进行了实验，结果表明Femto-Containers在内存占用、能源消耗和安全性方面具有良好的平衡。

### Goals of this paper

本文的目标是设计一种适用于异构微控制器的中间件函数运行时，主要实现在低功耗物联网设备上安全地部署、执行和隔离小型虚拟软件功能。我们的首要目标是部署功能的小启动时间，并且与原生实现相比，对微控制器的内存占用几乎没有额外开销。本文的主要贡献如下：

### Contri

• 我们提出了Femto-Containers，这是一种新的中间件，可以在异构微控制器的物联网设备上抽象、安全地部署、执行和隔离（多个并发）软件功能。我们将 Femto-Containers 设计为rBPF虚拟机的扩展；
• 我们基于Python、WebAssembly、JavaScript和eBPF评估了超轻量级虚拟化技术的性能，并展示了基于eBPF虚拟化的Femto-Container运行时相比其他技术需要10倍更少的内存占用；
• 我们提供了 Femto-Containers 的开源实现，并将其实际集成到低功耗网络微控制器的常见通用操作系统（RIOT）中；
• 我们正式验证了 Femto-Container 实现的关键组件，保证了Femto-Containers之间以及底层操作系统之间的故障隔离；
• 我们在Arm Cortex-M、ESP32和RISC-V等流行的32位微控制器架构上评估了Femto-Containers在各种用例下的性能。

场景：

在这个背景下，我们确定了以下使用案例类别，如图1所示：
（1）使用案例1：托管和隔离高级业务功能。该功能可以通过低功耗网络进行安全、按需、远程更新。这种逻辑的执行通常是周期性的，并且具有松散的（非实时的）时间要求。
（2）使用案例2：托管和隔离底层的调试和监视代码功能。这些功能可以通过网络按需插入和删除。这些功能不能干扰设备上现有的代码。相比之下，这种函数的生命周期较短，具有更严格的时间要求。
（3）使用案例3：托管和隔离由几个不同租户管理的几个功能。
上述场景的用户提供了基于事件驱动的编程模型和精细的计算空间，可以按需托管在指定的低功耗IoT设备上。此外，对于一个功能可用的API基本上抽象了大部分硬件和操作系统。从概念上讲，这些场景在某种程度上类似于函数即服务（FaaS）编程模型[12]。

然而，由于不能保证稳定的高吞吐量网络连接，存储能力被限制为设备本地存储。此外，FaaS和容器技术的可扩展性方面（例如在单台机器上运行数千个容器）在这里并不起重要作用。相反，我们所确定的场景需要在嵌入式操作系统上运行少量隔离的功能。然而，考虑到潜在的大量IoT设备，该场景可能仍涉及大量容器（但跨多个设备）。

威胁模型

当客户在现场部署设备上的功能时，嵌入式环境必须确保这些功能被沙箱化。在我们的威胁模型中，我们考虑了可能部署恶意代码的恶意租户和可能恶意交互已部署代码的恶意客户端[34]。

![Untitled](imgs/Untitled.png)

relate work

先前关于轻量级虚拟化运行时的绝大多数工作[29]并不针对微控制器，而是针对微处理器级计算机。最近的例子包括用于无服务器计算的AWS Firecracker [2]，用于Web浏览器中的进程隔离的WebAssembly [14]，或在运行时插入Linux内核的调试和检验代码的eBPF [11,28]。然而，一些超轻量级虚拟化方法已经被提出用于微控制器。例如，提出了适用于32位微控制器的最小化WebAssembly运行时，例如WAMR [10]和WASM3 [35]。RapidPatch [17]使用eBPF运行时为RTOS固件提供热补丁框架。微控制器的VM运行时还包括早期的示例，例如Mate [25]或Darjeeling [9]，它是Java VM的子集，修改为使用16位体系结构，专为8位和16位微控制器设计。JavaCard [31]还使用了专为加密目的量身定制的小型Java虚拟机，运行在智能卡上。最近，还提出了微小的脚本逻辑解释器和运行时，以提供基本的虚拟化环境。例如，MicroPython [27]是在微控制器上使用的非常流行的脚本逻辑解释器。在先前的工作中，如NanoLambda [13]，在ESP8266微控制器上使用小型Python运行时。在先前的工作中，如RIOTjs [4]，在Cortex-M微控制器上使用小型JavaScript运行时。然而，应该使用互相隔离的补充机制来保证脚本之间的相互隔离（例如SecureJS [20]）。最相关的工作发表在[39]和[37]中。在[39]中，作者提供了rBPF，eBPF指令集的一个端口，以在微控制器上托管（单个）VM。相比之下，我们扩展了rBPF的指令集架构和VM核心，提供了适当的嵌入式加载和执行环境，以满足在网络化微控制器上实时部署（多个）函数的明确定义的、事件驱动的、短暂的和隔离的（并发）执行。另一方面，虽然[37]关注单个rBPF指令解释器的形式验证，但我们也验证了预先检查的指令检查器，并将两者集成到我们的femto-container实现中-我们在各种微控制器上彻底评估了其性能。我们的设计和实现非常小（几百行代码），因此形式验证确实是现实的。相比之下，软件替代方案（WASM，MicroPython...）将需要数十万行代码，以及更多的证明，几乎无法具体验证。据我们所知，硬件替代方案（例如TrustZone [32]）没有经过形式验证，并且可能需要软件API以避免未指定的硬件行为，因此会出现故障。据我们所知，我们的工作提供了第一个基于eBPF虚拟化的经过形式验证的中间件，能够在各种异构低功率微控制器上托管多个微小的运行时容器。

我们的工作提供了第一个基于eBPF虚拟化的经过形式验证的中间件，能够在各种异构低功率微控制器上托管多个微小的运行时容器。

嵌入式运行时架构设计

与FaaS运行时类似，Femto-容器允许部署和执行小型逻辑模块。这些模块或函数托管在中间件之上提供隔离、抽象和与底层操作系统和硬件紧密隔离。通过结合隔离和硬件/操作系统抽象，我们保留了FaaS运行时的关键属性：代码移植性和网络安全性。然而，与典型的FaaS运行时不同，Femto-容器必须能够与特定硬件（例如传感器/执行器）交互，并且必须大大减少虚拟化的范围和成本以应对物联网硬件限制。因此，Femto-容器架构依赖于超轻量级虚拟化，以及一系列假设和功能。

Benchmark

在本节中，我们比较了使用RIOT [5]来扩展Femto-Container功能的概念验证的性能，基于不同的超轻量级隔离技术：Python（MicroPython运行时），WebAssembly（WASM3运行时），eBPF（rBPF运行时）和Javascript（RIOTjs运行时）。我们在一个现成的物联网硬件平台上运行每个虚拟化候选，该平台代表现代32位微控制器架构的景观：Arm CortexM4。基准测试设置的详细信息在附录A中。在下面的基准测试中，每个实现都加载了一个VM，该VM托管在360 B输入字符串上执行Fletcher32校验和逻辑。

![Untitled](imgs/Untitled 1.png)

为什么最后选了 eBPF?

我们的基准测试显示，在内存开销、启动时间和代码行数方面，使用eBPF虚拟化的Femto-Containers是迄今为止最具吸引力的。我们注意到，使用WebAssembly的执行时间比rBPF快2倍。但是，我们预计在我们针对的小型处理工作负载等用例中，执行时间增加2倍不会产生实质性影响。因为我们的重点在于内存占用（回想一下我们对容器化功能的内存开销约为10%的目标），因此我们选择rBPF来进一步完善我们的概念。

FEMTO-CONTAINER RUNTIME IMPLEMENTATION

![Untitled](imgs/Untitled 2.png)

Programming Model

Femto-Containers遵循事件驱动编程模型。托管的应用程序仅在操作系统中触发事件时才执行。应用程序指定入口点和它们要附加到操作系统中的钩子。Femto-Containers中可以部署的逻辑受限于eBPF架构。例如，不支持异步操作：没有选项可以从虚拟机外部中断Femto-Container应用程序中的控制流。这主要是由于架构的简单性导致的：既不支持中断也不支持间接跳转。这种权衡减少了灵活性，但增加了主机操作系统的安全性。

微型容器的关键组件在网络安全方面是rBPF解释器和预飞指令检查器。由于实现非常小巧（解释器和检查器仅有500行C代码），我们的目标是生产这些组件的正式验证实现。我们将使用经过正式验证的解释器和检查器的运行时称为CertFC（认证微型容器）。
针对要求的形式化。我们希望为微型容器提供的安全保障基本上是内存和故障隔离。更具体地说，我们想证明CertFC无法访问应用程序寄存器内存之外的内存位置，也无法执行导致未定义行为的指令，从而导致虚拟机和/或其主机崩溃。提供这些保证进一步加强了威胁模型所需的安全性，以防止访问沙箱外的内存，从而防止对操作系统或其他虚拟机的非特权访问。
正式验证方法。我们使用Coq证明助手通过采用图6中描述的设计工作流程来机械化和全面验证这些要求：

![Untitled](imgs/Untitled 3.png)

1. 首先，我们提供了一个证明模型和一个 C-ready 实现，它们分别对 RIOT 中 rBPF 验证器和虚拟机的本地、原始 C 实现进行了形式化（响应地进行了优化）。在 Coq 中，证明和“C-ready”模型被证明是语义等价的。
2. Coq 证明助手在 VM 的证明模型上执行了预期的安全性和隔离性属性的验证。它依赖于 a) CompCert C 内存模型 [24] ii) 验证器的预检运行时检查，以及 iii) 虚拟机本身的防御性运行时检查（针对数字和内存操作）提供的形式化隔离保证。
3. 通过使用 𝜕𝑥 工具 [19] 从 C-ready Coq 模型中自动提取验证的 C 实现。基于从 Coq 到 C 的一组形式化转换规则，𝜕𝑥 允许从功能性 Coq 定义中制作出可审查和优化的 C 代码。
4. 为确保提取的 C 代码细化了证明模型，从而满足安全性和隔离性属性，最终的仿真证明分为两个步骤。首先，使用 VST-clightgen 工具 [3] 从生成的 C 代码中提取 CompCert Clight 模型。其次，使用翻译验证 [33] 证明 Clight 模型可以模拟 C-ready 模型。

PERFORMANCE EVALUATION

![Untitled](imgs/Untitled 4.png)

结论

在本文中，我们介绍了 Femto-Containers，这是我们设计的一种新的中间件运行时架构，它使得 FaaS 能力嵌入到异构低功耗 IoT 硬件中。
使用 Femto-Containers，经授权的 IoT 软件维护者可以通过网络部署和管理嵌入在基于微控制器的设备上的互相隔离的软件模块。我们提供了 FemtoContainer 运行时的开源实现，它使用了移植到微控制器的 eBPF 指令集，并集成在一个通用的低功耗 IoT 操作系统（RIOT）中。我们正式验证了一个故障隔离保证，确保 RIOT 被屏蔽免受在 Femto-Container 中加载和执行的任意逻辑的影响，而不需要任何特定的基于硬件的内存隔离机制。然后，我们在最常见的 32 位微控制器架构上展示了 Femto-Container 运行时的性能：Arm Cortex-M、RISC-V、ESP32。我们展示了 Femto-Containers 明显提高了现有技术水平，通过在这些微控制器上提供强大的安全保证的 FaaS-like 能力，同时与本地执行相比仅需要极少的 Flash 和 RAM 内存开销（小于 10%）。
