先來(lái)說(shuō)一個(gè)新聞：谷歌前幾天（2022.10.14）宣布發(fā)布 KataOS，它是用于進(jìn)行機(jī)器學(xué)習(xí)的嵌入式設(shè)備的操作系統(tǒng)。KataOS 從設(shè)計(jì)上就具備安全考慮，不但幾乎完全是由 Rust 實(shí)現(xiàn)的，而且是建立在 seL4 微內(nèi)核的基礎(chǔ)之上，seL4 在數(shù)學(xué)上被證明是安全的，具有保證保密性、完整性和可用性。

關(guān)于嵌入式軟件的發(fā)展方向，說(shuō)點(diǎn)個(gè)人見(jiàn)解：

1）從linux宏內(nèi)核的粗放型會(huì)向微內(nèi)核的細(xì)顆粒控制的方向轉(zhuǎn)變，更強(qiáng)調(diào)系統(tǒng)的安全性，一方面內(nèi)核縮小，一方面各個(gè)應(yīng)用間彼此隔離。

2）從編程語(yǔ)言上，會(huì)轉(zhuǎn)向少寫(xiě)bug的語(yǔ)言，當(dāng)代碼很容易堆砌，成本比較低的時(shí)候，會(huì)更加注重質(zhì)量，新的編程語(yǔ)言一方面會(huì)校驗(yàn)不寫(xiě)bug，另一方面會(huì)隨著硬件變化自動(dòng)補(bǔ)充功能，雖然編程語(yǔ)言的發(fā)展很難，例如Rust十幾年了才更被大家所知，但是這是趨勢(shì)。

3）對(duì)于核心程序已經(jīng)不能滿足工具技術(shù)來(lái)讓其正確了，需要對(duì)bug零容忍，也就是從正面保證其正確性，而不是靠經(jīng)驗(yàn)的測(cè)試和編碼，從數(shù)學(xué)上就是形式化，但是證明工作量巨大，不過(guò)也是趨勢(shì)。

現(xiàn)在你再去看這段新聞，你會(huì)發(fā)現(xiàn)不得了，大家想干的事情，谷歌先干了，而且不自己從無(wú)到有的造一個(gè)，用了已有的sel4（微內(nèi)核+形式化驗(yàn)證）和Rust（新語(yǔ)言）結(jié)合。美中不足的是現(xiàn)在還在開(kāi)發(fā)中，只是公布了第一版，但是就像之前谷歌的Fuchsia、安卓等一樣，代碼開(kāi)放程度還是挺好的，基本不保留。這樣我們就可以上我們的慣例了： 代碼下載+編譯+運(yùn)行。

1.KataOS簡(jiǎn)介

????

目前我們使用的很多智能設(shè)備收集的個(gè)人身份數(shù)據(jù)——例如人的圖像和他們的聲音錄音等，如果其被惡意軟件訪問(wèn)就會(huì)有安全問(wèn)題。所以必須從數(shù)學(xué)上證明能夠保證數(shù)據(jù)的安全，也就是我們經(jīng)常說(shuō)的形式化驗(yàn)證的方法。KataOS就是這么一個(gè)簡(jiǎn)單的解決方案來(lái)為嵌入式硬件構(gòu)建可驗(yàn)證的安全系統(tǒng)。

GoogleResearch 團(tuán)隊(duì)已著手通過(guò)構(gòu)建一個(gè)可證明的安全平臺(tái)來(lái)解決這個(gè)問(wèn)題，就是上面說(shuō)的KataOS。這是一個(gè)正在進(jìn)行的項(xiàng)目，還有很多事情要做，但我們很高興能分享一些早期的細(xì)節(jié)并邀請(qǐng)其他人在平臺(tái)上進(jìn)行協(xié)作，這樣我們就可以構(gòu)建默認(rèn)內(nèi)置安全性的智能環(huán)境系統(tǒng)。

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完全借用了開(kāi)源軟件的力量，可以說(shuō)是攢出來(lái)的系統(tǒng)，微內(nèi)核用現(xiàn)成的SeL4，為了在其上面運(yùn)行Rust程序使用了一個(gè)開(kāi)源軟件sel4-syscrate，然后跟Antmicro公司合作優(yōu)化了sel4-syscrate，形成了框架，加上了調(diào)試模擬和基于硬件的Sparrow安全驗(yàn)證運(yùn)行環(huán)境（初始版本未公開(kāi)）。

下面看官網(wǎng)論壇介紹：

KataOS 開(kāi)源了幾個(gè)組件，并與 Antmicro合作開(kāi)發(fā)了他們的Renode 模擬器和相關(guān)框架。作為這個(gè)新操作系統(tǒng)的基礎(chǔ)，我們選擇seL4作為微內(nèi)核，因?yàn)樗寻踩旁谑孜唬凰跀?shù)學(xué)上被證明是安全的，具有保證的機(jī)密性、完整性和可用性。通過(guò) seL4CAmkES 框架，我們還能夠提供靜態(tài)定義和可分析的系統(tǒng)組件。

KataOS提供了一個(gè)可驗(yàn)證安全的平臺(tái)來(lái)保護(hù)用戶的隱私，因?yàn)閼?yīng)用程序在邏輯上不可能違反內(nèi)核的硬件安全保護(hù)，并且系統(tǒng)組件是可驗(yàn)證安全的。KataOS也幾乎完全用Rust實(shí)現(xiàn)，它為軟件安全性提供了一個(gè)強(qiáng)有力的起點(diǎn)，因?yàn)樗苏麄€(gè)類別的錯(cuò)誤，例如一個(gè)錯(cuò)誤和緩沖區(qū)溢出。

