seL4在AArch64上的安全证明终于完成

SeL4 security proofs now complete on AArch64

Proofcraft宣布，seL4微内核在AArch64架构上的安全证明已全面达成。在继功能正确性和完整性证明之后，团队成功建立了机密性（confidentiality）的数学证明，确保运行在seL4之上的应用程序无法未经授权获取信息。这一里程碑得益于NCSC的持续支持，标志着seL4在AArch64上的安全隔离机制得到形式化验证。此外，Proofcraft还在RISC-V架构上完成了seL4的MCS配置验证，并推出了支持动态域调度的新API，使信息流控制更加灵活。这些进展不仅推动了高可信系统的发展，也为汽车、航空航天等关键领域的应用提供了坚实保障。