Skip to content

MAP.md

Latest commit

 

History

History
140 lines (115 loc) · 8.31 KB

MAP.md

File metadata and controls

140 lines (115 loc) · 8.31 KB
Raw

Kernel Rust Coverage Map: Charon extraction

What of the Linux kernel's Rust extracts to LLBC through Charon (the Rust front-end of the Aeneas toolchain), measured across the whole tree against one shared stub layer. Phase 1 inventory: INVENTORY.md / inventory.csv. Per-unit Charon outcomes: results.csv.

Result

Self-contained parsing leaves extract cleanly. Whole driver and module crates do not: the barrier is the kernel-crate surface. Against a shared minimal stub, every hand-extracted parsing leaf translates, including the union-based binder deserializer, while every whole driver crate and the kernel crate itself fail on the first unstubbed kernel:: path. 27 of 28 whole-crate failures are "missing kernel API," the same shared cost across units. The earlier spike saw the same pattern.

Coverage (Charon extraction units)

Extraction is at crate granularity. The 80 rust/kernel modules are one crate (kernel_crate); their per-module analytics live in the inventory. Drivers, samples, and support crates are their own crates. Two hand-extracted leaves (binder_parse_leaf, nova_sbuffer_leaf) are included to show what is reachable.

Outcome n Units
CLEAN 8 binder_parse_leaf†, nova_sbuffer_leaf†, drm_panic_qr, sample_rust_minimal, rust_build_error, rust_ffi, rust_compiler_builtins, mm_kasan_test
FAIL 28 all 10 driver crates (nova_core, android_binder, drm_tyr, drm_nova, net_phy_*, cpufreq_dt, pwm_th1520, block_rnull), kernel_crate, 13 samples, pin_init, rust_uapi, rust_bindings, lib_find_bit_benchmark
N/A 4 rust_macros (proc-macro crate), sample_hostprogs, scripts_build_tools, tools_perf_workload (userspace/host)
TIMEBOX 0 every unit resolved inside the 15-min cap (all failures were fast compile errors)

† hand-extracted leaf against the shared stub. drm_panic_qr (1016 LOC) and mm_kasan_test are whole units that extract as-is.

Failure-cause breakdown

Category n Note
missing kernel API 27 first unstubbed kernel::<mod> (sync, io, device, net, block, …). Includes kernel_crate (needs CONFIG_* cfgs + generated bindings) and rust_uapi/rust_bindings (need OBJTREE bindgen output).
proc-macro 1 pin_init needs its pin_init_internal proc-macro subcrate.
unsupported language feature 0 none. Charon accepted every feature the leaves used (unions, MaybeUninit, raw-pointer casts, unsafe, closures, ?).
FFI boundary 0 not reached. Units fail at the Rust kernel:: surface before any C call.
macro expansion 0 driver-registration macros (module!, module_*_driver!, declare_drm_ioctls!) were absorbed by no-op stubs, so no unit failed on a macro.

The dominant edge is uniform: error[E0433]: cannot find \sync` in `kernel`` and siblings. No unit reached a Charon-level (post-compile) rejection. Every failure is an ordinary rustc name-resolution error against the shallow stub.

Verification-target shortlist: untrusted-input units by outcome and union status

