Picture this: A company who specializes in high assurance embedded systems has a customer who needs a specific set of specifications for an embedded core. The market does not offer any cores that meet this spec, and the system will need to run several virtual machines for the customer’s application.
Previously the smaller company only had two choices, neither of which are ideal. They could use a market core that supports virtualization but does not meet the customers requested spec, or create a custom RISC-V core but lose out on virtualization support.
With a seL4 microkernel based foundation and RISC-V architecture, DornerWorks is solving this problem, helping the company meet the customer’s core specifications and providing virtualization support on the core.
RISC-V is an open source, free instruction set architecture (ISA) that is seeing an increase in adoption rate year after year. The ISA started as a graduate project at UC Berkeley in 2010 and has quickly become a big player in the RISC architecture community.
According to Deloitte, the number of RISC-V processors is expected to double in 2022 and then double again in 2023. The reason RISC-V is becoming more popular is because it is completely free and fully open source. This means companies can design and manufacture their own custom implementations without paying any royalty or licensing fee, a big difference from most competitors.
As more implementations become available, and the acceptance of RISC-V continues to grow it, is important that those devices offer all the same capabilities that other devices can. One of those vital capabilities is virtualization which helps provide application isolation and reusability across different pieces of hardware. The seL4 microkernel provides not only the ability to virtualize but also high assurance due to its formal verification. While seL4 has been ported over to the RISC-V architecture before, virtualization on seL4 running on real hardware has not been done until now.
This post outlines how an seL4 guest was booted on a RISC-V soft SoC (System on Chip) and shows that RISC-V is a viable option for companies that need virtualization but want to avoid licensing fees and royalties.
Virtualization on RISC-V requires one of the ISA’s extensions, the H-Extension, where H is short for hypervisor. This extension is one of the newer additions to the instruction set and so the extension is not available in silicon yet. For this reason, the RISC-V Rocket chip SoC was chosen to run the guest on top of RISC-V seL4. The Rocket chip is a fully functional and customizable RISC-V SoC. It utilizes the Scala language to create configurations that are then compiled into an intermediate language that is then turned into Verilog. From there Xilinx’s Vivado tool can be leveraged to generate a bitstream that can be programmed to a variety of FPGAs. In this case the Xilinx ZCU102, a Zynq Ultrascale+ MPSoC(ZUS+) based development board, was used to run the soft SoC.
The design above shows how the Rocket chip can access the ZUS+ SoC’s system timer and UART ports, both of which are used to bring up the guest OS on top of seL4. All these connections were made by compiling the source Scala to Verilog and then generating the bitstream for the ZCU102. After the bitstream was generated, the design was programmed to the ZCU102 using the Xilinx Software Command-line Tool (XSCT) and JTAG.
Figure 2 shows the system stack all the way from the hardware to the Linux guest. The stack starts with the ZCU102 programmable logic (PL), which is where the Rocket chip bitstream is programmed. In order to begin the boot process, there needs to be a firmware that talks to the hardware through the supervisor binary interface (SBI). The point of the SBI is to provide an abstraction layer so that supervisor mode software is portable across different platforms. OpenSBI is an open-source implementation of the SBI and is widely used in the RISC-V community. The soft SoC then loads OpenSBI with the seL4 image attached as a payload. OpenSBI runs in the highest privilege mode machine mode (M Mode) like EL3 in the ARM architecture. OpenSBI does some initialization of the Rocket chip and then executes the payload.
This is when the seL4 hypervisor takes over and begins setup to launch the guest image.
The seL4 hypervisor is made up of two parts: the first is part is the microkernel code and the other is a virtual machine manager (VMM) application that runs in user mode. These two parts work together to handle traps and exceptions as well as emulate hardware for the guest OS. In order to setup for the guest, the hypervisor must map in devices, register interrupts, and load the guest image into RAM. After this the guest is then started and begins booting on top of the hypervisor.
The microkernel runs in hypervisor supervisor (HS) mode, which is used to communicate with the SBI, and correlates to EL2 from the ARM architecture. The guest and all its applications run in virtualized supervisor (VS) and virtualized user (VU) modes, respectively. VS mode acts just like supervisor mode but rather than interacting with the SBI directly it goes through the hypervisor. It also activates two stage address translation. VU mode acts much like user mode except that it also activates two stage address translation. VU and VS modes are only available when virtualization mode is enabled on the currently active hardware thread in RISC-V.
The two apps shown running on the guest can be any type of service that one might run on top of Linux. For instance, a web server that listens for sensor clients to perform a system diagnostic test on a vehicle and inform the driver if something is wrong.
As stated, this is the first time a virtualized guest has been booted on real hardware running RISC-V seL4. This is an important first step both for seL4 and the RISC-V architecture itself. As the ISA grows in adoption and the silicon begins to support the H-Extension, more companies will look to RISC-V for its virtualization capabilities. The work done here demonstrates that RISC-V can provide the same capabilities as its competitors with the advantage of being royalty free and fully open source.
A special thank you to the following people:
This was a team effort completed by: Robert VanVossen, Michael Doran, Lourens Willekes, and Eric Spidle
