DevSecOps Enablement via High Assurance seL4 Microkernel

Containers have exploded in popularity due to their portability, modularity, and small overhead compared to virtual machines (VMs). This adoption has fueled design of DevSecOps pipelines in industry that enable a more rapid development cycle of systems with security baked in.  These same development practices can be applied to many commercial embedded devices, but there exists a wide range of applications for which container-based workloads are not an ideal match due to security, real-time, I/O, and many other requirements. Using a high assurance type 1 hypervisor such as the formally proven seL4 hosting virtual machines can provide security and isolation assurances baked in from the start, and using containers within these virtual machines can provide significant development flexibility while also taking advantage of the greater isolation benefits of virtual machines.  The DornerWorks VMComposer tool helps developers, design, configure, and deploy virtual machine-based systems.  The proposed work seeks to extend this support to include containers in order to allow DevSecOps workloads to be quickly deployed to embedded devices and allow the user to make intelligent trade-offs between running an individual application in a container or a virtual machine on the embedded target. DornerWorks also intends to explore unikernels as a potential middleground between virtual machines and containers, since they can be used to create light weight VM packages comparable to containers supporting micro-services while increasing performance and security by removing the need for a GPOS.