The two planning columns together (from INVENTORY.md). Whole-unit outcome is the crate extraction; kernel::* modules resolve via kernel_crate. union flags the known Aeneas blocker (AeneasVerif/aeneas#1199).

Unit LOC whole-unit outcome union reachable leaf
nova_core 13,451 FAIL (missing kernel API) yes nova_sbuffer_leaf → CLEAN (byte cursor the GSP parsers use)
android_binder 9,489 FAIL (missing kernel API) yes binder_parse_leaf → CLEAN (the deserializer; unions survive → Aeneas-blocked)
kernel::drm 2,770 FAIL (via kernel_crate) yes -
drm_tyr 2,167 FAIL (missing kernel API) no -
kernel::debugfs 1,752 FAIL (via kernel_crate) no -
kernel::str 1,066 FAIL (via kernel_crate) no - (marginal parser)
kernel::configfs 1,044 FAIL (via kernel_crate) no -
kernel::uaccess 664 FAIL (via kernel_crate) no - (its SliceReader surface is in the shared stub)
kernel::miscdevice 439 FAIL (via kernel_crate) no -
kernel::iov 314 FAIL (via kernel_crate) yes -
sample_rust_misc_device 291 FAIL (missing kernel API) no -
drm_nova 226 FAIL (missing kernel API) no -
sample_rust_debugfs_scoped 144 FAIL (missing kernel API) no -

No untrusted-input unit extracts as a whole crate against a minimal shared stub; each needs the broad kernel surface. The parsing cores of the two largest targets, binder and nova-core, do extract once the environment is stubbed. Among the four union-touching untrusted units, binder's extractable leaf is the one that contains the union, which makes it the concrete instance of the Aeneas blocker on a real target; nova_core, kernel::drm, and kernel::iov carry unions elsewhere in the crate.

Top 5 observations

  1. 27 of 28 failures are "missing kernel API," all of the same shape: the first unstubbed kernel::<mod>. Coverage is gated by how much of the kernel crate the shared stub models. Each stubbed module unblocks several units at once.

  2. Zero units failed on a language feature, FFI, or a Charon-level rejection. Everything that compiled extracted. The leaves exercised unions, MaybeUninit/assume_init, raw-pointer casts, unreachable_unchecked, closures, and ?, all of which pass Charon.

  3. binder_parse_leaf and nova_sbuffer_leaf extract against the shared stub, and drm_panic_qr (1016 LOC) extracts as a whole unit. The reachable surface is the self-contained leaf, obtained by growing one shared stub.

  4. binder_parse_leaf passes Charon with its union intact, which is what Aeneas rejects (#1199). Even a complete kernel stub leaves binder's deserializer blocked at the Aeneas stage until union support lands, or a [u8; N] re-model per the spike. nova_core, kernel::drm, and kernel::iov also touch unions.

  5. All 13 non-trivial samples FAIL identically (missing kernel::sync/device/…) despite being tiny; they are thin wrappers over the same broad kernel surface. sample_rust_minimal is the only one that extracts, because it uses nothing but KVec and printk. Samples do not reduce the kernel-surface stub cost.

Note on zerocopy

zerocopy is excluded from the target set as a vendored third-party crate. Three facts about it bear on later phases: the kernel is migrating onto it, an Aeneas developer (Nadrieril) has recommended it, and its author (joshlf) is already bringing it into Aeneas.

Environment

  • Kernel: ~/linux v7.2-rc2 (7.2.0-rc2, "Baby Opossum Posse"), read-only, unmodified.
  • Charon: ~/charon commit 909ff09a, v0.1.220 (the version Aeneas pins), prebuilt ~/charon/bin/charon; invoked as charon cargo --preset=aeneas. Toolchain nightly-2026-06-01.
  • Shared stub layer (stubs/kernel): one kernel crate, #![no_std] + alloc, reusing the spike's stub design. Provides error (Error/Result/EINVAL/…), transmute (FromBytes/AsBytes markers), uaccess (UserSliceReader/SliceReader over &[u8], the 4-method reader surface), alloc (KVec/KBox/Flags/GFP_KERNEL), str (CStr/BStr), a hand-written uapi module (the five binder #[repr(C)] structs + unions + BINDER_TYPE_*), pci::Vendor, prelude, and no-op pr_*/dev_*/driver-registration macros. Bodies exist only to typecheck; every real API beyond this surface is deliberately absent, so a unit that needs more is a "missing kernel API" data point.
  • Harness (tools/run_unit.py, tools/run_all.py): assembles a scratch crate per unit against the shared stub, runs charon cargo --preset=aeneas under a 15-min cap, records outcome + verbatim first error + category. Shared preprocessing strips pure-codegen proc-macro attributes (#[export], #[vtable], #[pinned_drop]); no per-target source edits beyond the two leaves.

Reproduce: python3 tools/run_all.py && python3 tools/finalize.py. Leaves: cd scratch/<leaf> && charon cargo --preset=aeneas.