Work on the mathematical formal verification of the reliability and security of the seL4 microkernel on systems with the AArch64 instruction set architecture has been completed. The verification amounts to a mathematical proof of the correctness of the seL4 operation, which confirms its full compliance with the specifications given in formal languages. The reliability proof allows seL4 to be used in critical systems based on ARM64 processors, requiring a high level of security and guaranteeing the absence of failures.
Initially, the seL4 microkernel was verified for 32-bit ARM processors, and later for 64-bit x86 and RISC-V processors. The verification guarantees that in the event of a failure in one part of the system, this failure will not spread to the rest of the system and its critical parts. In the context of security assurance, the verification confirms that the kernel provides an adequate level of application isolation, prevents unauthorized access to information, and guarantees that in case of compromise of secondary applications, the attack will not spread to critical applications.
The architecture of the seL4 microkernel is notable for moving parts of kernel resource management into user space and applying the same access control mechanisms to these resources as for user resources. The microkernel does not provide ready-made high-level abstractions for managing files, processes, network connections, etc.; instead, it offers only minimal mechanisms for managing access to physical address space, interrupts, and CPU resources. High-level abstractions and drivers for interacting with hardware are implemented separately above the microkernel in the form of tasks executed at the user level. Access of these tasks to the resources available to the microkernel is organized through the definition of rules.
Source: opennet.ru
