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.
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, 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.
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.
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:
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.
