Fast, Secure, Adaptable: LionsOS Design, Implementation and Performance

TL;DR

LionsOS tackles the challenge of building a high-assurance OS for security- and safety-critical embedded systems by basing its design on the formally verified seL4 microkernel and enforcing radical simplicity through strict modularity and use-case-specific policies. The system uses a static architecture with fine-grained separation of concerns, SPSC queues, and per-client virtualisers to isolate devices while enabling high performance, even on system-call intensive workloads. Empirical results show LionsOS can outperform Linux on networking tasks and scales across Arm and x86 platforms, aided by driver VMs for legacy device support and a lightweight, per-client file system and networking stack that stay out of the TCB. The work demonstrates that modularity and verification-friendly design can coexist with high performance in embedded contexts, and the open-source LionsOS release provides a practical path toward dependable, configurable, and extensible secure OS components for cyber-physical systems.

Abstract

We present LionsOS, an operating system for security- and safety-critical embedded systems. LionsOS is based on the formally verified seL4 microkernel and designed with verification in mind. It uses a static architecture and features a highly modular design driven by strict separa- tion of concerns and a focus on simplicity. We demonstrate that LionsOS achieves excellent performance on system-call intensive workloads.

Figures (7)

• Figure 1: Memory regions for Ethernet: device control (Dev Ctl), device metadata (Dev MD), transmit and receive data (Tx Data, Rx Data), driver metadata (Tx D MD, Rx D MD) and virtualiser metadata (Tx V MD, Rx V MD). Arrows indicate access to regions by components, thick black arrows indicate DMA by the device, the thick coloured arrow indicates uncached access by the driver. The TxVirt only maps the Tx Data region if needed for cache management (shown as dashed). We only show a single client of the virtualiser.
• Figure 2: Driver-VM architecture
• Figure 3: Architecture of the LionsOS-based web server.
• Figure 4: Performance comparisons on i.MX8MQ UDP echo benchmark. Here and in other figures, the left axis and solid lines are throughput except where stated otherwise, dashed lines as per graph label (right axis).
• Figure 5: LionsOS vs Linux performance on x86_64 UDP echo benchmark. Dashed lines are CPU use except in graph b (RTT).