高度な保証：seL4

ウィキペディア小見出し辞書

高度な保証：seL4

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/03/21 10:04 UTC 版)

「L4マイクロカーネルファミリー」の記事における「高度な保証：seL4」の解説

2006年にNICTAのグループはseL4と呼ばれる第3世代マイクロカーネルの設計を開始した。これはコモンクライテリア（Common Criteria：略称CC ISO/IEC 15408規格）を満たす、あるいはそれ以上のセキュリティ要件を満たすために高い安全性と信頼性が得られるような基本方針で設計された。最初からカーネルの形式的証明を目指して開発を行った。性能と検証の時に相反する要求を満たすために、チームはHaskellで書かれた実行可能な定義からソフトウェアによる処理を行いその結果を用る方法をとった。seL4ではオブジェクトのアクセス権についての形式的推論を可能にするために capability-basedアクセス制御 を用いている。 機能の正しさの形式的証明は2009年に完了した。この証明はカーネルの実装がその定義に対して正しいことを示し、従ってデッドロック、ライブロック（あるプロセスがbusy状態のまま実行権を放さなくなってしまう状態を指す）、バッファオーバーフロー、数値演算の例外、初期化していない変数の使用などの実装バグの無いことを意味する。seL4は汎用のOSカーネルとしては初めて証明されたという主張がなされている。 seL4は、カーネルリソースの管理に新しい方法をとっている。 カーネルリソースの管理はユーザーレベルに任され、ユーザーリソースと同じCapability-based securityのアクセス制御を受ける。このモデルはチューリッヒ工科大学による研究OSのBarrelfish（英語版）でも採用されたもので、プロパティ分離についての推論を容易にして、seL4がコアセキュリティプロパティの完全性と秘匿性を強制することを後に証明することを可能にするものとなった。 NICTAのチームはCから実行可能な機械語への変換の正確さの確認を行い、seL4のトラステッド・コンピューティング・ベースからコンパイラを取り除いた。これは実行可能なカーネルにおいて高度なセキュリティが証明されているという事である。seL4はまた、ハードリアルタイムシステムに必須な完全性と最悪ケースにおける正確な実行時間の解析を行ったと最初に公表された保護モードのOSカーネルである。 2014年7月29日、NICTA（英語版）とジェネラル・ダイナミクス・ミッション・システムズ（英語版）は隅から隅まで検証されたseL4をオープンソースでリリースした。カーネルコードと検証コードはGPLv2で提供され、ほとんどのライブラリとツールは2条項BSDライセンスで提供されている。研究者のコメントによれば、ソフトウェアの形式的証明のコストはより高い信頼性を提供するにも関わらず従来の「高度な保証」を有するソフトウェアを設計するコストよりも低いとしている。 具体的には、従来の「高度な保証」を有するソフトウェアでは1行あたりのコストは1000米ドルであるのに対し、開発中のseL4の1行あたりのコストは400米ドルと見積もられた。 NICTAはアメリカ国防高等研究計画局(DARPA)の高保証サイバー軍事システム計画（High-Assurance Cyber Military Systems(HACMS)の下でプロジェクトパートナーのロックウェル・コリンズ社、ガロア社、ミネソタ大学、ボーイング社と共同でseL4ベースの高保証ドローンを保証ツールとソフトウェアと共に開発した。これはボーイングで開発中の操縦も可能な自律型無人ヘリコプターボーイング AH-6への技術移転も計画されていた。最終的なHACMS技術のデモンストレーションは2017年4月、バージニア州スターリングで行われた。 DARPAはまたジョン・ランチベリー博士の提唱でseL4に関連した中小企業技術革新研究プログラム(SBIR)による出資を行った。seL4によるSBIRを受けた企業にはDornerWorks、Techshot、Wearable Inc、Real Time Innovations、Critical Technologiesなどがある。