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

Alwin Joshy; Anuraag Ganesh; Bill Nguyen; Cheng Li; Courtney Darville; Gernot Heiser; Guangtao Zhu; Ivan Velickovic; James Archer; Jingyao Zhou

REVIEW 3 major objections 6 minor 1 cited by

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

T0 review · 3 major / 6 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper claims the performance penalty of highly modular microkernel-based OSes is not inevitable: LionsOS, built on the formally verified seL4 microkernel, matches or beats Linux on UDP echo and storage workloads while using far less…

desk verdict LionsOS is a real, open-source microkernel OS with surprisingly strong UDP echo and storage numbers; the headline claim is probably right, but the Linux baseline fairness and missing variance are the soft spots a referee should push on. read the letter →

arxiv 2501.06234 v2 pith:BJTZ6LTI submitted 2025-01-08 cs.OS cs.CR

Gernot Heiser , Ivan Velickovic , Peter Chubb , Alwin Joshy , Anuraag Ganesh , Bill Nguyen , Cheng Li , Courtney Darville

show 7 more authors

Guangtao Zhu James Archer Jingyao Zhou Krishnan Winter Lucy Parker Szymon Duchniewicz Tianyi Bai

This is my paper · ORCID

classification cs.OScs.CR

keywords LionsOSseL4microkernelmodularoperatingsystemsembeddedseparationofconcernsIPCperformancedevicedrivers

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to overturn the long-held assumption that fine-grained modularity in microkernel-based operating systems inevitably carries a prohibitive performance cost. It presents LionsOS, an operating system for safety- and security-critical embedded systems that sits on the formally verified seL4 microkernel and is built from many small, single-purpose, address-space-isolated components communicating through simple lock-free queues. The paper claims this is the first such highly modular system to perform at par with or better than monolithic designs, and demonstrates it on system-call-intensive workloads: UDP echo networking, where LionsOS sustains full line rate with a large fraction of CPU to spare while Linux saturates at roughly half the throughput, and storage benchmarks with similar bandwidth at a fraction of Linux's CPU cost. LionsOS itself is not yet formally verified; the claim is that the extreme simplicity of its components makes verification achievable, and the paper already cites a verified NIC driver in the same style.

What carries the argument

The mechanism that makes the performance claim work is the combination of a static system architecture with single-producer-single-consumer (SPSC) shared-memory queues synchronised by semaphores. The seL4 Microkit fixes the system at configuration time as a set of single-threaded protection domains (PDs) with declared communication channels; LionsOS components then communicate only through bounded, lock-free SPSC queues, signalling a peer only when a queue changes between empty and non-empty (or full and non-full). All policy-independent state lives in shared memory, so a failed component can be restarted or even swapped for a different executable (a demonstrated 17 µs policy switch) without disturbing the rest of the system. Because no component ever blocks on another's internal state, components are location-transparent: a component cannot tell whether its peer runs on the same core or a remote one, so multicore scaling comes from distributing the small components across cores rather than from threading, and device drivers are reduced to pure hardware translation, with data buffers deliberately unmapped from the driver's address space.

What would settle it

Run the identical UDP echo benchmark with a carefully tuned Linux on the same board — minimal initramfs userspace, IRQ coalescing and busy-polling tuned to the offered load, the echo process pinned, and preemption configured for throughput — and compare throughput per core and round-trip latency. If tuned Linux matches or beats LionsOS on throughput and latency at equal CPU cost, the claim that modularity costs nothing would be falsified; the same test can be rerun with hardware offload features (Tx IRQ coalescing, checksum offload) re-enabled for the CEOS comparison to check that the disabled-features choice is not the source of the gap.

Watch

Extended reading notes

Core claim

The paper's central claim is that LionsOS is the first highly modular microkernel-based OS to achieve performance at par with or better than traditional monolithic designs, and that on context-switch intensive workloads — where modularity-imposed overheads should be greatest — it outperforms all systems compared against, including Linux, Genode, and a commercial microkernel OS (CEOS). The paper attributes this result to "radical simplicity": strict separation of concerns, least privilege, narrow interfaces, and use-case-specific policies produce components so small that their frequent context switches cost less than the interface layers and generality of monolithic designs. The evidence is quantitative: on an Arm i.MX8MQ platform LionsOS sustains the full 1 Gb/s NIC capacity with roughly one third of the CPU left unused, whereas Linux plateaus at about 500 Mb/s with its core saturated and round-trip times three to ten times higher; on x86 with a 10 Gb/s NIC, LionsOS keeps up with about 20% CPU spare while Linux saturates at 4 Gb/s. Simulated IPC costs from zero (free IPC) to Zircon-like prices change LionsOS's CPU utilisation only slightly, which the paper takes as evidence that context-switch cost is not the bottleneck the literature has assumed.

