seL4 オープン マイクロカーネル プロジェクトは、コンピュータ システムの分野で最も尊敬される国際組織であるコンピューティング機械協会 (ACM) によって毎年与えられる賞である ACM ソフトウェア システム賞を受賞しました。 この賞は、数学的動作証明の分野での業績に対して与えられます。これは、形式言語で指定された仕様に完全に準拠していることを示し、ミッションクリティカルなアプリケーションでの使用の準備が整っていることを認めます。 seL4 プロジェクトは、産業用オペレーティング システムのレベルでプロジェクトの信頼性とセキュリティを完全に正式に検証できるだけでなく、パフォーマンスと汎用性を犠牲にすることなくこれを達成できることを示しました。
ACM ソフトウェア システム賞は、新しい概念の導入や新しい商用アプリケーションの開拓など、業界に決定的な影響を与えたソフトウェア システムの開発を表彰するために毎年授与されます。 賞金は35米ドルです。 過去数年間、ACM 賞は GCC プロジェクトと LLVM プロジェクト、およびその創設者である Richard Stallman 氏と Chris Latner 氏に授与されてきました。 他に受賞したプロジェクトとテクノロジには、UNIX、Java、Apache、Mosaic、WWW、Smalltalk、PostScript、TeX、Tcl/Tk、RPC、Make、DNS、AFS、Eiffel、VMware、Wireshark、Jupyter Notebooks、Berkeley DB、eclipse がありました。 。
seL4 マイクロカーネルのアーキテクチャは、ユーザー空間でカーネル リソースを管理する部分が削除されていることと、そのようなリソースに対してユーザー リソースと同じアクセス制御手段を適用していることが注目に値します。 マイクロカーネルは、ファイル、プロセス、ネットワーク接続などを管理するためのすぐに使用できる高レベルの抽象化を提供せず、代わりに、物理アドレス空間、割り込み、プロセッサ リソースへのアクセスを制御するための最小限のメカニズムのみを提供します。 ハードウェアと対話するための高レベルの抽象化とドライバーは、ユーザーレベルのタスクの形式でマイクロカーネルの上に個別に実装されます。 マイクロカーネルが利用できるリソースへのこのようなタスクのアクセスは、ルールの定義によって組織化されます。
出所： オープンネット.ru