RISC-V財団 マイクロカーネルの動作確認について RISC-V 命令セット アーキテクチャを備えたシステム上。 検証は結局のところ、 seL4 動作の信頼性。これは、形式言語で指定された仕様に完全に準拠していることを示します。 信頼性の証明 seL4 は、高いレベルの信頼性を必要とし、障害がないことを保証する RISC-V RV64 プロセッサをベースとしたミッション クリティカル システムに使用されます。 seL4 カーネル上で実行されるソフトウェアの開発者は、システムの一部に障害が発生しても、この障害がシステムの残りの部分、特に重要な部分に広がることはないと完全に確信できます。
seL4 マイクロカーネルは、最初は 32 ビット ARM プロセッサに対して検証され、その後、64 ビット x86 プロセッサに対して検証されました。 オープン RISC-V ハードウェア アーキテクチャとオープン seL4 マイクロカーネルの組み合わせにより、将来的にはハードウェア コンポーネントも完全に検証できるようになるため、新しいレベルのセキュリティが達成されることに注意してください。これは、独自のハードウェア アーキテクチャでは達成することが不可能です。
seL4 を検証する場合、機器は記載どおりに動作し、仕様にはシステムの動作が完全に記述されていると想定されますが、実際には機器にエラーがないわけではありません。これは、seLXNUMX の投機的実行メカニズムで定期的に発生する問題によって明らかに示されています。説明書。 オープン ハードウェア プラットフォームにより、セキュリティ関連の変更の統合が容易になります。たとえば、考えられるすべてのサイドチャネル リークをブロックする場合、ソフトウェアで回避策を見つけるよりもハードウェアで問題を取り除く方がはるかに効率的です。
seL4 アーキテクチャを思い出してください。 カーネルリソースを管理する部分をユーザー空間に移動し、そのようなリソースに対してユーザーリソースと同じアクセス制御手段を適用します。 マイクロカーネルは、ファイル、プロセス、ネットワーク接続などを管理するための既製の高レベルの抽象化を提供せず、代わりに、物理アドレス空間、割り込み、プロセッサ リソースへのアクセスを制御するための最小限のメカニズムのみを提供します。 ハードウェアと対話するための高レベルの抽象化とドライバーは、ユーザーレベルのタスクの形式でマイクロカーネルの上に個別に実装されます。 マイクロカーネルが利用できるリソースへのこのようなタスクのアクセスは、ルールの定義によって組織化されます。
RISC-V は、使用料や使用条件を必要とせずに、任意のアプリケーション向けにマイクロプロセッサを構築できる、オープンで柔軟な機械命令システムを提供します。 RISC-V を使用すると、完全にオープンな SoC およびプロセッサを作成できます。 現在、さまざまな無料ライセンス (BSD、MIT、Apache 2.0) のもとで、さまざまな企業やコミュニティによる RISC-V 仕様に基づいています。 すでに数十種類のマイクロプロセッサコア、SoC、チップが生産されている。RISC-Vのサポートは、Glibc 2.27、binutils 2.30、gcc 7、およびカーネルのリリース以降に提供されている。 Linux 4.15.
出所： オープンネット.ru
