一文浅析KataOS的基础知识

先来说一个新闻：谷歌前几天（2022.10.14）宣布发布 KataOS，它是用于进行机器学习的嵌入式设备的操作系统。KataOS 从设计上就具备安全考虑，不但几乎完全是由 Rust 实现的，而且是建立在 seL4 微内核的基础之上，seL4 在数学上被证明是安全的，具有保证保密性、完整性和可用性。

关于嵌入式软件的发展方向，说点个人见解：

1）从linux宏内核的粗放型会向微内核的细颗粒控制的方向转变，更强调系统的安全性，一方面内核缩小，一方面各个应用间彼此隔离。

2）从编程语言上，会转向少写bug的语言，当代码很容易堆砌，成本比较低的时候，会更加注重质量，新的编程语言一方面会校验不写bug，另一方面会随着硬件变化自动补充功能，虽然编程语言的发展很难，例如Rust十几年了才更被大家所知，但是这是趋势。

3）对于核心程序已经不能满足工具技术来让其正确了，需要对bug零容忍，也就是从正面保证其正确性，而不是靠经验的测试和编码，从数学上就是形式化，但是证明工作量巨大，不过也是趋势。

现在你再去看这段新闻，你会发现不得了，大家想干的事情，谷歌先干了，而且不自己从无到有的造一个，用了已有的sel4（微内核+形式化验证）和Rust（新语言）结合。美中不足的是现在还在开发中，只是公布了第一版，但是就像之前谷歌的Fuchsia、安卓等一样，代码开放程度还是挺好的，基本不保留。这样我们就可以上我们的惯例了： 代码下载+编译+运行。

1.KataOS简介

    

目前我们使用的很多智能设备收集的个人身份数据——例如人的图像和他们的声音录音等，如果其被恶意软件访问就会有安全问题。所以必须从数学上证明能够保证数据的安全，也就是我们经常说的形式化验证的方法。KataOS就是这么一个简单的解决方案来为嵌入式硬件构建可验证的安全系统。

GoogleResearch 团队已着手通过构建一个可证明的安全平台来解决这个问题，就是上面说的KataOS。这是一个正在进行的项目，还有很多事情要做，但我们很高兴能分享一些早期的细节并邀请其他人在平台上进行协作，这样我们就可以构建默认内置安全性的智能环境系统。

sudo apt-get install repo
mkdir sparrow
cd sparrow
repo init -u https://github.com/AmbiML/sparrow-manifest -m camkes-manifest.xml
repo sync -j4

2. 代码介绍

    

从整体上看，KataOS完全借用了开源软件的力量，可以说是攒出来的系统，微内核用现成的SeL4，为了在其上面运行Rust程序使用了一个开源软件sel4-syscrate，然后跟Antmicro公司合作优化了sel4-syscrate，形成了框架，加上了调试模拟和基于硬件的Sparrow安全验证运行环境（初始版本未公开）。

下面看官网论坛介绍：

KataOS 开源了几个组件，并与 Antmicro合作开发了他们的Renode 模拟器和相关框架。作为这个新操作系统的基础，我们选择seL4作为微内核，因为它把安全放在首位；它在数学上被证明是安全的，具有保证的机密性、完整性和可用性。通过 seL4CAmkES 框架，我们还能够提供静态定义和可分析的系统组件。

KataOS提供了一个可验证安全的平台来保护用户的隐私，因为应用程序在逻辑上不可能违反内核的硬件安全保护，并且系统组件是可验证安全的。KataOS也几乎完全用Rust实现，它为软件安全性提供了一个强有力的起点，因为它消除了整个类别的错误，例如一个错误和缓冲区溢出。

当前的 GitHub 版本包含了大部分 KataOS 核心部分，包括我们用于 Rust 的框架（例如 sel4-sys crate，它提供了 seL4 系统调用 API），一个用 Rust 编写的备用根服务器（用于动态系统范围的内存管理） )，以及对 seL4 的内核修改，可以回收根服务器使用的内存。我们与 Antmicro合作，使用Renode为我们的目标硬件启用 GDB 调试和模拟。

