rel4-linux-kit — 在 seL4 微内核上运行 Linux ELF 二进制文件 | 分析日期:2026-07-19
在 seL4 微内核 上实现 Linux 兼容层(LCL),使 Linux ELF 二进制文件(如 busybox)可以直接运行。
运行 busybox iozone 对 ext4 文件系统进行基准测试 — 即通过 LCL 的文件 syscall 路径实现真实的文件 I/O(open/read/write/lseek/stat)。
fs/ipc_client.rs → seL4 Endpointext4-srv/src/service.rs → lwext4-taskx86_64-sel4.json总计定义 55+ 个 Linux syscall 号,实际实现情况如下:
| 类别 | Syscall | 状态 | 说明 |
|---|---|---|---|
| 文件 I/O | read (0) | ✅ 完成 | stdin/stdout/stderr + 设备文件 + IPC ext4 |
| write (1) | ✅ 完成 | stdout/stderr → 串口,其他 → IPC ext4 | |
| openat (257) | ✅ 完成 | 设备文件 + IPC ext4 路径 | |
| close (3) | ✅ 完成 | fd 0-2/设备 + IPC ext4 | |
| lseek (8) | ✅ 完成 | 通过 IPC ext4 实现 | |
| 文件属性 | fstat (5) | ⚠️ 部分 | 设备文件返回 0,ext4 仅获取 size |
| fstatat (262) | ✅ 完成 | 构建完整 struct stat(144 字节) | |
| getdents64 (217) | ✅ 完成 | 通过 IPC ext4 实现目录遍历 | |
| mkdirat (258) | ✅ 完成 | 通过 IPC ext4 | |
| unlinkat (263) | ✅ 完成 | 通过 IPC ext4 | |
| faccessat (269) | ✅ 完成 | 通过 IPC ext4 | |
| 内存管理 | brk (12) | ✅ 完成 | 按页映射堆增长(已修复) |
| mmap (9) | ✅ 完成 | 查找空闲区域 + 按页映射 | |
| munmap (11) | ✅ 完成 | 解除页映射 | |
| mprotect (10) | 🔶 Stub | 返回 0,未实际执行 | |
| 进程/线程 | exit (60) | ✅ 完成 | 设置退出码 |
| exit_group (231) | ✅ 完成 | 设置退出码 | |
| getpid (39) | ✅ 完成 | 返回 task.pid | |
| set_tid_address (218) | ✅ 完成 | 设置 clear_child_tid | |
| clone (56) | ❌ ENOSYS | 返回 38,未实现 | |
| wait4 (61) | ❌ ECHILD | 返回 10 | |
| 信号 | rt_sigaction (13) | ✅ 完成 | 信号处理器注册 |
| sigprocmask (14) | ✅ 完成 | SIG_BLOCK/UNBLOCK/SETMASK | |
| kill (62) | ✅ 完成 | 信号发送 | |
| Stub / 未实现 | pipe2 (22) | ❌ ENOSYS | 管道未实现 |
| dup/dup3 (32/33) | ❌ ENOSYS | fd 复制未实现 | |
| renameat (264) | 🔶 Stub | 返回 0,未实际操作 | |
| mount/umount2 | ❌ EPERM | 返回 EPERM | |
| ftruncate (77) | 🔶 Stub | 返回 0,未实际操作 |
| 模块 | 进度 | 条形图 |
|---|---|---|
| seL4 内核引导 | 100% | |
| ELF 加载器 | 100% | |
| Syscall 分发 | 95% | |
| 内存管理 (brk/mmap) | 90% | |
| 文件 I/O (IPC ext4) | 75% | |
| 进程管理 (fork/clone) | 20% | |
| 管道/重定向 | 10% | |
| 信号完整支持 | 60% | |
| iozone 端到端 | 30% |
initfeat: porting to x86_64ls 系统 | 最后一次提交sys_clone 返回 ENOSYS,这意味着:
sh -c "command" 以外的交互式 shellcmd1 | cmd2 和 I/O 重定向依赖 pipe2 和 dup/dup3。当前均返回 ENOSYS。
ls -l 等命令需要完整的 stat 信息。
openat, read, write, close, lseek, getdents64, mkdirat, unlinkat 等核心文件操作已通过 IPC 实现。
sh -c "..."/ # 提示符)ls 命令(通过 getdents64 + fstatat)| Crate | 角色 | 编译目标 |
|---|---|---|
root-task | 主入口,系统初始化,测试,busybox 运行 | x86_64-sel4 (no_std) |
lcl | Linux 兼容层 — syscall 模拟核心 | x86_64-sel4 (no_std) |
ext4-srv | ext4 文件系统 IPC 服务 | x86_64-sel4 (no_std) |
blk-task | 块设备(ramdisk) | x86_64-linux-musl |
lwext4-task | ext4 操作(lwext4_rust) | x86_64-linux-musl |
sel4-sys | 底层 seL4 syscall 包装(纯 asm) | x86_64-sel4 |
sel4-ulib | seL4 用户空间工具库 | x86_64-sel4 |
common | 共享常量、分配器、slot 管理 | x86_64-sel4 |
srv-gate | 服务门抽象(block, fs, uart) | x86_64-sel4 |
libc-core | 最小 libc(errno, fcntl, types) | x86_64-sel4 |
| 优先级 | 任务 | 复杂度 | 影响 |
|---|---|---|---|
| 🔴 P0 | 实现 fork/clone(至少 CLONE_VM 模式) | 高 | 解锁交互式 shell 和子进程 |
| 🔴 P0 | 实现 pipe2 + dup/dup3 | 中 | 解锁 shell 管道和 I/O 重定向 |
| 🟡 P1 | 完善 fstat(写入完整 struct stat) | 低 | 修复 ls -l 等命令 |
| 🟡 P1 | 实现 renameat | 低 | 文件重命名操作 |
| 🟡 P1 | 实现 ftruncate | 低 | 文件截断操作 |
| 🟢 P2 | 完善 writev(实际写入数据) | 低 | 某些程序的输出 |
| 🟢 P2 | 实现 pread64/pwrite64 | 低 | 随机读写支持 |
| 🟢 P2 | 实现 sendfile | 低 | 高效文件传输 |
mk-call-merge 是一个雄心勃勃的项目,目标是在 seL4 微内核上实现 Linux syscall 兼容层。项目在 6 天内从零发展到能运行 busybox shell,进展迅速。
核心成就:
主要差距:
距离 iozone 目标:需要先实现 fork、pipe、完善的文件操作,然后才能运行 iozone 基准测试。预估还需要 2-4 周 的密集开发。