Work on the formal mathematical verification of the reliability and security of the seL4 microkernel on systems with the AArch64 instruction set architecture has been completed. Verification consists of a mathematical proof of the correctness of seL4 operation, which demonstrates full compliance with the specifications defined in the formal language. This proof of reliability enables the use of seL4 in mission-critical systems based on ARM64 processors that require a high level of security and guarantee 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. Verification ensures that if a failure occurs in one part of the system, it will not spread to the rest of the system and its critical components. In the context of security, verification confirms that the kernel provides the appropriate level of application isolation, prevents them from accessing information without authorization, and ensures that if secondary applications are compromised, the attack will not spread to critical applications.
The architecture of the seL4 microkernel is notable for the removal of parts for managing kernel resources in user space and for applying the same means of access control for such resources as for user resources. The microkernel does not provide out-of-the-box high-level abstractions for managing files, processes, network connections, and the like, instead it provides only minimal mechanisms for controlling access to the physical address space, interrupts, and processor resources. High-level abstractions and drivers for interacting with hardware are implemented separately on top of the microkernel in the form of user-level tasks. The access of such tasks to the resources available to the microkernel is organized through the definition of rules.
Source: opennet.ru
