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