seL4のAArch64対応でセキュリティ証明が完了

SeL4 security proofs now complete on AArch64

Proofcraftは、AArch64アーキテクチャ上でseL4マイクロカーネルの機密性（confidentiality）の証明を完了し、これにより機能的正しさ、完全性（integrity）、機密性を含むセキュリティ証明一式が揃いました。この成果は、アプリケーションがカーネル上で不正に情報を取得できないことを数学的に保証するもので、NCSCの支援を受けています。これにより、非クリティカルなアプリケーションへの攻撃がクリティカルなアプリケーションに波及するのを防ぎます。