seL4 + LKL + UINTR: 复用 Linux 生态的微内核架构 Linux 实例 A (隔离域) nginx python redis libc / POSIX 用户态库 (原封不动) ELF 加载 → seL4 task 创建 (地址空间隔离) Linux 实例 B (隔离域) 数据库 服务B 服务C libc / POSIX 用户态库 (原封不动) ELF 加载 → seL4 task 创建 (独立地址空间) seL4 原生任务 设备驱动服务 文件系统服务 seL4 原生驱动 (cap 授权硬件访问) 与 LKL 实例共享驱动 (IPC 通信) UINTR 快速路径 syscall 指令 → 用户态直接陷入 LKL LKL 实例 1 (seL4 task) Linux Kernel Library — 改造后的 syscall 路由 VFS / 网络栈 ext4, tcp/ip, ... 驱动模块加载 virtio, usb, nvme... syscall → seL4 IPC cap-based 安全路由 host_os backend: pthread → seL4_tcb, mmap → seL4_vspace, signal → seL4_notification LKL 实例 2 (seL4 task) 独立地址空间，独立资源 — 崩溃不影响实例 1 VFS / 网络栈 独立实例 驱动模块加载 按需加载 syscall → seL4 IPC 独立 cap 空间 可按需启动多个实例，强隔离 / 崩溃恢复 / 负载均衡 seL4 微内核 形式化验证 · 最小 TCB · capability-based 访问控制 调度器 priority-based preemptive IPC / Notification 同步 cap-based IPC UINTR 处理 用户态中断路由 (新增) 内存管理 vspace / untyped caps 硬件 cap 映射 MMIO/IRQ → cap 授权 硬件层 CPU (UINTR 支持) MMIO 设备 中断控制器 网络 / 存储 DMA 引擎 核心机制 UINTR 快速 syscall 用户态 syscall → UINTR 通知 → LKL 直接处理 (无内核 trap) 延迟: ~百 cycle vs ~千 cycle 驱动复用 Linux 内核模块在 LKL 中加载 硬件访问通过 seL4 cap 授权 驱动崩溃 → 实例隔离，不影响其他 多实例管理 Linux = seL4 task (轻量) 按需启动 / 销毁 / 重启 崩溃恢复 = destroy + create 隔离保证 seL4 cap 天然隔离地址空间 不同实例 = 不同 vspace + cap 树 强隔离: 故障域完全独立 数据流 语义/机制 UINTR 快速路径 可选