KataOS入门-简介和代码编译
原创 thatway 那路谈OS与SoC嵌入式软件 2022-10-19 07:21
先来说一个新闻：谷歌前几天（2022.10.14）宣布发布 **KataOS**
，它是用于进行机器学习的嵌入式
设备的操作系统。KataOS 从设计上就具备安全
考虑，不但几乎完全是由 Rust
实现的，而且是建立在 seL4 微内核
的基础之上，seL4 在数学上被证明
是安全的，具有保证保密性、完整性和可用性。
关于嵌入式软件的发展方向
，说点
个人见解
：
1）从linux宏内核的粗放型会向微内核的细颗粒控制
的方向转变，更强调系统的安全性
，一方面内核缩小，一方面各个应用间彼此隔离。
2）从编程语言上，会转向少写bu**g
的语言，当代码很容易堆砌，成本比较低的时候，会更加注重质量
，新的编程语言一方面会校验
不写bug，另一方面会随着硬件变化**
自动补充功能，虽然编程语言的发展很难，例如Rust十几年了才更被大家所知，但是这是趋势。参考文章：
https://mp.weixin.qq.com/s/6GapcTpdE3Vg0ntKexbSSA
3）对于核心程序已经不能满足工具技术来让其正确了，需要对bug零容忍，也就是从正面保证
其正确性
，而不是靠经验的测试和编码，从数学上就是形式化
，但是证明工作量巨大，不过也是趋势。
现在你再去看这段**新闻**
，你会发现不得了，大家想干的事情，谷歌先干了
，而且不自己从无到有的造一个，用了已有的sel4
（微内核+形式化验证）和Rust
（新语言）结合。美中不足的是现在还在开发中，只是公布了第一版，但是就像之前谷歌的Fuchsia、安卓等一样，代码开放程度还是挺好的，基本不保留。这样我们就可以上我们的惯例了：
代码下载+编译+运行
。
1. KataOS简介
目前我们使用的很多智能设备收集的**个人身份数据**
——
例如人的图像和他们的声音录音等，如果其被恶意软件访问就会有安全问题
。所以必须从数学上证明能够保证数据的安全，也就是我们经常说的形式化验证的方法。KataOS
就是这么一个简单的解决方案来为嵌入式硬件构建可验证的安全系统。
**Google
Research 团队**
已着手通过构建一个可证明的安全平台来解决这个问题，就是上面说的
KataOS
。这是一个正在进行的项目，还有很多事情要做，但我们很高兴能分享一些早期的细节并邀请其他人在平台上进行协作，这样我们就可以构建默认内置安全性的智能环境系统。上代码：
https://github.com/AmbiML/sparrow-manifest
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-sys
crate
，然后跟
Antmicro公司
合作优化了
sel4-sys
crate
，形成了框架，加上了调试模拟和基于硬件的Sparrow
安全验证运行环境（初始版本未公开
）。
下面看官网论坛介绍：
KataOS
开源了几个组件，并与
Antmicro
合作开发了他们的
Renode
模拟器和相关框架
。作为这个新操作系统的基础，我们选择
seL4
作为微内核，因为它把安全放在首位；它在数学上被证明是安全的，具有保证的机密性、完整性和可用性。通过
seL4
CAmkES
框架，我们还能够提供静态定义和可分析的系统组件。
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
系统始终值得信赖的未来。
---作者：Sam、Scott 和 June –
AmbiML 开发人员
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
3.2 rust环境安装
然后是Rust安装，参考：
https://www.rust-lang.org/learn/get-started
执行命令：
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编译器安装
```
会提示编译工具找不到，如下：
![][3]
打开：
https://developer.arm.com/downloads/-/gnu-a
![][4]
下载后解压到文件夹，然后把路径添加到环境变量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，修正后会出现如下：**
![][5]
表示编译成功，下面就是运行了。
****
**4. 运行**
```
cd build-aarch64
./simulate -M raspi3b
修改代码：
重新编译运行，会看到打印出来。
这里的adder项目是**camkes**的，不是**Sparrow框架**
的，上面说过
Sparrow还没开源，可能是其基于
RISC-V硬件实现的，还没有用qemu搞。
后记：
本文算是对**最新**
的OS技术进行一些探究，这个KataOS跟SeL4很有渊源，后续会继续研究下。
后续会继续更新，纯干货
分析，无广告，不打赏，欢迎
转载
，欢迎
评论交流
！
参考：