seL4 on PolarFire SOC Provides a Trusted Base for Defense, Industrial and Medical Products

Posted on September 4, 2020 by Matthew Russell

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 Icicle Kit from Microchip.

The seL4 microkernel, developed by Data61, provides a trusted base for critical software components built on these devices.

Public access to the Icicle Kit was first announced via a crowdfunding campaign on CrowdSupply. As one of Microchip’s Authorized Design Partners, with experience using Microchip silicon in products for IoT and space applications, DornerWorks received one of the PolarFire SoC Icicle Kits before the official Sept. 15 release date.

Porting seL4 to the PolarFire SoC with Antmicro’s Renode

The four serial terminals show: Hart software services (upper left), Uboot (upper right), seL4 debug prints (lower left), and seL4 test user space (lower right).
OpenSBI is initialized on the system.
seL4test runs through a series of tests on the PolarFire SoC.

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.

The tests pass and “All is well in the universe.”

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:

  • New UART and timer drivers
  • Adjusted page size requirements to meet memory constraints
  • Corrected a mismatch between the kernel and the userspace libraries where seL4test was checking the wrong message registers in the fault handler.


OpenSBI, Uboot, and 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:
Porting seL4 to PolarFire SoC
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.

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 PolarFire SoC FPGAs, schedule a meeting with us. We will collaborate on a plan to turn your ideas into reality.

Matthew Russell
by Matthew Russell