cancel
Showing results for 
Show  only  | Search instead for 
Did you mean: 

Partner: seL4 Configs to Accelerate Secure Platform Development with Xilinx Hardware

Xilinx Employee
Xilinx Employee
0 0 696

Editor’s Note: This content is contributed by Matthew Russell, Marketing Specialist at DornerWorks

 

Accelerate Secure Software Solutions Using Pre-configured seL4 Packages

Verifying the security of your system can be difficult. In search of a trusted foundation for a single piece of software, repeated cycles of pen testing and iteration can extend development cycles far beyond what the market is willing to wait for. These tests can provide increased confidence in the security of an application but will also fall short of ever proving it. 

Let's face it. Customers aren't willing to risk their data security on a hunch that application security is possible. They want proof. Thankfully, the proof is available. 

 

Formal Verification Gives You Proof

Formal verification can be used to definitively prove the security properties of individual software applications, particularly those built using the seL4 microkernel.  This provides an opportunity to "set it, and forget it," trading hours of costly testing for mathematical proof and greater confidence.

One of the inaugural members of the seL4 Foundation, DornerWorks is a leader in helping companies accelerate the integration of the seL4 microkernel as the trusted base for their software. This most often looks like a custom-configured package developed for the customer, which they can plug into their system and use to grow their business. 

Here are two examples:

  1. VMM mode on ARMv8 - A DoD customer was interested in using seL4 as a hypervisor to provide robust security and isolation, and they wanted to run on the latest ARMv8 platform due to its performance and feature set. DornerWorks ported the existing ARMv7 virtualization support to an ARMv8 implementation and provided BSP layers for the Xilinx® Zynq® UltraScale+™ MPSoC platform. The prototype showed the isolation benefits that the customer required on the platform they needed.
  1. seL4 port to Xilinx Zynq UltraScale+ MPSoC - The Zynq UltraScale+ MPSoC has a quad-core Arm® Cortex®-A53, a dual-core Cortex-R5F, a GPU, and an FPGA. This chip is Xilinx’s most secure solution yet, with features like Secure Boot, Xilinx Memory Protection Unit (XMPU), and Xilinx Peripheral Protection Unit (XPPU). DornerWorks ported seL4 to the MPSoC, allowing it to be run as a Hypervisor, which is another means of reinforcing the budding seL4 ecosystem by allowing guest operating systems to run on top of seL4.

 

Accelerated Paths to Formally Verified Platforms

Trusted software foundations enabled by the seL4 microkernel are becoming the earmark of advanced software security features now in use by the U.S. Navy, U.S. Army, and companies in the defense, medical, and industrial markets. But the path to formal verification is not short. Configuring seL4 and deriving mathematical proof for a completely custom hardware design can take months, if not years. 

For those with more aggressive schedules in mind, DornerWorks has not only ported seL4 to Armv8 device, we have developed three tiers of virtual machine (VM) configurations that can provide a secure foundation, interoperability, and even real-time responsiveness for countless software solutions while maintaining all rigors of separation between VMs.

 

CONFIGURATION 1 - Lowest Cost

Avnet Ultra96 Dev Board with 2 Linux Virtual Machines

Configuration 1.jpg

This entry distribution is configured to run two separate instances of Linux OS on the low-cost Ultra96.

  • VM0 is exclusively allocated to the SD card after bootup, allowing your software to act as the gatekeeper to files that VM1 can access.
  • VM1 is allocated with sole access to the WiFi network interface, allowing you to control external access to VM0.
 

CONFIGURATION 2 - VM Workhorse

Xilinx ZCU102 Dev Board with 3 Linux Virtual Machines

Configuration 2.jpg

This distribution builds on our two VM versions by adding a third VM running your “secret sauce” on Linux on the more I/O capable ZCU102 board.

 

CONFIGURATION 3 - Highest Versatility

Xilinx ZCU102 Dev Board with 3 Linux VMs and 1 FreeRTOS Virtual Machine

Configuration 3.jpg

 

This distribution offers the versatile and capable mix of three Linux VMs and a real-time operating system VM. The RTOS VM has control of the CAN bus so you can handle those pesky CAN messages in real time.

The preconfigured options Include software binaries and instructions on an SD card and are available at: https://dornerworks.com/solutions/embedded-virtualization/sel4-microkernel/configurations/

Whether you’re just getting your feet wet with a few VMs or looking to build your products on a custom seL4 configuration using Xilinx devices, DornerWorks can help you enhance your system’s security by implementing the seL4 microkernel as the trusted base for your products.

Schedule a meeting with DornerWorks today and get started.