先來說一個新聞：谷歌前幾天（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

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

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

表示編譯成功，下面就是運行了。

4.運行

cd build-aarch64
./simulate -M raspi3b

后記：

本文算是對最新的OS技術進行一些探究，這個KataOS跟SeL4很有淵源，后續會繼續研究下。






審核編輯：劉清