Organization RISC-V Foundation on the verification of the microkernel operation on systems with the RISC-V instruction set architecture. Verification entails of the reliability of seL4, which indicates complete compliance with the specifications defined in formal language. The proof of reliability seL4 in critical systems based on RISC-V RV64 processors that require a high level of reliability and guarantee the absence of failures. Software developers working on top of the seL4 kernel can be fully assured that in the event of a failure in one part of the system, this failure will not propagate to the rest of the system, particularly its critical components.
Initially, the seL4 microkernel was verified for 32-bit ARM processors and later for 64-bit x86 processors. It is noted that the combination of the open hardware architecture RISC-V with the open microkernel seL4 will achieve a new level of security, as the hardware components could also potentially be fully verified in the future, which is not achievable with proprietary hardware architectures.
During the verification of seL4, it is assumed that the hardware operates as declared and that the specification fully describes the system's behavior, but in reality, the hardware is not free from errors, as regularly demonstrated by persistent issues in the speculative execution mechanism. Open hardware platforms simplify the integration of security-related changes — for instance, to block all possible channels of leakage through side channels, where it is often more effective to solve the problem at the hardware level than to seek software workarounds.
Recall that the architecture seL4 by offloading parts for core resource management into user space and applying the same access control tools for 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 only provides minimal mechanisms for managing access to physical address space, interrupts, and CPU resources. High-level abstractions and drivers for hardware interaction are implemented separately on top of the microkernel in the form of tasks executed at the user level. Access for these tasks to resources available to the microkernel is organized through rule definition.
RISC-V offers an open and flexible instruction set architecture that enables the creation of microprocessors for arbitrary applications without requiring royalty fees or imposing usage conditions. RISC-V allows for the development of completely open SoCs and processors. Currently, various companies and communities are producing several dozen variants of microprocessor cores, SoCs, and chips based on the RISC-V specification under different open licenses (BSD, MIT, Apache 2.0). Support for RISC-V has been available since the releases of Glibc 2.27, binutils 2.30, gcc 7, and Linux kernel 4.15.
Source: opennet.ru
