Work on the mathematical formal verification of the reliability and safety of the microkernel seL4 on systems with AArch64 instruction set architecture has been completed. This verification involves a mathematical proof of the correct operation of seL4, demonstrating full compliance with the specified specifications in a formal language. The proof of reliability enables seL4 to be utilized in mission-critical systems based on ARM64 processors, offering a heightened level of security and ensuring the absence of failures.
The seL4 microkernel was initially verified for 32-bit ARM processors and later for 64-bit x86 and RISC-V processors. This verification ensures that any failures in one part of the system will not propagate to the rest of the system or its critical components. In terms of security, the verification confirms that the kernel provides adequate application isolation, preventing unauthorized access to information and containing potential compromises from spreading to critical applications.
The architecture of the SeL4 microkernel is notable for relocating parts responsible for managing kernel resources to user space and utilizing the same access control mechanisms for both kernel and user resources. Unlike traditional kernels, SeL4 does not offer pre-built high-level abstractions for managing files, processes, or network connections. Instead, it provides minimal mechanisms for regulating access to physical address space, interrupts, and processor resources. Higher-level abstractions and hardware interaction drivers are implemented separately as user-level tasks on top of the microkernel, with access to microkernel resources controlled through defined rules.