ついに完全達成！セキュアOS「seL4」のセキュリティ証明がAArch64に対応しました

究極の信頼性を誇るマイクロカーネル「seL4」にて、長らく待望されていたAArch64アーキテクチャ（ARM 64bit）向けの形式的検証（セキュリティ証明）が完了しました。これにより、ハイパフォーマンスなARM環境においても、数学的に証明された最高レベルのセキュアなシステム構築が可能になります。サーバーから組み込み開発まで、信頼性を最優先するエンジニアにとっての大きなマイルストーンです。

SeL4を使ってるOSって何があるの？今知ってるのはこれくらい。

• GenodeOS

• LionsOS

• 中国の自動車メーカーが車のハイパーバイザーとして使ってた気がする

• 他には何かある？誰かプライベートな環境での導入事例とか知ってる？

そのうちサイドチャネルタイミング攻撃でこの結果が完全に無効化される未来が見える

細部までちゃんと読まないと。「non-MCS (mixed criticality systems)、シングルコア」って書いてあるよ

組み込みや軍事分野からは当面の間資金援助が続くかもしれないけど、彼らのケーパビリティモデルでシステムのセキュリティを改善してるって本気で主張するなら、ネイティブなseL4/Linuxが必要だよね。

セキュアブート対応の仮想化プラットフォームなんて今やどこにでもあるし。