seL4 on PolarFire SOC Provides a Trusted Base for Defense, Industrial and Medical Products
Trusted software applications can keep a pilot safer in the air, industrial processes running more efficiently, and your medical device protected. These applications involve mission-critical processes that can’t be interrupted by vulnerabilities. They must be securely isolated from concurrent processes and less trusted software—all on hardware with size, weight, and power constraints.
A challenge, indeed, but not impossible.
The fact is, reduced SWaP does not have to come at the cost of application security. The combination of?Microchip’s PolarFire SoC ?and the?seL4 microkernel ?is proof in more ways than one.
Building products with the PolarFire SoC Icicle Kit from Microchip
The?PolarFire SoC ?is the first commercially available multi-core FPGA System-on-Chip that can support these mixed-criticality systems on open source Linux and the?RISC-V ?Core IP from SiFive . It enables the determinism needed for real-time hardware applications, while living up to the interoperability promise of RISC-V. The Icicle Kit is putting PolarFire power into the hands of developers who are building them.
The seL4 microkernel provides a trusted base for critical software components built on these devices.
As one of Microchip’s Authorized Design Partners, with experience using Microchip silicon in products for IoT and space applications, our engineers had access to one of the early release PolarFire SoC Icicle Kits for this project.
Porting seL4 to the PolarFire SoC with Antmicro’s Renode
Even before this hardware was available, DornerWorks engineers used Antmicro’s?Renode ?emulator to port the seL4 microkernel to an emulated PolarFire SoC. The security properties of seL4 can be formally verified on RISC-V hardware, providing mathematical proof that the system will support and isolate software processes as expected. DornerWorks engineers also used Renode to port seL4 to the?HiFive unleashed expansion board , which uses the PolarFire FPGAs. The device trees between the HiFive unleashed expansion board and the Icicle Kit are nearly identical, especially where Ethernet networking is concerned, which reduced the complexity of this porting effort.
领英推荐
Porting seL4 to the PolarFire SoC using the Icicle Kit
When the PolarFire SoC Icicle Kit arrived at DornerWorks, we ran?seL4test ?on the board. The effort took a few days and, with a little tweaking, the reassuring, “All is well in the universe,” soon showed up in the debugging window verifying the seL4 port was successful.
To complete the port to the Icicle Board, we worked through the following:
OpenSBI, Uboot, and the Hart software services (hardware threads) were configured to be bundled together in the CMake build system. The Uboot component was initially built from a Yocto recipe targeting a seL4 image rather than Linux, but the completed port allows Uboot to be built within the seL4 build system, circumventing the need for Yocto altogether. This effort makes the booting run smoothly.
Find instructions on getting the code and running the demo yourself here:
Using this code yourself is easy because DornerWorks has developed a repo of helper scripts in a single build step. Simply insert an SD card with the image and turn on the board.
The PolarFire SoC will soon support seL4’s formal verification, making the most of the microkernel’s enhanced security potential.
This is an optimal time to incorporate the flexibility and power of the PolarFire SoC into your own designs either through prototyping with the Icicle Kit, or through design discussions with an experienced engineering partner.
DornerWorks is an inaugural member of the seL4 Foundation ?and a member of the?Linux Foundation ?with deep expertise in RISC-V development. Pairing the trusted application environments enabled by the seL4 microkernel with the PolarFire SoC is a natural fit for our team and paves the way for future trusted software innovation that could grow your business.
If you want to build your software on the trusted software base of seL4 accelerated by the PolarFire SoC,?schedule a meeting ?with us. We will collaborate on a plan to turn your ideas into reality.