Load-bearing premise

The central performance claim rests on the fairness of the comparison: Linux, Genode, and CEOS must be reasonably well-tuned representatives of their designs, so that LionsOS's win reflects its architecture rather than under-configured rivals.

Editorial extensions

If this is right

If modularity no longer costs performance, isolation-heavy OS architectures become the natural choice for mixed-criticality embedded systems, since the security and safety benefits come without the traditional performance tax.
The simplicity of the small components makes formal verification tractable: a high-performance NIC driver written in the LionsOS style has already been verified with automated proof techniques, and the paper expects the rest of the small trusted computing base to follow.
Linux driver reuse inside small virtual machines (a few MiB of RAM for optimised configurations, weeks of effort per device class) gives LionsOS broad hardware coverage without sacrificing the isolation model, so device availability is not a barrier to adoption.
Runtime policy swapping (demonstrated at 17 µs for network traffic shaping) lets a static-architecture system change behaviour on the fly, so use-case-specific policies do not mean inflexible systems.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the performance advantage is really about simplicity rather than kernel speed, then porting the same protection-domain structure to a microkernel with deliberately inflated IPC latency should reproduce the same throughput, isolating the design principle from the processor's context-switch cost; the paper's simulated-IPC experiments suggest this test is cheap to run.
The use-case-specific policy principle implies the performance story may not transfer to general-purpose workloads: static resource allocation works because embedded systems do not over-commit, so on dynamic, unpredictable workloads the advantage over adaptive monolithic schedulers could shrink or even reverse.
The 17 µs policy swap suggests a broader design pattern for adaptive behaviour in critical systems: keep a small library of specialised policy modules and hot-swap them in response to events, rather than building one general policy with configuration knobs — a pattern that could also be applied to schedulers, cache partitioning, and power management.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Quick take: this is a serious systems paper, not vaporware. The authors built LionsOS on seL4 Microkit, shipped it open source, and run a real web server on it. The design principles—strict separation of concerns, least privilege, use-case-specific policies—are coherent, and the evaluation is much more than a toy: UDP echo against Linux, Genode, and CEOS on Arm and x86, plus storage and file benchmarks. The code-size comparison (LionsOS NIC drivers 400-670 SLOC vs Linux 3,000-10,000) is a concrete, reproducible point. The 'free IPC' simulation is explicitly rough, and they say so, which is good practice.

The two real soft spots. First, the Linux baseline may not be tuned. On Arm they use a stock Buildroot 6.1 kernel; on x86, a stock Debian 6.6 kernel with the performance governor. They don't report trying interrupt coalescing, IRQ affinity, socket buffer tuning, or the specific FEC driver settings. The stress-test note is right that a tuned Linux could close part of the gap. That said, the gap is large (LionsOS uses less than half the CPU at line rate, RTTs 3-10x lower), and Linux is given two threads on x86 without matching LionsOS. So I would not call the comparison invalid, but the claim 'outperforms all systems' is stronger than what the paper proves. It proves it against the configurations tested. That is a fixable weakness, not a fatal one.

Second, no error bars or run-to-run variance anywhere in Section 6. For a performance paper, that's a standard referee request. The graphs show single curves; we don't know if the SLOC ratios or the throughput gaps are stable across runs. This is minor to fix but should be in the revised version.

The benchmark coverage is narrow—UDP echo and block I/O—but the paper's claim is about system-call intensive workloads, and UDP echo is exactly that. I won't penalize it heavily.

Bottom line: the central argument holds up: a highly modular microkernel OS can be fast if the components are simple and the policies are tailored. The paper deserves a serious referee. I'd send it to review, and ask for tuned Linux baselines, error bars, and a statement about configuration details. It's a useful paper for anyone in embedded systems, seL4, or microkernel performance.

Referee Report

3 major / 6 minor

