Last week, the Data61 division of the Commonwealth Scientific and Industrial Research Organisation (CSIRO) in Australia released the first open source instruction set (RISC-V) version of the seL4 microkernel. The SeL4 microkernel project has a long history. In the beginning, the Data61 department was also the Australian national information and communication technology department to establish a micro-kernel that could verify security. Later, the project was renamed the open source kernel lab and in 2014 it released the first open source version of the seL4 microkernel.
According to the RISC-V organization’s plan, the federal scientific and industrial research organization is already a member of the organization, so it is possible to develop the industry standard architecture (ISA) chip structure together with other members. The RISC-V organization not only opens up the chip architecture but also provides a lot of reference materials. Because the chip structure designed by RISC-V organization is based on previous successful experience, the chip structure thus designed is clear.
Currently, RISC-V has become the seL4 microkernel, the third platform beside the Intel and ARM chip platforms. People have already talked about the Meltdown/Spectre hardware vulnerabilities of Intel chips. It is necessary to consider migrating chips to other structural platforms. The SeL4 microkernel works well on the native ARM platform and is being tested on the Intel platform. The next open source hardware platform testing will be steadily progressing.
The open source nature of the RISC-V platform allows the original complex chip structure to be accessible to everyone. Everyone can analyze the structure and find loopholes that may cause security problems. If countries or companies that did not have chip production capacity before, they can learn about the structural design of the chip through continuous learning in the community.
SeL4 microkernel spent 8 years to use Apple’s equipment, and now every year Apple’s purchases are in millions. The seL4 microkernel in the iPhone protects against unauthorized device attacks. However, since it is a micro-kernel, it also needs a lot of debugging for the device system to work. The specific features of many devices are implemented in the seL4 microkernel common userspace in Linux kernel-based systems.