DornerWorks

seL4 on PolarFire FPGAs 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.

seL4 engineer Jesse Millwood runs seL4test on the PolarFire SOC Icicle Kit from Microchip.

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

Even before this hardware was available, seL4 engineer Jesse Millwood 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. With the help of seL4 engineer Alex Pavey, Millwood 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 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.
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, Millwood 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, Millwood 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.

 


 
Pavey configured OpenSBI, Uboot, and the Hart software services (hardware threads) 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
 
The code will be upstreamed to the main seL4 repository and using it 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.

Soon, with the work of Data61, the PolarFire SoC will be able to support seL4’s formal verification, making the most of the microkernel’s enhanced security potential.

This is an optimal time for early adopters to provide important feedback that could guide future iterations of the Icicle Kit and its potential in embedded projects. It’s also 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.

Enabling Device Security with a Formally Verified Microkernel

It can take a lot of time and effort to verify that your system is secure, time and effort developers using the seL4 microkernel are spending on their design, instead.

Learn more about how the seL4 microkernel running on a PolarFire® SoC FPGA provides an excellent starting point for your next security-focused product in our upcoming Microchip SHIELDS UP! webinar (#22) and jump start your trusted application development.

REGISTER FOR THE WEBINAR

 

Matthew Russell
by Matthew Russell
Marketing Specialist
Matthew Russell is a marketing specialist at DornerWorks.