针对基于 AArch64 指令集架构的系统，seL4 微内核的可靠性和安全性已完成形式化数学验证。验证过程包括对 seL4 运行正确性的数学证明，证明其完全符合形式化语言中定义的规范。该可靠性证明使得 seL4 能够应用于基于 ARM64 处理器的关键任务系统中，这些系统需要高安全性并保证无故障运行。
seL4 微内核最初针对 32 位 ARM 处理器进行了验证，之后又针对 64 位 x86 和 RISC-V 处理器进行了验证。验证确保即使系统某个部分发生故障，故障也不会扩散到系统的其他部分及其关键组件。在安全性方面，验证确认内核提供了适当的应用程序隔离级别，防止应用程序未经授权访问信息，并确保即使辅助应用程序遭到入侵，攻击也不会扩散到关键应用程序。
seL4 微内核的体系结构以删除在用户空间中管理内核资源的部分以及对此类资源应用与用户资源相同的访问控制方式而著称。 微内核不提供用于管理文件、进程、网络连接等的开箱即用的高级抽象，相反，它仅提供用于控制对物理地址空间、中断和处理器资源的访问的最小机制。 用于与硬件交互的高级抽象和驱动程序以用户级任务的形式在微内核之上单独实现。 这些任务对微内核可用资源的访问是通过规则的定义来组织的。
来源： opennet.ru
