The RISC-V Foundation announced that it has verified how the microkernel works seL4 in systems with the instruction set architecture RISC-V. In which the verification process is reduced to the mathematical proof of the reliability of seL4, which indicates full compliance with the specifications specified in a formal language.
Reliability testing enables seL4 to be used in mission critical systems based on RISC-V processors RV64, which requires a higher level of reliability and does not guarantee failure.
Software developers that run on top of the seL4 kernel can be completely confident 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, in particular, to its critical parts. .
About seL4
The seL4 architecture is notable for removing parts to manage kernel resources in user space and use the same access control methods for such resources as for user resources.
The microkernel does not provide high-level abstractions already prepared to manage files, processes, network connections, etc., but instead only provides minimal mechanisms to control access to the physical address space, interrupts, and processor resources.
High-level abstractions and drivers for interacting with the computer are implemented separately on top of the microkernel in the form of tasks performed at the user level.
The access of such tasks to the resources available in the microkernel is organized through the definition of rules.
RISC-V provides an open and flexible system of machine instructions that allows to create microprocessors for arbitrary applications, without requiring deductions and without imposing conditions of use.
RISC-V allows you to create completely open SoCs and processors. Currently, based on the RISC-V specification, several companies and communities under various free licenses (BSD, MIT, Apache 2.0) are developing several dozen variants of already produced microprocessor cores, SoCs and chips.
RISC-V support has been around since the release of Glibc 2.27, binutils 2.30, gcc 7, and the Linux 4.15 kernel.
About the seL4 microkernel testing
Initially, the microkernel seL4 was verified for 32-bit ARM processors, and later for x86 64-bit processors.
It is observed that the combination of the RISC-V open hardware architecture with the open microkernel seL4 will achieve a new level of security, as the hardware components in the future can also be fully verified, which is impossible to achieve for proprietary hardware architectures.
When we check seL4, we must assume that the hardware is working properly (that is, as specified). That assumes there is an unambiguous specification in the first place, which is not the case for all hardware.
But even when such a specification exists, and it is formal (that is, ritten in a mathematical formalism that supports mathematical reasoning about its properties), how do we know that it actually captures the behavior of the hardware?
The reality is that we can be pretty sure that it is not. Hardware is no different from software in that both are buggy.
But having an open ISA has advantages that go beyond being royalty-free. One is that it allows open source hardware implementations.
When checking seL4, it is assumed that the equipment works as indicated and the specification fully describes the behavior of the system, but in fact the equipment is not error-free, which is well demonstrated by problems that regularly arise in the speculative execution mechanism Instructions.
Open hardware platforms simplify integration of changes related to security, for example, to block all possible leak channels through third-party channels, where it is much more efficient to get rid of a problem by hardware than to try to find solutions by software.
Finally, if you want to know more about it, you can consult the note in the following link
To me, this processor is something that calls me a lot. It only remains for some fat computer dog to make a computer that we can buy.
The ARM issue is something that squeaks me, we already saw what happened with Huawei with the sanctions. I am clear that for my RISC-V it is a much better solution at all levels. At the moment Huawei has already set its eye on it and perhaps in the future they will have equipment with this micro. If so, surely there will be more companies that adopt it and for me that would be the ideal and above all that the distros give support and not only ARM as happens with most.
+10