Funding
Our Partners
Carrels:
Secure Containerisation for High-Assurance Microservices
Aim
Develop a framework for secure microservices on LionsOS, and harden un-verified services against attacks on memory errors.
Context
Containerisation has become a popular approach for deploying software. Using containerisation platforms, such as Docker and Kubernetes, developers can construct standalone computing units that can be deployed portably and scaled to meet the necessary workloads, reducing the cost and complexity of computing system operations. Compared to virtualisation, containerisation requires less software (e.g., no guest operating system), reducing dependencies that may cause maintenance and portability problems. Gartner predicts that by 2027, 85% of global organisations will be running containerized applications in production.
However, applying containerisation still has risks. While modern containerisation removes the need for the guest operating system required in virtualisation, containerised systems are still prone to exploitation through kernel vulnerabilities. For example, dozens of critical vulnerabilities are reported for Linux each year. The kernels on which containerized systems run are large, monolithic systems, where a single kernel vulnerability places all the hosted containers at risk.
Thus, the ability of the host kernel to protect itself from compromise and ensure isolation among containers is of paramount importance. The seL4 microkernel is the world's first formally verified operating system kernel. It is highly performant and remains the most thoroughly formally assured kernel, and is mature enough to have been deployed across a variety of critical systems across defence and business. This makes it the best foundation for secure containerisation.
Objectives
We aim to develop Carrels, a prototype of a secure, seL4-based microservices framework, which satisfies the following objectives:
- Each microservice can be started and stopped independently.
- New instances of each microservice can be started with different access rights, such as access to additional sensors, or accessing a cloud service with a different identity.
- Performance is at least as good as Linux containers, in terms of spin-up and spin-down latency, and overall latency of microservice execution.
- TCB components are verifiable.
- Memory safety of all Carrels subsystems will be explicitly evaluated.
Approach
Carrels is based on LionsOS, a highly modular, high-performance, seL4-based OS designed for formal verification. LionsOS provides protection domains (PDs) as the core execution abstraction, which are very lightweight (compared e.g. to Linux containers) and map to seL4-enforced isolation boundaries.
A Carrels system is configured with a fixed number of proto-containers, from which containers can be instantiated by loading an ELF file. When a container terminates, it reverts back to a proto-container.
An ELF file for Carrels is linked against a library OS (libOS) that provides I/O services (networking and storage) to the container (and optionally a console for debugging). The executable that is loaded into a container contains a list of signed capabilities that authorize any external (I/O) services the container may use.
Containers that need provide a level of compatibility that cannot be achieved with a libOS can be configured as full virtual machines (VMs) running a stripped- down Linux guest. VMs in Carrels are far more lightweight than on, say, KVM, although the host boot time limits the spin-up speed.
Microservices can be implemented in C, Rust or Python (as far as supported by MicroPython).
Status
The project has commenced in April 2025.
Support
The project is financially supported by the US Air Force Research Laboratory (AFRL).
Collaborations
Carrels is a collaboration between TS and the group of Trent Jaeger at UC Riverside.