バグフリーマイクロカーネルのseL4がバージョン7.0.0をリリース

seL4マイクロカーネルのバージョン7.0.0がリリースされた。付属するCMakeベースのビルドシステムにより、アウト・オブ・ソースのビルドとインタラクティブなコンフィギュレーションをサポートする。今回のリリースには、スタンドアロンのiae32ビルドとaarch64用のドキュメントも含まれている。

seL4はエンドツーエンドの証明に裏打ちされた強力なアイソレーションを保証する、高品質のマイクロカーネルである。これは事実上、証明済みの前提条件が成立する限り仕様通りの振る舞いを見せるという意味において、seL4のコードベースがバグフリーであるということでもある。それによって、信頼性の高い重要なコンポーネントを、同じプロセッサ上で動作する信頼性の低いコンポーネントから分離するために使用される。

seL4マイクロカーネルはNICTAが開発とメンテナンス、および初期の検証作業(現在はTrustworthy Systems Group at Data61)を行い、現在はGeneral Dynamics C4 Systems(GDC4S)が所有する。NICTAとGDC4Sは2014年、“より信頼性と安全性の高いコンピュータシステムの開発に寄与することを願って”、seL4をオープンソースとして公開した。

最初の機能検証(proof of functional correctness)は2009年にL4.verifiedプロジェクトによって行われ、正式なカーネル仕様が適切に実装されていることが確認された。その後の開発作業では、カーネルの包括的な公式検証を通じて、仕様が“可用性、権限管理、完全性、機密性”など、望ましい高水準のセキュリティ属性を満足していることと、それらの属性がコードおよびバイナリレベルへの転換後も有効であることを確認している。それらを合わせた結果として、汎用オペレーティングシステムとしては初めて、エンドツーエンドの証明が実現したのだ。特記すべきは、この証明がカーネルとともに10年間にわたって成長し進化していることである。この規模のソフトウェアとしては異例のことだ。

seL4カーネルは設計面において、高度なパフォーマンスを維持している。大量の検証作業への対応が、実際にはパフォーマンス最適化の一助となっているのだ。これまでの検証を通じて得た特性や定数が、カーネルの最悪実行時間(WCET)を解析するための情報となり、結果としてカーネルの実装改善を実現することで、WCETをさらに低減させている。また、同じ過程で追加されたファーストパスは、利用可能な場合にプロセス間通信(IPC)を自動的に高速化している。証明範囲も拡張されており、ファーストパス使用の有無に係わらず、カーネル動作が仕様に準拠していることが検証済みである。このような作業の結果として、防衛設備や自動車、医療機器、産業オートメーションなどのアプリケーション分野を持った、高速で安全で信頼性の高いカーネルが実現されている。

米国では、seL4に関連する防衛プロジェクトへの資金提供を目的とするSBIR(Small Business Innovation Research)プログラムを通じて、230万ドルを越える賞が授与された。そのようなプロジェクトのひとつであるSMACCMチームでは、“高いハック耐性を備えた”無人航空機(UAV)の開発にseL4を使用した。このチームではseL４を使って、クリティカルでないコードを実行する仮想Linuxインスタンスを、同じ“ミッションボード”上で動作する重要なコードから分離している。Red Teamによるハッキング試行に対して、Blue TeamはseL4ベースのシステムを効果的に運用することができた。当初は一般的なドローンを使って開発されていたが、後にボーイング社が開発した自立型ヘリコプタであるUnmanned Little Bird (ULB)に移管されている。しかし、seL4は軍事産業だけのものではない。Raspberry Pi 3でサポートされたことにより、安全でセキュアで信頼性の高いseL4ベースのシステムが、学生でも手の届くものになった。

seL4はセキュアなオペレーティングシステム開発の最先端を行くものだが、定義上は最小限のシステムである。さまざまなデバイスのサポートや簡易なプロセス間通信といった、Linuxなどフル機能のオペレーティングシステムを使用する時のような便利なものは含まれていない。

現在実施されている開発や検証作業のステータスは開発および検証ロードマップで公開されており、更新も頻繁に行われている。一般的な質問に対する回答は、プロジェクトのFAQページで確認できる。