RISC-V Foundationは、検証したことを発表しました マイクロカーネルのしくみ システム内のseL4 命令セットアーキテクチャ RISC-V。 検証プロセスは、seL4の信頼性の数学的証明に還元されます。これは、形式言語で指定された仕様に完全に準拠していることを示します。
信頼性テストにより、SEL4をRISC-Vプロセッサに基づくミッションクリティカルなシステムで使用できるようになります RV64、これはより高いレベルの信頼性を必要とし、故障を保証するものではありません。
seL4カーネル上で実行されているソフトウェア開発者は、システムの一部で障害が発生した場合に、この障害がシステムの残りの部分、特にその重要な部分に広がることはないと完全に確信できます。
seL4について
seL4アーキテクチャ ユーザースペースでカーネルリソースを管理するためのパーツを削除することで注目に値します また、ユーザーリソースと同じアクセス制御方法をそのようなリソースに使用します。
マイクロカーネル 高レベルの抽象化を提供しません ファイル、プロセス、ネットワーク接続などを管理する準備ができていますが、代わりに 物理アドレス空間へのアクセスを制御するための最小限のメカニズムのみを提供します、割り込み、およびプロセッサリソース。
コンピューターと対話するための高レベルの抽象化とドライバーは、ユーザーレベルで実行されるタスクの形式で、マイクロカーネルの上に個別に実装されます。
マイクロカーネルで利用可能なリソースへのそのようなタスクのアクセスは、ルールの定義を通じて編成されます。
RISC-Vは、オープンで柔軟なシステムを提供します 機械命令の 控除を必要とせずに、任意のアプリケーション用のマイクロプロセッサを作成できます 使用条件を課すことなく。
RISC-Vを使用すると、完全にオープンなプロセッサとSoCを作成できます。 現在、RISC-V仕様に基づいて、さまざまな無料ライセンス（BSD、MIT、Apache 2.0）の下で、いくつかの企業やコミュニティが、すでに製造されているマイクロプロセッサコア、SoC、およびチップの数十のバリアントを開発しています。
RISC-Vのサポートは、Glibc 2.27、binutils 2.30、gcc 7、およびLinux4.15カーネルのリリース以来存在しています。
seL4マイクロカーネルテストについて
最初は、マイクロカーネル seL4は32ビットARMプロセッサで検証されました、そして、 後でx86ビットプロセッサの場合.
RISC-Vオープンハードウェアアーキテクチャとオープンマイクロカーネルの組み合わせが観察されます。 seL4は新しいレベルのセキュリティを実現します、将来のハードウェアコンポーネントも完全に検証できるため、独自のハードウェアアーキテクチャでは実現できません。
seL4をチェックするときは、ハードウェアが正しく機能している（つまり、指定されている）と想定する必要があります。 これは、そもそも明確な仕様があることを前提としていますが、すべてのハードウェアに当てはまるわけではありません。
しかし、そのような仕様が存在し、それが形式的である（つまり、そのプロパティに関する数学的推論をサポートする数学的形式に記述されている）場合でも、ハードウェアの動作を実際にキャプチャしていることをどのようにして知ることができますか？
現実には、そうではないと確信することができます。 ハードウェアは、どちらもバグがあるという点でソフトウェアと同じです。
しかし、オープンISAを持つことには、ロイヤリティフリーである以上の利点があります。 XNUMXつは、オープンソースハードウェアの実装を可能にすることです。
seL4をチェックするとき、機器は示されているように動作し、仕様はシステムの動作を完全に説明していると想定されますが、実際には機器にエラーがないわけではなく、投機的実行メカニズムの命令で定期的に発生する問題によってよく示されています。
オープンハードウェアプラットフォームは、変更の統合を簡素化します たとえば、セキュリティに関連して、サードパーティのチャネルを介して考えられるすべてのリークチャネルをブロックします。この場合、ソフトウェアで解決策を見つけるよりも、ハードウェアで問題を取り除く方がはるかに効率的です。
最後に、それについてもっと知りたい場合は、のメモを参照してください。 次のリンク。