Google は、組み込みハードウェア用の安全なオペレーティング システムの作成を目的とした KataOS プロジェクトに関連する開発が発見されたことを発表しました。 KataOS システム コンポーネントは Rust で書かれ、seL4 マイクロカーネル上で実行されます。RISC-V システムでは信頼性の数学的証明が提供されており、コードが形式言語で指定された仕様に完全に準拠していることが示されています。 プロジェクト コードは、Apache 2.0 ライセンスに基づいて公開されています。
このシステムは、RISC-V および ARM64 アーキテクチャに基づくプラットフォームをサポートします。 ハードウェア上で seL4 と KataOS 環境の動作をシミュレートするために、開発プロセス中に Renode フレームワークが使用されます。 リファレンス実装として、KataOS と OpenTitan プラットフォームに基づくセキュア チップを組み合わせた Sparrow ソフトウェアとハードウェアの複合体が提案されています。 提案されたソリューションでは、論理的に検証されたオペレーティング システム カーネルと、OpenTitan プラットフォームと RISC-V アーキテクチャを使用して構築された信頼できるハードウェア コンポーネント (RoT、Root of Trust) を組み合わせることができます。 KataOS コードに加えて、将来的にはハードウェア コンポーネントを含む他のすべての Sparrow コンポーネントもオープンする予定です。
このプラットフォームは、特別なレベルの保護と障害がないことの確認が必要な、機械学習および機密情報処理用のアプリケーションを実行するように設計された特殊なチップへの応用を念頭に置いて開発されています。 このようなアプリケーションの例には、人物の画像や音声録音を操作するシステムが含まれます。 KataOS では信頼性検証を使用することで、システムの一部に障害が発生した場合でも、その障害がシステムの残りの部分、特にカーネルや重要な部分に波及しないことが保証されます。
seL4 アーキテクチャは、カーネル リソースを管理する部分をユーザー空間に移動し、ユーザー リソースと同じアクセス制御ツールをそのようなリソースに適用することで注目に値します。 マイクロカーネルは、ファイル、プロセス、ネットワーク接続などを管理するための既製の高レベルの抽象化を提供せず、代わりに、物理アドレス空間、割り込み、プロセッサ リソースへのアクセスを制御するための最小限のメカニズムのみを提供します。 ハードウェアと対話するための高レベルの抽象化とドライバーは、ユーザーレベルのタスクの形式でマイクロカーネルの上に個別に実装されます。 マイクロカーネルが利用できるリソースへのこのようなタスクのアクセスは、ルールの定義によって組織化されます。
さらなる保護のため、マイクロカーネルを除くすべてのコンポーネントは、解放後のメモリアクセス、null ポインタの逆参照、バッファ オーバーランなどの問題につながるメモリ エラーを最小限に抑える安全なプログラミング技術を使用して、Rust でネイティブに開発されています。 seL4環境のアプリケーションローダー、システムサービス、アプリケーション開発用のフレームワーク、システムコールにアクセスするためのAPI、プロセスマネージャー、動的メモリ割り当ての仕組みなどがRustで書かれています。 検証されたアセンブリでは、seL4 プロジェクトによって開発された CAmkES ツールキットが使用されます。 CAmkES のコンポーネントは Rust で作成することもできます。
Rust は、参照チェック、オブジェクトの所有権、オブジェクトの有効期間の追跡 (スコープ) を通じて、また実行時にメモリ アクセスの正確性を評価することによって、コンパイル時にメモリの安全性を強化します。 Rust は整数オーバーフローに対する保護も提供し、変数値を使用前に初期化する必要があり、デフォルトで不変参照と変数の概念を使用し、論理エラーを最小限に抑えるための強力な静的型付けを提供します。
出所： オープンネット.ru