Summary. The paper presents LionsOS, an operating system for safety- and security-critical embedded systems built on the formally verified seL4 microkernel. The design is deliberately static and highly modular, with strict separation of concerns, least privilege, and use-case-specific policies. The authors report an implementation of Ethernet and storage subsystems using device drivers, virtualisers, and shared-memory SPSC queues, plus mechanisms for reusing Linux drivers in virtual machines. The evaluation compares LionsOS against Linux, Genode, and a commercial microkernel-based OS (CEOS) on UDP echo and block I/O workloads. The headline results are that LionsOS sustains line-rate UDP echo with substantially lower CPU utilisation and lower round-trip times than Linux on both Arm and x86, and that storage throughput is comparable to Linux while using less CPU at small block sizes. The paper also reports code-size comparisons, a dynamic policy-swap experiment, and a simulated analysis of IPC cost. The central claim is that LionsOS is the first highly modular microkernel-based OS whose performance is at par with or better than traditional monolithic designs on system-call intensive workloads.

Significance. If the performance claims hold, this is a significant result for the microkernel and verified-OS communities: it would show that fine-grained modularity, with many inter-component context switches, need not impose a prohibitive performance penalty. The paper is also useful as a systems design study, with concrete mechanisms (SPSC queues, virtualisers, location transparency, driver VMs) and an openly available implementation. The authors are explicit about the verification-friendly intent and provide code-size data and a reproducible benchmark methodology. The main empirical contribution, however, rests on the fairness of the Linux baseline and on the absence of run-to-run variance reporting, so the strength of the headline claim is currently not fully established.

major comments (3)

[Section 6.3.1, Figures 4 and 5] The central claim that LionsOS outperforms traditional monolithic designs is supported almost entirely by the UDP echo comparison against Linux, but the Linux baseline is not shown to be reasonably tuned. Section 6.1 states only that the Arm Linux runs a Buildroot system with kernel 6.1.0 and that the x86 Linux uses a Debian kernel 6.6.15-2 with the performance frequency governor. The paper mentions that Linux requires an Rx IRQ hold-off configuration and switches to polling under high load, but it does not report what tuning was attempted on the Linux side (e.g., interrupt coalescing, IRQ affinity, receive-side scaling, socket buffer sizes, or kernel configuration options). On the i.MX8MQ FEC controller, stock interrupt defaults can severely limit throughput, so the observed Linux plateau of about 500 Mb/s may not represent a well-configured monolithic baseline. Please repeat the comparison with a Linux configuration that has been explicitly tuned for this NIC and workload, report the specific settings, and state whether the qualitative conclusion (LionsOS uses less than half the CPU and has lower RTT) survives. Without this, the headline claim is vulnerable to the objection that an untuned baseline, rather than modularity, explains the result.
[Section 6.3.1, Figures 4-6] No error bars or run-to-run variance are reported anywhere in the networking evaluation. The curves in Figures 4, 5, and 6 appear to be single measurements, and the text reports precise-looking ratios (e.g., 'less than half the CPU', RTTs 'three to ten times less') without any indication of measurement spread or repeat count. Because the deltas are used to assert a large performance advantage, the paper should report at least the number of repetitions and the min/median/max (or confidence intervals) for the key curves, and should state how the load generator handles packet loss and measurement error. This is particularly important near saturation, where CPU utilisation and achieved throughput can be sensitive to timing artifacts.
[Section 6.3.1, Figure 5d and Section 7] The 'free IPC' simulation is explicitly acknowledged as imprecise ('We do not claim that this is in any way precise'), yet Section 7 uses it to conclude that IPC cost has only minor impact and to contradict prior claims that IPC cost is still a bottleneck. Adding fixed delays to seL4 system calls, or subtracting 493 cycles for 'free' IPC, is a coarse approximation of what would happen on Fiasco, Zircon, or a hypothetical zero-cost IPC system; it does not model differences in cache behaviour, scheduling, queue batching, or notification mechanisms. This experiment is useful as a sensitivity analysis, but the conclusion in Section 7 should be hedged accordingly, or the paper should provide a more direct comparison against at least one of the actual kernels. As written, the strength of the 'IPC cost matters little' conclusion exceeds what the methodology can support.

minor comments (6)

