seL4のAArch64対応でセキュリティ証明が完了
SeL4 security proofs now complete on AArch64
Proofcraftは、AArch64アーキテクチャ上でseL4マイクロカーネルの機密性（confidentiality）の証明を完了し、これにより機能的正しさ、完全性（integrity）、機密性を含むセキュリティ証明一式が揃いました。この成果は、アプリケーションがカーネル上で不正に情報を取得できないことを数学的に保証するもので、NCSCの支援を受けています。これにより、非クリティカルなアプリケーションへの攻撃がクリティカルなアプリケーションに波及するのを防ぎます。
この隔離により、非クリティカルなアプリケーションへの攻撃がクリティカルなアプリケーションに波及して侵害することを防ぎます。
HNでの議論
52- StilesCrisis
もうすぐ来るぞ：この結果を完全に無効化するサイドチャネルタイミング攻撃。
- i_am_a_peasant
細かい文字を読め、「非MCS（混合臨界度システム）、ユニコア」だ。
- kvuj
どのOSがseL4を使っている？私が知っているのは以下の通り：
- GenodeOS
- LionsOS
- 中国の自動車メーカーが車載ハイパーバイザーとして使っていた、確か
- 他には？君たちが知っている民間での導入例はある？
- avadodin
組み込み市場と軍事市場は当面彼らに資金を提供し続けるかもしれないが、もし彼らのケーパビリティモデルでシステムのセキュリティを本当に改善していると正直に主張したいなら、ネイティブのseL4/Linuxが必要だ。
今やセキュアブート仮想化プラットフォームは掃いて捨てるほどある。