在内部，KataOS还能够动态加载和运行在CAmkES 框架之外构建的第三方应用程序。目前，Github上的代码不包含运行这些应用程序所需的组件，但我们希望在不久的将来发布这些功能。

为了完整地证明一个安全的环境系统，我们还为KataOS 构建了一个名为Sparrow 的参考实现，它将KataOS 与一个安全的硬件平台相结合。因此，除了逻辑安全的操作系统内核之外，Sparrow还包括一个逻辑安全的信任根，该信任根是使用OpenTitan在 RISC-V 架构上构建的。但是，对于我们的初始版本，我们的目标是使用QEMU 在模拟中运行更标准的64 位ARM 平台。

我们的目标是开源所有Sparrow，包括所有硬件和软件设计。目前，我们刚刚开始在 GitHub 上发布 KataOS的早期版本。所以这只是一个开始，我们希望您能与我们一起建立一个智能环境ML 系统始终值得信赖的未来。

camkes-tool : seL4 的 camkes-tool 存储库，增加了支持 KataOS 服务的功能
capdl : seL4 的 capdl 存储库，添加了 KataOS 服务和 KataOS 根服务器（替代 capdl-loader-app，用 Rust 编写并支持将系统资源移交给 KataOS MemoryManager 服务）
kernel:seL4的内核，带有用于Sparrow的RISC-V平台的驱动程序，并支持回收KataOS根服务器使用的内存用于在Rust中开发的kata框架，以及（最终）KataOS系统服务
脚本：支持脚本，包括 build-sparrow.sh

大多数 KataOS Rust crates 位于kata/apps/system/components目录中。通用/共享代码在kata-os-common中：

allocator : 建立在链表分配器箱上的堆分配器
camkes：支持在 Rust 中编写 CAmkES 组件
capdl : 支持读取 capDL-tool 生成的 capDL 规范
copyregion : 临时将物理页面映射到线程的 VSpace 的助手
cspace-slot ：插槽分配器的 RAII 助手
logger : seL4 与 Rust logger crate 的集成
model : 支持处理 capDL；由 kata-os-rootserver 使用
panic：一个特定于 seL4 的恐慌处理程序
sel4-config : 为 seL4 内核配置构建胶水
sel4-sys : seL4 系统接口和胶水
slot-allocator：顶级 CNode 中插槽的分配器

3.搭建编译环境

3.1 sel4环境安装

由于其使用的sel4微内核，可以先搭建下sel4的，参考 https://docs.sel4.systems/projects/buildsystem/host-dependencies.html seL4微内核入门-代码下载运行及资料

3.2 rust环境安装

然后是Rust安装，执行命令：

curl --proto '=https'--tlsv1.2 -sSf https://sh.rustup.rs | sh
cargo --version
rustup toolchain add nightly-2021-11-05
rustup target add --toolchain
nightly-2021-11-05-x86_64-unknown-linux-gnu aarch64-unknown-none

3.3 gcc编译器安装

执行：sh scripts/build-sparrow.sh aarch64 会提示编译工具找不到，如下：



打开： https://developer.arm.com/downloads/-/gnu-a



下载后解压到文件夹，然后把路径添加到环境变量PATH： 例如：在~/.bashrc中加入：

export PATH=$PATH: /home/XXX/tools/gcc-arm-10.3-2021.07-x86_64-aarch64-none-linux-gnu/bin

3.4 tempita安装

pip install tempita

多次执行sh scripts/build-sparrow.sh aarch64，修正后会出现如下：

表示编译成功，下面就是运行了。

4.运行

cd build-aarch64
./simulate -M raspi3b

修改代码：



重新编译运行，会看到打印出来。

这里的adder项目是camkes的，不是Sparrow框架的，上面说过Sparrow还没开源，可能是其基于RISC-V硬件实现的，还没有用qemu搞。

后记：

本文算是对最新的OS技术进行一些探究，这个KataOS跟SeL4很有渊源，后续会继续研究下。






审核编辑：刘清