seL4 to PolarFire SOC demo
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
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 architecture. 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, 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.
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.
Find instructions on getting the code and running the demo yourself here: https://dornerworks.com/wp-content/uploads/2020/09/seL4-on-PolarFire-SoC-Instructions.pdf
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.
Follow DornerWorks on Twitter: https://twitter.com/DornerWorks
Follow DornerWorks on Linkedin: https://www.linkedin.com/company/dornerworks
Follow DornerWorks on Facebook: https://www.facebook.com/dornerworks
Engineering to help turn your ideas into reality.
Learn more about DorneWorks: https://DornerWorks.com
linux foundation
