延伸操作系统论坛的一篇帖子,欢迎参与讨论
CantripOS 操作系统,它运行在 seL4 之上并且几乎完全用 Rust 编写。 CantripOS 由一组使用 CAmkES 封装的系统服务和动态加载到 seL4 线程上下文中的应用程序组成,并通过 SDK 运行时环境与系统服务进行通信。CantripOS 据悉是可能是由 KataOS 更名而来。Google 研究员曾在 seL4 2023 峰会上介绍过 CantripOS 我们将在未来专门介绍那次演讲的内容。
根据Google Opensecura页面的信息显示:
概述:什么是 CantripOS?
CantripOS 是一个面向环境机器学习应用的低功耗安全嵌入式操作系统,小巧、安全且可扩展的操作系统框架,专为资源受限的嵌入式设备设计。它的核心目标是利用 seL4
微内核 提供的高保证度安全特性,为设备构建一个可信的计算基础 (Trusted Computing Base, TCB)。
CantripOS 是 Shodan 项目中自主研发的操作系统,它运行在经过形式化验证的 seL4 微内核之上,并且(除了 seL4 内核部分)几乎完全采用 Rust 编写。下面我们将详细介绍 CantripOS 的设计理念、架构与实现细节。
Project Shodan 致力于构建一个低功耗、安全的嵌入式平台,专门针对环境机器学习(Ambient ML)应用。该平台充分利用了 RISC-V 架构和 OpenTitan 安全核心,为物联网、传感器网络以及其他安全关键型嵌入式设备提供坚实的硬件基础。
一、总体架构与设计理念
CantripOS 的设计充分考虑了嵌入式环境对安全性、可靠性和低功耗的严格要求。其核心设计理念主要体现在以下几个方面:
-
基于 seL4 微内核的安全隔离
- 形式化证明的安全性:seL4 微内核以形式化证明而著称,它为整个系统提供了严格的安全隔离和资源控制,确保内核层能够防止恶意代码和错误访问。
- 硬件保护:利用微控制器上的内存保护单元(MPU),确保用户进程之间、以及进程与内核之间的隔离,即使多个组件共享同一硬件总线(如 I²C),也只能访问各自被授权的外设。
-
100% Rust 实现的运行时环境
- 语言安全:除 seL4 内核外,CantripOS 的所有系统服务和大部分运行时组件均采用 Rust 编写。Rust 的所有权模型和类型安全保证在编译时捕获绝大多数内存错误,极大降低运行时故障风险。
- 组件化设计:CantripOS 借鉴了 CAmkES 的静态组件化思想,通过 Rust 模板和工具(如 camkes-tool 与 capdl),实现了类似“乐高积木”的服务组装方式。这样,系统服务与应用程序可以灵活组合,彼此之间通过明确定义的接口通信。
-
动态应用加载与 SDK 运行时环境
- 动态加载:应用程序被动态加载到受限的 seL4 线程上下文中,并通过一个专门的 SDK 运行时环境与系统服务进行通信。这种设计既确保了系统的灵活性,又允许在运行时更新和扩展应用功能。
- 进程与 Capsule 混合模型:内核组件以 Capsule 形式运行(协作式调度,几乎无运行时开销),而用户应用则以独立进程运行(通过 MPU 隔离,采用抢占式调度),各自权衡了性能、内存开销与安全性。
-
安全启动与可信执行
- 基于 OpenTitan 的安全核心:CantripOS 集成了 OpenTitan 安全核心,确保安全引导、固件验证和加密操作,形成了可信执行链条,为整个系统的安全运行提供了坚实保障。
二、软件组成与构建流程
Project Shodan 的软件堆栈包括以下主要部分:
-
CantripOS 操作系统
运行在 seL4 微内核之上,其核心服务和运行时组件几乎完全由 Rust 实现。系统内的服务通过 Capsule 和进程模型实现不同级别的隔离和并发调度。 -
CAmkES 系统服务组装
CantripOS 的系统服务由 CAmkES 项目组装,该项目代码存在于一个独立的 Git 仓库中,因为其中包含了不打算上游到 seL4 源码树的部分。目标平台相关的 CAmkES 组装描述文件位于apps/system/platforms
目录中,使用标准的 CAmkES 构建系统构建,要求预先安装好 CAmkES 的依赖项。 -
顶层配置与构建文件
- 配置文件:顶层配置文件存放在
easy-settings.cmake
和settings.cmake
中,用于定义项目的全局配置参数。 - 构建脚本:与构建相关的配置则位于
build/kata.mk
以及附近的 makefile 文件中,确保整个系统的编译和链接过程符合目标平台要求。
- 配置文件:顶层配置文件存放在
三、关键特性与优势
1. 安全性
- 硬件与软件双重防护:利用 MPU 实现硬件级内存隔离,同时依靠 Rust 的类型系统在编译时提供安全检查,确保各组件只能通过明确接口访问共享资源。
- 隔离与容错:无论是系统服务还是应用程序,均实现了严格的隔离,即使某个组件发生故障也不会影响整个系统。
2. 可靠性
- 事件驱动内核:CantripOS 内核采用事件驱动模型,不使用动态堆分配,从而杜绝了内存泄漏和碎片化问题,确保长时间稳定运行。
- 抢占式进程调度:用户进程采用抢占式调度,即使单个进程崩溃,内核仍能保证其他进程继续正常运行,并支持动态加载与更新。
3. 低功耗运行
- 自动低功耗管理:系统能够根据应用需求自动将硬件置于最低功耗状态,无需开发者编写专门的电源管理代码,使得设备能够在电池供电或能量采集条件下长期稳定运行。
- 适用于环境机器学习:针对 Ambient ML 应用,CantripOS 在保证高安全性与可靠性的同时,优化了能耗,使其非常适合部署在远程传感器、智能设备等低功耗场景中。
四、面向未来的应用场景
Project Shodan 的目标平台面向环境机器学习应用,强调在嵌入式设备上安全、高效地运行复杂的机器学习工作负载。通过结合先进的硬件(RISC-V 与 OpenTitan)和软件架构,CantripOS 不仅能满足传感器网络、物联网设备以及安全关键设备的需求,还为基于 ML 的新兴应用场景提供了理想的平台。
五、总结
Project Shodan 及其核心操作系统 CantripOS 代表了嵌入式系统设计的一种前沿趋势:在极其受限的硬件资源下,通过硬件保护、形式化验证和现代编程语言(Rust)的安全特性,实现高安全性、高可靠性和低功耗的多任务运行环境。其灵活的组件化设计和动态应用加载机制使系统既能够满足传统嵌入式设备的需求,又为环境机器学习等新兴应用场景提供了强大的支持。本文使用了多种翻译工具来翻译和补充背景信息和知识。不足之处及疏忽请移步讨论:https://zhos.net/t/kataos-cantripos/1305
参考资料:seL4 Summit 2023 演讲文稿、相关项目文档与 CAmkES 构建系统说明, Google
Comments