Accelerate Secure Software Solutions Using Preconfigured 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 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, 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 a mathematical proof and greater confidence.

One of the inaugural members of the seL4 Foundation, DornerWorks is a leader in helping companies accelerate 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 in to their system and use to grow their business.

Here are a few short 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 AMD Zynq UltraScale+ MPSoC and the NXP i.MX8 platforms. The prototype showed the isolation benefits that the customer required on the platform they needed.
2. seL4 port to AMD Zynq UltraScale+ MPSoC – The Zynq UltraScale+ is a MultiProcessor System on a Chip that has a quad-core Cortex-A53, a dual-core Cortex-R5, a GPU, and an FPGA. This chip is AMD’s most secure solution yet, with features like Secure Boot, AMD Memory Protection Unit (XMPU), and AMD 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.
3. seL4 port to RISC-V platforms – Open source RISC-V hardware architecture has provided developers with a cost-effective platform on which to build products that can easily integrate with others in the rapidly growing RISC-V ecosystem. DornerWorks has ported seL4 to several RISC-V platforms including implementations with enhanced security features. The openness and expandability of RISC-V can provide added confidence beyond that already provided by seL4. The two combined make it possible to build enhanced security products that new devices and supercharged processing platforms like Microchip’s PolarFire FPGAs can harness.

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 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, x86 and RISC-V devices, 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

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

• VM0 is exclusively allocated the SD card after bootup, allowing your software to act as gate keeper to which files 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

AMD ZCU102 dev board with 3 Linux Virtual Machines

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

Configuration 3 – Highest Versatility

AMD ZCU102 dev board with 3 Linux VMs and 1 FreeRTOS Virtual Machines

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 the link below.
 
Get A Configuration

Whether you are just getting your feet wet with a few VMs or looking to build your products on a custom seL4 configuration, DornerWorks can help you accelerate the path to building products on the secure base of the seL4 microkernel.

Schedule a meeting with us today and get started.