Luna — LKL on seL4 架构

Linux Kernel Library 作为 seL4 隔离 Task 运行

seL4 User Space — Root Manager VSpace 隔离 Child VSpace · 独立 CSpace QEMU x86_64 硬件模拟平台 seL4 Microkernel Capability-based 访问控制 · IPC · 调度 Root Manager main.c · Bootstrap · TSC 校准 Isolation Manager isolation_manager.c · 装载/诊断/重建 Timer Service isolation_timer.c · 周期/单次定时 luna-lkl-task 隔离 Child · 独立 CSpace/VSpace LKL Host Ops lkl_task_host.c · 线程/同步/TLS 适配 LKL 内核 Linux 6.12+ · 单地址空间 Library OS BusyBox ash Shell · 管道 · 后台任务 · Applet Virtio Block lkl_task_disk.c · ext4 持久根 Virtio Net isolation_net.c · IPv4/ICMP/TCP 网络后端 slirp · passt · TAP 持久存储 memory-backend-file · 跨 QEMU 重启 root task 启动 装载 · 独立 CSpace/VSpace lkl_init + start_kernel 静态 ABI · spawn DMA 共享页 DMA 共享页 ext4 fault EP · 诊断 · 重建 Notification → trigger_irq Legend Cloud Security Backend Frontend Database Message bus

关键设计

  • • LKL 作为纯用户态 Task，不需硬件 syscall 陷入
  • • 单地址空间 Library OS + seL4 TCB 实现线程
  • • Manager 不链接 LKL，仅管理 child 生命周期
  • • 每个 LKL host 线程 = 一个 seL4 TCB

已验证能力

  • • BusyBox ash 交互式 shell
  • • ext4 持久化 + 跨 QEMU 重启
  • • virtio-net ICMP/TCP 网络
  • • 100 次 child boot/halt/destroy 压力测试
  • • 管道、后台任务、多 worker

Architecture diagram • Built with Archify • Press T for theme and E for export