RISC-V Foundation about verifying the operation of the microkernel on systems with RISC-V instruction set architecture. Verification comes down to reliability of seL4 operation, which indicates full compliance with the specifications specified in the formal language. Proof of reliability seL4 in mission-critical systems based on RISC-V RV64 processors that require an increased level of reliability and guarantee the absence of failures. Developers of software running on top of the seL4 kernel can be completely confident that if there is a failure in one part of the system, this failure will not spread to the rest of the system and, in particular, its critical parts.
The seL4 microkernel was initially verified for 32-bit ARM processors, and later for 64-bit x86 processors. It is noted that the combination of the open RISC-V hardware architecture with the open seL4 microkernel will achieve a new level of security, since the hardware components can also be fully verified in the future, which is impossible to achieve for proprietary hardware architectures.
When verifying seL4, it is assumed that the equipment works as stated and the specification fully describes the behavior of the system, but in reality the equipment is not free from errors, which is clearly demonstrated by regularly emerging problems in the mechanism of speculative execution of instructions. Open hardware platforms make it easier to integrate security-related changes - for example, to block all possible side-channel leaks, where it is much more efficient to get rid of the problem in hardware than to try to find workarounds in software.
Recall that the seL4 architecture moving parts for managing kernel resources into user space and applying the same access control means for such resources as for user resources. The microkernel does not provide ready-made high-level abstractions for managing files, processes, network connections, and the like; instead, it provides only minimal mechanisms for controlling access to 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. Access of such tasks to the resources available to the microkernel is organized through the definition of rules.
RISC-V provides an open and flexible machine instruction system that allows microprocessors to be built for arbitrary applications without requiring royalties or strings attached to use. RISC-V allows you to create completely open SoCs and processors. Currently based on the RISC-V specification by different companies and communities under various free licenses (BSD, MIT, Apache 2.0) several dozen variants of microprocessor cores, SoCs and already produced chips. RISC-V support has been present since the releases of Glibc 2.27, binutils 2.30, gcc 7, and the Linux kernel 4.15.
Source: opennet.ru