當(dāng)前的 GitHub 版本包含了大部分 KataOS 核心部分，包括我們用于 Rust 的框架（例如 sel4-sys crate，它提供了 seL4 系統(tǒng)調(diào)用 API），一個(gè)用 Rust 編寫(xiě)的備用根服務(wù)器（用于動(dòng)態(tài)系統(tǒng)范圍的內(nèi)存管理） )，以及對(duì) seL4 的內(nèi)核修改，可以回收根服務(wù)器使用的內(nèi)存。我們與 Antmicro合作，使用Renode為我們的目標(biāo)硬件啟用 GDB 調(diào)試和模擬。

在內(nèi)部，KataOS還能夠動(dòng)態(tài)加載和運(yùn)行在CAmkES 框架之外構(gòu)建的第三方應(yīng)用程序。目前，Github上的代碼不包含運(yùn)行這些應(yīng)用程序所需的組件，但我們希望在不久的將來(lái)發(fā)布這些功能。

為了完整地證明一個(gè)安全的環(huán)境系統(tǒng)，我們還為KataOS 構(gòu)建了一個(gè)名為Sparrow 的參考實(shí)現(xiàn)，它將KataOS 與一個(gè)安全的硬件平臺(tái)相結(jié)合。因此，除了邏輯安全的操作系統(tǒng)內(nèi)核之外，Sparrow還包括一個(gè)邏輯安全的信任根，該信任根是使用OpenTitan在 RISC-V 架構(gòu)上構(gòu)建的。但是，對(duì)于我們的初始版本，我們的目標(biāo)是使用QEMU 在模擬中運(yùn)行更標(biāo)準(zhǔn)的64 位ARM 平臺(tái)。

我們的目標(biāo)是開(kāi)源所有Sparrow，包括所有硬件和軟件設(shè)計(jì)。目前，我們剛剛開(kāi)始在 GitHub 上發(fā)布 KataOS的早期版本。所以這只是一個(gè)開(kāi)始，我們希望您能與我們一起建立一個(gè)智能環(huán)境ML 系統(tǒng)始終值得信賴的未來(lái)。

camkes-tool : seL4 的 camkes-tool 存儲(chǔ)庫(kù)，增加了支持 KataOS 服務(wù)的功能
capdl : seL4 的 capdl 存儲(chǔ)庫(kù)，添加了 KataOS 服務(wù)和 KataOS 根服務(wù)器（替代 capdl-loader-app，用 Rust 編寫(xiě)并支持將系統(tǒng)資源移交給 KataOS MemoryManager 服務(wù)）
kernel:seL4的內(nèi)核，帶有用于Sparrow的RISC-V平臺(tái)的驅(qū)動(dòng)程序，并支持回收KataOS根服務(wù)器使用的內(nèi)存用于在Rust中開(kāi)發(fā)的kata框架，以及（最終）KataOS系統(tǒng)服務(wù)
腳本：支持腳本，包括 build-sparrow.sh

大多數(shù) KataOS Rust crates 位于kata/apps/system/components目錄中。通用/共享代碼在kata-os-common中：

allocator : 建立在鏈表分配器箱上的堆分配器
camkes：支持在 Rust 中編寫(xiě) CAmkES 組件
capdl : 支持讀取 capDL-tool 生成的 capDL 規(guī)范
copyregion : 臨時(shí)將物理頁(yè)面映射到線程的 VSpace 的助手
cspace-slot ：插槽分配器的 RAII 助手
logger : seL4 與 Rust logger crate 的集成
model : 支持處理 capDL；由 kata-os-rootserver 使用
panic：一個(gè)特定于 seL4 的恐慌處理程序
sel4-config : 為 seL4 內(nèi)核配置構(gòu)建膠水
sel4-sys : seL4 系統(tǒng)接口和膠水
slot-allocator：頂級(jí) CNode 中插槽的分配器

3.搭建編譯環(huán)境

3.1 sel4環(huán)境安裝

由于其使用的sel4微內(nèi)核，可以先搭建下sel4的，參考 https://docs.sel4.systems/projects/buildsystem/host-dependencies.html seL4微內(nèi)核入門(mén)-代碼下載運(yùn)行及資料

3.2 rust環(huán)境安裝

然后是Rust安裝，執(zhí)行命令：

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編譯器安裝

執(zhí)行：sh scripts/build-sparrow.sh aarch64 會(huì)提示編譯工具找不到，如下：



打開(kāi)： https://developer.arm.com/downloads/-/gnu-a



下載后解壓到文件夾，然后把路徑添加到環(huán)境變量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

多次執(zhí)行sh scripts/build-sparrow.sh aarch64，修正后會(huì)出現(xiàn)如下：

表示編譯成功，下面就是運(yùn)行了。

4.運(yùn)行

cd build-aarch64
./simulate -M raspi3b

修改代碼：



重新編譯運(yùn)行，會(huì)看到打印出來(lái)。

這里的adder項(xiàng)目是camkes的，不是Sparrow框架的，上面說(shuō)過(guò)Sparrow還沒(méi)開(kāi)源，可能是其基于RISC-V硬件實(shí)現(xiàn)的，還沒(méi)有用qemu搞。

后記：

本文算是對(duì)最新的OS技術(shù)進(jìn)行一些探究，這個(gè)KataOS跟SeL4很有淵源，后續(xù)會(huì)繼續(xù)研究下。






審核編輯：劉清