Software security is a major concern for product developers, with the potential for data breaches and cyber-attacks becoming increasingly prevalent. Traditional software architectures are not equipped to handle these threats, leading to vulnerabilities that can be exploited by hackers. Additionally, hardware limitations can restrict the efficiency of software products, leading to slower and less reliable performance.
Because of this, software product development teams are constantly on the lookout for technologies that can enable more secure, reliable, and efficient software products.
The combination of seL4 and AMD Versal hardware is one such technology, which is revolutionizing the way development teams build secure software products.
The seL4 microkernel provides a secure foundation for the next generation of software enabled systems, ensuring that they are protected against vulnerabilities and cyber-attacks. Versal is a powerful platform that combines FPGA programmable logic with an AI engine, supporting demanding software workloads, and enabling developers to create faster and more efficient software products.
DornerWorks has experience developing products on the Versal platform, and in porting the seL4 microkernel to Versal, open up new possibilities for embedded systems designers and developers. Prior to this, the group ported seL4 to the Zynq UltraScale+ MPSoC.
As DornerWorks embedded engineer Zach Clark explains, running seL4 on Versal gives AMD customers a new option for advanced security in AI applications and beyond.
seL4 is a formally verified microkernel that provides a high degree of security and reliability for embedded systems. It offers strong isolation guarantees between components, preventing unauthorized access and ensuring that the system behaves predictably. This can be especially important in safety-critical systems where failures can have serious consequences.
Porting seL4 to Versal was not that dissimilar from the work required for running seL4 on the Zynq UltraScale+ MPSoC, Clark says.
“The main difference that presented itself was in the Generic Interrupt Controller v3, the virtual platform, whereas the MPSOC has an older version of the GIC,” Clark says. “We were not emulating that newer version of the interrupt controller. That was probably the biggest challenge that we came across was needing to add emulation of the newer version of the GIC rather than just being able to use the GIC v2 that the MPSoC used.”
Clark says overcoming this challenge was a highlight of the project for him.
“I learned the most about the GIC from the porting effort,” he says. “I had not really gotten into the emulation of the GIC at all before this. To go from never having worked with the virtual GIC to emulating a new version of the GIC was a new experience. I had to learn some things to be able to emulate that.”
The combination of seL4 and Versal offers strong memory protection and supports fine-grained access control for hardware resources. It also includes support for virtualization and can be used to create secure partitions for running multiple applications or operating systems on the same hardware. These features can be especially useful for applications such as avionics, and industrial control systems.
By building software products on the foundation of seL4 and Versal, product developers can enjoy a host of benefits, including:
Clark says the seL4 security features enabled by Versal are similar to those that the MPSoC can leverage. The main advantage the Versal platform brings to the table is being able to support robust AI applications.
“With other platforms, you might not have specific AI engines available to you that you have with Versal and seL4,” Clark says.
Using the Versal platform allows those AI resources to be shared across VMs running on an MPSoC whereas the same approach might be a challenge on other FPGAs.
seL4 on Versal can be an effective combination for several areas including safety-critical systems, virtualization, and secure IoT devices to name just a few. For another example, seL4 can be used to create secure partitions for running multiple applications or operating systems on the same hardware, which is useful in avionics, industrial control systems and automotive systems.
The seL4 microkernel is a cost-effective, open source solution you can use to build products on a trusted software base, and DornerWorks, a founding member of the seL4 Foundation, can accelerate your integration. We are leaders in accelerating integration of seL4 as the trusted software base for your product.
The formally proven seL4 ensures cyber resiliency for mission-critical systems. Its formal proof offers assurance that it is free of exploitable defects and has qualities of data integrity and confidentiality. With a VM-based software architecture, it enables isolation of software components and software redundancy. By sandboxing components and firewalling I/O outside of the operating system, it can mitigate “critical” legacy vulnerabilities.
DornerWorks offers a range of support and resources for developers who want to use seL4 on the Versal platform, including training, consulting, and development services. The seL4 community also provides extensive documentation, tools, and support for developers who want to use the microkernel in their projects.
The port of seL4 to AMD Versal hardware opens up new possibilities for secure and reliable embedded systems development and demonstrates the flexibility and portability of the seL4 microkernel. Developers interested in using seL4 on Versal can find a range of resources and support from DornerWorks and the seL4 community.
The combination of seL4 and Versal is a powerful technology that can revolutionize the way software products are developed. Consider using this combination for your next software product development project to experience the benefits firsthand, and schedule a meeting with our team when you are ready to accelerate development.