[Section 6.3.1, Figure 4 caption] The caption states that 'the left axis and solid lines are throughput except where stated otherwise', but Figure 4a shows CPU utilisation on the left axis and does not appear to follow this rule. Please clarify the axis assignment for each subfigure, or standardise the captions.
[Section 6.1 and Section 6.3.1] The term 'unicore' is used repeatedly; 'single-core' or 'uniprocessor' is the conventional term and would read more naturally.
[Section 6.3.2, Figure 7e] The text says the benchmark reads 4 files, while the figure shows 4 file positions, but then states that LionsOS 'is slower when reading more than five files'. This is internally inconsistent; please reconcile the number of files in the benchmark with the reported cross-over point.
[Section 6.3.1, Figure 5d] The methodology for the simulated Fiasco, Zircon, and 'free IPC' curves is described only in the text; adding a concise explanation in the figure caption would improve readability.
[Section 6.3.1, 'Other OSes' paragraph] The Genode comparison uses the 'hw' base configuration, which runs bare metal without a microkernel underneath, so it is not directly comparable to a microkernel-based design. The text acknowledges this, but the figure legend simply lists 'Genode'; please make the configuration difference explicit in the figure and in the corresponding discussion.
[Section 5.4 and Section 6.2.3] The driver-VM experiments report memory footprints and development effort, but not the latency overhead of the VM-based driver path. Since the text states that this path 'is unlikely to be an option for performance-critical devices', a quantitative latency or throughput comparison for at least one driver class would strengthen the claim.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central performance claims rest on direct measurements against independent external systems (Linux, Genode, CEOS) and on an explicitly labelled, rough IPC-cost simulation based on externally measured microkernel latencies.

full rationale

The paper's main contribution is an empirical performance evaluation, not a derived prediction. LionsOS throughput, CPU utilisation and latency are measured against Linux, Genode and CEOS using ipbench and iperf3; none of these baselines is produced by fitting a parameter to LionsOS data or by defining LionsOS's result in terms of the comparison. The 'free IPC' simulation is explicitly an estimate ('We do not claim that this is in any way precise') built from published, externally measured seL4, Fiasco.OC and Zircon round-trip latencies [Mi et al., 2019]; it is not fitted to LionsOS and the paper's headline claim does not depend on it. Self-citations appear (seL4 verification, seL4 Microkit, first steps in verifying the Core Platform, a verified NIC driver), but these are not load-bearing for the performance claim: the seL4 verification is machine-checked, the Microkit is described as the starting point rather than as evidence of performance, and the cited verified NIC driver is mentioned only in the conclusions as an outlook, not as support for the benchmark results. The design principles (KISS, separation of concerns, use-case-specific policies) are presented as an argument about why performance is achievable, but the actual demonstration is the independent evaluation. No equation or fitted parameter is renamed as a prediction, and no cited 'uniqueness theorem' is used to force a choice. Accordingly, the paper shows no material circularity and receives score 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper introduces no new physical or abstract entities beyond software components; its core claims rest on seL4's verified guarantees, the scalability argument for small modules, the static-architecture premise, and the fairness of the baseline configurations.

assumptions (5)

domain assumption seL4 microkernel correctly enforces spatial and temporal isolation, confidentiality, and integrity.
The entire LionsOS security and safety argument depends on seL4's formal verification. Invoked in Section 1 and throughout.
domain assumption Verification effort scales quadratically with specification size.
Used in Section 2.1 to justify the modular design. Based on Matichuk et al. 2015 empirical study, not independently re-derived.
ad hoc to paper A static system architecture can serve all realistic embedded use cases.
Stated in Section 3 as a design premise: 'We are yet to see a realistic use case in the embedded space that cannot be addressed with a static architecture.' No proof is offered.
domain assumption The SPIN model-checking results correctly prove deadlock-freedom of the signalling protocols.
Section 6.2.2 claims model checking eliminates protocol bugs. Requires trusting the models and the SPIN tool.
domain assumption The Linux, Genode, and CEOS configurations used as baselines are representative, fairly-tuned comparisons.
The performance conclusion depends on the baselines being comparable; the paper does not provide error bars or tuning details for Linux beyond standard distributions.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Fast, Secure, Adaptable: LionsOS Design, Implementation and Performance." pith.science (2026). https://pith.science/paper/BJTZ6LTI

@misc{pith2026250106234,
  author       = {Pith},
  title        = {Pith review of: Fast, Secure, Adaptable: LionsOS Design, Implementation and Performance},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BJTZ6LTI}},
  note         = {Machine review of arXiv:2501.06234}
}

read the original 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

Figures reproduced from arXiv: 2501.06234 by the authors.

