谷歌宣布發現了與 KataOS 專案相關的進展，旨在為嵌入式硬體創建安全操作系統。 KataOS系統元件採用Rust編寫，運行在seL4微核心之上，並在RISC-V系統上提供了可靠性的數學證明，表明程式碼完全符合形式語言中指定的規範。 此專案代碼在 Apache 2.0 許可證下開放。
該系統提供對基於RISC-V和ARM64架構的平台的支援。 為了在硬體之上模擬seL4和KataOS環境的運行，在開發過程中使用了Renode框架。 作為參考實現，提出了 Sparrow 軟體和硬體複合體，將 KataOS 與基於 OpenTitan 平台的安全晶片結合。 所提出的解決方案可讓您將經過邏輯驗證的作業系統核心與使用 OpenTitan 平台和 RISC-V 架構建構的值得信賴的硬體元件（RoT，信任根）結合。 除了KataOS代碼之外，未來還計劃開放所有其他Sparrow組件，包括硬體組件。
該平台的開發著眼於專用晶片的應用，這些晶片旨在運行機器學習和處理機密資訊的應用程序，這需要特殊級別的保護和確認不存在故障。 此類應用的範例包括操縱人物影像和錄音的系統。 KataOS 採用可靠性驗證，確保如果系統的某一部分發生故障，故障不會蔓延到系統的其餘部分，特別是核心和關鍵部分。
seL4 架構的著名之處在於將管理核心資源的部分移至使用者空間，並對此類資源套用與使用者資源相同的存取控制工具。 微核心不提供用於管理文件、進程、網路連接等的現成的高級抽象；相反，它僅提供用於控制對物理位址空間、中斷和處理器資源的存取的最小機制。 用於與硬體互動的高級抽象和驅動程式以用戶級任務的形式在微內核之上單獨實現。 此類任務對微核心可用資源的存取是透過規則的定義來組織的。
為了提供額外的保護，除了微內核之外的所有元件都是使用安全編程技術在Rust 中原生開發的，可以最大限度地減少記憶體錯誤，這些錯誤會導致釋放後記憶體存取、空指標取消引用和緩衝區溢等問題。 seL4環境中的應用程式載入器、系統服務、應用程式開發框架、用於存取系統呼叫的API、進程管理器、動態記憶體分配機制等都是用Rust編寫的。 驗證的程序集使用由 seL4 專案開發的 CAmkES 工具包。 CAmkES 的元件也可以在 Rust 中建立。
Rust 透過引用檢查、物件所有權和物件生命週期追蹤（範圍）以及在執行時間評估記憶體存取的正確性來強制編譯時的記憶體安全。 Rust 還提供針對整數溢位的保護，要求變數值在使用前初始化，預設使用不可變引用和變數的概念，並提供強大的靜態類型以最大限度地減少邏輯錯誤。
來源： opennet.ru