2015年、アメリカの会社Rockwell Collinsは、ボーイングおよび3D-Roboticsとともに、耐タンパー性のアイリスクワッドコプターとリトルバード無人ヘリコプターを「信頼性の高い」オペレーティングシステムでテストしました。
防犯ドローンの開発は、米国国防総省の高度防衛プロジェクト庁（DARPA）によって委託されています。DARPAは、潜在的な脆弱性から高度な無人およびオプションの有人航空機を保護することに関心があります。
無人航空機のハッキングには、少なくとも3つの方法があります.1つ目は、通信チャネルのハッキングまたは認証データのスプーフィングによって制御へのアクセスを取得する方法、2つ目はソフトウェアの脆弱性を使用する方法、3つ目は元のソフトウェアインターフェイスとデータチャネルを使用して悪意のあるコードをダウンロードする方法です。
seL4マイクロカーネルに基づいてロックウェルコリンズが開発したオペレーティングシステムは、3種類すべてのハッキングに耐性があります。 seL4ベースのオペレーティングシステムは、当初は主にセキュリティに焦点を合わせていました。 英語では、これは美しいフレーズ「ハックプルーフ」（盗難防止）と呼ばれます。
その機能は、コードスプーフィングに耐性のあるカーネルであり、数学的なアルゴリズムとチェックサムを使用して実行中のサービスをチェックし、プロセスの個別の実行も提供します。
システムを使用すると、ゲストプログラムがメインプロセスまたはハードウェアにアクセスできない仮想マシンを起動できます。 プログラムが起動すると、チェックサムがカーネルに報告され、それに基づいてエラーが修正されるか、不正なプロセスが閉じられます。
テストは成功しました。サイバーセキュリティの専門家は、安全なオペレーティングシステムを搭載した無人車両で悪意のあるコードを実行することも、ドローンの制御を奪ったり、システム障害を引き起こすこともできませんでした。
seL4マイクロカーネルは、航空だけでなく、医療、金融セクター、エネルギー、および故障がないことの保証が必要なその他の分野でも使用されています。
seL4アーキテクチャの重要な機能は、カーネルリソースをユーザースペースに管理するためのパーツを削除し、これらのリソースに対してユーザーリソースと同じアクセス制御方法を使用することです。 マイクロカーネルは、ファイル、プロセス、ネットワーク接続などを管理するための既製の高レベルの抽象化を提供しません。
代わりに、物理アドレス空間、割り込み、およびプロセッサリソースへのアクセスを制御するための最小限のメカニズムのみを提供します。
機器と対話するための高レベルの抽象化とドライバは、ユーザーレベルで実行されるタスクの形式でマイクロカーネルの上に個別に実装されます。 マイクロカーネルで使用可能なリソースへのこのようなタスクのアクセスは、ルールの定義を通じて編成されます。
プログラマーには、コンポーネント指向のアプリケーション開発プラットフォームCAmkESがあります。これにより、相互作用するコンポーネントのコレクションの形でseL4に基づいてシステムをシミュレートおよび作成できます。
L4アーキテクチャで正式に検証されたコアであるL4.verifiedプロジェクトは、 seL4に遺伝的にリンクされています。
L4は、1993年にJochen Lidtkeによって開発された第2世代のマイクロカーネルです。L4マイクロカーネルのアーキテクチャは成功しています。 多くのABIおよびL4マイクロカーネルAPI実装が作成されています。 すべての実装は、「L4小核ファミリー」と呼ばれるようになりました。 そのため、seL4がありました。 そして、Lidtkeの実装は「L4 / x86」と非公式に命名されました。
seL4と同様に、L4.verifiedの主なアイデアは、カーネル実装の正確性を数学的に証明することです。 実際、GNU / Linuxのようなモノリシックモジュラーモンスターとは異なり、マイクロカーネルは非常に小さいサイズです。 もしそうなら、それらは正式に検証することができます。 コードの各行は、証明が必要な数学的ステートメントに関連付けられています。
L4.verifiedのマイクロカーネルは、モデル実装の適合性、永続的なサイクルの欠如、およびその他のことを証明します。 この調査の費用は約600万ドルで、プロジェクトは7年間続きました。 作業量は25人年に達しました。
メインアプリケーション（seL4と同様に安全性）に加えて、L4は他の分野でも使用されています。 そこで、クアルコムは、 NICTAが開発したL4マイクロカーネルの実装を、「モバイルステーションモデム」（ MSM ）と呼ばれるチップセットで開始しました。 これは2005年11月にNICTAの代表者によって発表され、2006年末にMSMチップセットが販売されました。 そのため、L4マイクロカーネルの実装が携帯電話に登場しました。
信頼性の高いソフトウェアを作成するという問題は、アプリケーションの大半がネットワーク上で動作し、大量のデータを処理するようになったときに特に重要になりました。 そして、このデータは多くの場合機密です。
信頼性の高いオペレーティングシステムを作成する際の正式な検証の役割については、ネットワーク上にあまり資料がありません。 さらに少ない詳細な議論。 したがって、以下は、このトピックに関する記事に関する会話の1つの主な考えと議論です。
- 検証ツールとその有能な実装の配布により、あらゆるソフトウェアのあらゆるクラスのエラーを取り除くことができます。 たとえば、「バッファオーバーフロー」などのエラーは、必要なパラメータをチェックするだけで防止できます。
そこにはまだバグがあり、解説者の一人はこの資料を参照して結論付けています 。
- seL4コードにはある程度の信頼性があると言われています。 ハッキングから完全に保護されたOSの作成がユートピアである場合、なぜDARPAのようなクールなチームがこれを続けるのですか？
- ハッカーが検証済みのコードをスリップさせた場合はどうなりますか？ それとも不可能ですか？ すべてのOSに、ハッカーが間違いなく使用できるバグがあるのはなぜですか？
- なぜコード検証をハッキング保護と結び付けなければならないのですか？ 不可能は何ですか？ コードの検証とハッキングに対する保護は、たまにしか交差しない2つの異なるタスクです。
トロイの木馬、サイバー強要、フィッシング、クリックジャッキングは、アプリケーションのプログラムコードまたはオペレーティングシステム全体のエラーの有無に関係なく機能する攻撃の一種です。 そして、ユーザーが弱いパスワードを選択した場合はどうなりますか？ これもソフトウェア開発者のせいですか？
- 誰も研究者へのアクセスを許可したことがないため、実験は現実と矛盾しています。 このようなシステムでは、管理者以外の人がコードを挿入できないように注意深く監視する必要があります。
- わあ！ 適切に作成され、テストされたアプリケーションは、クラックするのが非常に困難です。 誰が考えていたでしょう...実際には、プログラムコードはすでに数学的に検証された構造で構成されています。
- 検証済みのコードを開発するのは、ほとんど手に入らない贅沢です。 そして、そのメンテナンスと変更の継続的な導入はさらに贅沢です。
- 管理の観点から見ると、プログラマは多くの場合双極的に行動します。 大規模な開発タスクをサブタスクに分割するように求められたとき、彼らは簡単に同意します。 しかし、可能性のある間違いについて事前に考えて体系的に防止するように彼らに申し出た場合、反応はまったく異なります。「それは非現実的」、「あなたはすべてを予見しません」、「それはどうですか？」、「それはどうですか？」...誰もが考えたいとは限りません事前にコードの品質。
- しかし、検証ツール自体にエラーが含まれている場合はどうでしょうか？ 検証者は誰が検証しますか？
- 純粋な数学には「バグ」はありません。 ゼロで割ることが不可能であるという規則がある場合、分母がゼロである場合は単に考慮されません。 実際には、この手法は機能しません。 ソフトウェア開発について話をしているのであれば、プログラムが「気に入らない」価値観でさえも働かなければなりません。 ゼロで除算した結果は無限大です。 そして、あなたはそれを使って何かをする必要があり、そのような結果ができないと言うことはしないでください。
PSもちろん、あなたは無限に議論することができます。 しかし、DARPAなどの大規模な組織がこれらのプロジェクトを実装するための具体的な手順を実行する場合、このストーリーは少なくともフォローアップされ、少なくとも関与する必要があります。
seL4のソースコードは、まだGitHubで入手できます 。