分離コアが解放されました（分離カーネル）スイスの会社が開発したMuen コードラボ.
Muen は Intel x86_64 プラットフォームのみをサポートし、OS カーネルとその上で実行されているアプリケーションが、割り当てられたクォータを超えてリソースにアクセスできないようにします。これは、特に RAM、CPU 時間、I/O デバイスへのアクセスに当てはまります。
Linux カーネル、Ada/SPARK プログラム、および Solo5 フレームワークを使用して作成されたライブラリ OS (OCaml の MirageOS など) がゲスト アプリケーションとしてサポートされます。 PCI およびその他のホスト リソースへのアクセスを高速化するために、Linux 用のカーネル ドライバーが提供されています。
Muen 自体は、Ada 言語の安全なサブセットである SPARK で完全に実装されており、実行時エラーがないことが検証されています。コードは GPLv3 ライセンスに基づいて配布されます。
出所： linux.org.ru