**Figure 2.** shows the architecture. The driver VM runs the legacy driver as part of a (minimally configured) Linux guest. The guest runs a single, staticallylinked usermode program, the UIO driver (which replaces init). The program uses normal Linux system calls to interact with the device, and the Linux user I/O (UIO) framework to interact with the LionsOS driver queues. Specifically we use UIO to map guest physical memory… view at source ↗

**Figure 4.** Performance comparisons on i.MX8MQ UDP echo benchmark. Here and in other figures, the left axis and [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗

Figures from the paper (3 more)

**Figure 5.** Figure 5: LionsOS vs Linux performance on x86 64 UDP echo benchmark. Dashed lines are CPU use except in graph b (RTT). LionsOS, as the CEOS networking architecture is optimized for multicore and performed poorly in single-core experiments. CEOS provides a POSIX socket API, whic…

**Figure 6.** Figure 6: Component performance investigations. 0 10 20 30 40 50 60 70 80 90 4 16 64 256 10244096 0 5 10 15 20 Linux LionsOS Throughput (MiB/s) CPU Utilization (%) Request Size (KiB) (a) Sequential read. 4 16 64 256 10244096 0 5 10 15 20 Linux LionsOS CPU Utilization (%) Request…

**Figure 7.** Figure 7: I/O operation bandwidth on LionsOS and Linux. Solid lines are throughput, dashed lines are CPU utilisation. [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Verifying Device Drivers with Pancake
cs.PL 2025-01 conditional novelty 8.0 of 10

Pancake is a new language with a verified compiler and an automated Viper front-end; it is used to verify a performant Ethernet NIC driver, though the transpiler and reentry semantics remain unverified.

Reference graph

Works this paper leans on

3 extracted references · 3 canonical work pages · cited by 1 Pith paper

[2005]

InInternational Con- ference on Collaborative Computing

The Nizza Secure-System Architecture. InInternational Con- ference on Collaborative Computing. San Jose, CA, US. Jorrit N. Herder, Herbert Bos, Ben Gras, Philip Homburg, and An- drew S. Tanenbaum. 2006. MINIX 3: A Highly Reliable, Self- Repairing Operating System. ACM Operating Systems Review 40, 3 (July 2006), 80–89. Dan Hildebrand. 1992. An Architectura...

work page 1997
[2016]

In USENIX Symposium on Operating Systems Design and Im- plementation

Push-Button Verification of File Systems via Crash Refine- ment. In USENIX Symposium on Operating Systems Design and Im- plementation. Savannah, GA, US, 1–16. Bingyao Wang and Margo Seltzer. 2022. Tinkertoy: Build Your Own Operating Systems for IoT Devices. 41, 11 (2022), 4028–4039. Brent Welch. 1991. The File System Belongs in the Kernel. InUSENIX Mach W...

work page 2022
[2018]

In EuroSys Conference

Scheduling-Context Capabilities: A Principled, Light-Weight OS Mechanism for Managing Time. In EuroSys Conference. ACM, Porto, Portugal, 14. Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein, and Mark Staples. 2015. Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. In International Conference on S...

work page 1989

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [2005]

InInternational Con- ference on Collaborative Computing

The Nizza Secure-System Architecture. InInternational Con- ference on Collaborative Computing. San Jose, CA, US. Jorrit N. Herder, Herbert Bos, Ben Gras, Philip Homburg, and An- drew S. Tanenbaum. 2006. MINIX 3: A Highly Reliable, Self- Repairing Operating System. ACM Operating Systems Review 40, 3 (July 2006), 80–89. Dan Hildebrand. 1992. An Architectura...

work page 1997

[2] [2016]

In USENIX Symposium on Operating Systems Design and Im- plementation

Push-Button Verification of File Systems via Crash Refine- ment. In USENIX Symposium on Operating Systems Design and Im- plementation. Savannah, GA, US, 1–16. Bingyao Wang and Margo Seltzer. 2022. Tinkertoy: Build Your Own Operating Systems for IoT Devices. 41, 11 (2022), 4028–4039. Brent Welch. 1991. The File System Belongs in the Kernel. InUSENIX Mach W...

work page 2022

[3] [2018]

In EuroSys Conference

Scheduling-Context Capabilities: A Principled, Light-Weight OS Mechanism for Managing Time. In EuroSys Conference. ACM, Porto, Portugal, 14. Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein, and Mark Staples. 2015. Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. In International Conference on S...

work page 1989