diff --git a/crates/thumos/src/kinit.rs b/crates/thumos/src/kinit.rs index b969e25b..4aa34cb1 100644 --- a/crates/thumos/src/kinit.rs +++ b/crates/thumos/src/kinit.rs @@ -1204,135 +1204,6 @@ pub unsafe fn run() -> ! { } } } - crate::kinit_plan::MountPlan::Plain => { - use crate::lfs; - use crate::lfs_imap::LfsError; - - // Compute device size in sectors from the partition constants. - let sector_count = board::LFS_PARTITION_SIZE; - - // #603: the eMMC block device addresses the PHYSICAL medium (its LBA - // 0 is the eMMC's sector 0 -- the GPT/boot region), so its bound is - // the partition's END; the LFS mount then runs inside the userdata - // partition VIEW carved at LFS_PARTITION_START. Before the view, LFS - // would have formatted over the boot/vendor partitions. - // - // WHY the plain mount is still at the partition head: this arm is - // reachable only on an UNPROVISIONED device (no preamble), so no - // plaintext sector has been carved — byte-compatible with pre-#446 - // images. - let uninit = MsdcBlockDeviceUninit::new(board::LFS_PARTITION_START + sector_count); - - // SAFETY: eMMC controller was initialized successfully in Step 7. - // init() is called once here on a freshly constructed device. - match unsafe { uninit.init() } { - Ok(phys_dev) => { - let blk_dev = crate::block::PartitionBlockDevice::new( - phys_dev, - board::LFS_PARTITION_START, - sector_count, - ); - // Try to mount existing LFS. - match lfs::mount(alloc::boxed::Box::new(blk_dev)) { - Ok(fs) => { - serial.log(" LFS mounted OK\r\n"); - lfs_root = Some(alloc::boxed::Box::new(fs)); - } - // CURRENT UNSAFE COMPATIBILITY (#360): this result does - // not prove first boot. It also covers damaged or - // version-incompatible existing metadata, but this - // branch still formats. Production must distinguish an - // authenticated first-provisioning state or require an - // explicit operator-confirmed format action. - // - // WHY this arm is still ungated while the encrypted one - // above is not: the encrypted mount is reached only - // after a passphrase verifies, so `provisioned_this_boot` - // separates a device provisioned moments ago from one - // provisioned earlier. This arm is reached only when the - // preamble is `Unprovisioned` — a device that has never - // held a passphrase — so no such marker exists to - // consult, and nothing on the medium distinguishes a - // never-formatted plain LFS from a damaged one. Closing - // it needs a durable formatted-before marker, which is - // the remaining half of #360. - Err(LfsError::InvalidSuperblock) => { - serial.log( - " CRIT Ambiguous LFS superblock; legacy auto-format path (#360)\r\n", - ); - let fmt_uninit = MsdcBlockDeviceUninit::new( - board::LFS_PARTITION_START + sector_count, - ); - // SAFETY: eMMC controller was initialized successfully in - // Step 7; init() is called once here on a freshly - // constructed device. - if let Ok(fmt_phys) = unsafe { fmt_uninit.init() } { - let mut fmt_dev = crate::block::PartitionBlockDevice::new( - fmt_phys, - board::LFS_PARTITION_START, - sector_count, - ); - if lfs::format(&mut fmt_dev).is_ok() { - serial.log(" LFS formatted OK\r\n"); - // Remount the freshly formatted device so the - // VFS root is backed by durable storage from - // this boot onward, not just after the NEXT - // reboot (#343). - let remount_uninit = MsdcBlockDeviceUninit::new( - board::LFS_PARTITION_START + sector_count, - ); - // SAFETY: eMMC controller was initialized successfully - // in Step 7; init() is called once here on a freshly - // constructed device. - match unsafe { remount_uninit.init() } { - Ok(remount_phys) => { - let remount_dev = - crate::block::PartitionBlockDevice::new( - remount_phys, - board::LFS_PARTITION_START, - sector_count, - ); - match lfs::mount(alloc::boxed::Box::new(remount_dev)) { - Ok(fs) => { - serial.log(" LFS remounted OK\r\n"); - lfs_root = Some(alloc::boxed::Box::new(fs)); - } - Err(e) => { - boot_log!( - serial, - " WARN LFS remount after format failed: {:?}\r\n", - e - ); - } - } - } - Err(e) => { - boot_log!( - serial, - " WARN Block device re-init for remount failed: {:?}\r\n", - e - ); - } - } - } else { - serial.log(" WARN LFS format failed\r\n"); - } - } - } - Err(e) => { - boot_log!( - serial, - " CRIT LFS mount failed ({:?}) -- not reformatting, data at risk\r\n", - e - ); - } - } - } - Err(e) => { - boot_log!(serial, " WARN Block device init failed: {:?}\r\n", e); - } - } - } crate::kinit_plan::MountPlan::RamfsFallback => { if state.emmc_ok && state.secure_boot_ok { serial.log(" Skipped (payload locked or unreadable -- fail-closed)\r\n"); diff --git a/crates/thumos/src/kinit_plan.rs b/crates/thumos/src/kinit_plan.rs index 185752f6..5975f868 100644 --- a/crates/thumos/src/kinit_plan.rs +++ b/crates/thumos/src/kinit_plan.rs @@ -183,10 +183,6 @@ pub(crate) enum MountPlan { /// Wrap the payload view in `EncryptedBlockDevice` with the derived /// data key; LFS mounts one sector past the preamble. Encrypted, - /// Unprovisioned device: the plain LFS mount at the partition head. - /// This legacy dev/transition path is not protected-storage acceptance and - /// must be removed or made impossible in production under #866. - Plain, /// No persistent mount; the VFS root falls back to the initramfs. RamfsFallback, } @@ -194,11 +190,22 @@ pub(crate) enum MountPlan { /// Decide the userdata mount. Fail-closed invariants: /// - no eMMC or no verified boot: nothing persistent mounts (the #217 gate /// today's code already enforces); -/// - a provisioned (locked) payload is NEVER plain-mounted or formatted — -/// without the derived key the only honest mount is none; +/// - a provisioned (locked) payload is NEVER mounted or formatted without its +/// key — without the derived key the only honest mount is none; /// - an unreadable OR corrupt preamble is treated as provisioned (unknown -/// = locked, #621) — never as unprovisioned, which would plain-mount -/// and then format on the resulting `InvalidSuperblock`. +/// = locked, #621) — never as unprovisioned; +/// - **an unprovisioned device with no verified passphrase mounts nothing** +/// (#866). There is no plaintext arm to select. The persistent root is the +/// AES-XTS payload or it is the initramfs. +/// +/// WHY the plaintext arm was removed outright rather than gated behind a +/// non-production feature, which is what #866 offered as the minimum: it was +/// reachable ONLY in production. `secure_boot_ok` is set at exactly one place +/// in `kinit`, and only when `BOOT_KEY_IS_PRODUCTION` — a dev-anchor build +/// boots degraded with it false, so it could never reach past the gate above. +/// A compatibility path that exists in no configuration but the one it is +/// forbidden in has nothing left to be compatible with, and gating it would +/// have produced a branch that no build can execute and no test can reach. pub(crate) const fn mount_plan( emmc_ok: bool, secure_boot_ok: bool, @@ -208,16 +215,26 @@ pub(crate) const fn mount_plan( if !emmc_ok || !secure_boot_ok { return MountPlan::RamfsFallback; } - if passphrase_ok { + // WHY the preamble is re-checked here rather than trusted through + // `passphrase_ok`: today only `Provisioned` and `Unprovisioned` can produce + // a key at all -- `boot_passphrase_plan` answers `Skip` for the other three + // -- so this condition is currently implied. It is stated anyway because + // the implication lives in a DIFFERENT function, and the cost of it ever + // ceasing to hold is mounting the payload of a device whose preamble could + // not be read. Unknown stays locked (#621) whatever else changes. + if passphrase_ok + && matches!( + preamble, + PreambleLoad::Provisioned | PreambleLoad::Unprovisioned + ) + { return MountPlan::Encrypted; } - match preamble { - PreambleLoad::Unprovisioned => MountPlan::Plain, - PreambleLoad::Provisioned - | PreambleLoad::ReadFailed - | PreambleLoad::NotRead - | PreambleLoad::Corrupt => MountPlan::RamfsFallback, - } + // Every remaining state mounts nothing. `Unprovisioned` reaches here only + // when first-boot setup did not produce a verified passphrase -- skipped, + // interrupted, or unable to reach the operator -- and a device that has + // never held a secret has no userdata to lose by declining to mount. + MountPlan::RamfsFallback } /// Whether an ambiguous LFS superblock on the ENCRYPTED payload may be @@ -1032,14 +1049,27 @@ mod tests { mount_plan(true, true, PreambleLoad::NotRead, false), MountPlan::RamfsFallback ); - // #621: a corrupted-but-present preamble reaches neither the - // plain-mount arm nor a reformat -- it is locked on the same - // footing as an unreadable one, never treated as unprovisioned. + // #621: a corrupted-but-present preamble is locked on the same footing + // as an unreadable one, never treated as unprovisioned. assert_eq!( mount_plan(true, true, PreambleLoad::Corrupt, false), MountPlan::RamfsFallback, - "corrupt preamble is locked, never plain-mounted or formatted (#621)" + "corrupt preamble is locked, never mounted or formatted (#621)" ); + // An unreadable preamble stays locked even if a key somehow exists -- + // the check does not depend on boot_passphrase_plan continuing to + // refuse one (#621). + for locked in [ + PreambleLoad::Corrupt, + PreambleLoad::ReadFailed, + PreambleLoad::NotRead, + ] { + assert_eq!( + mount_plan(true, true, locked, true), + MountPlan::RamfsFallback, + "{locked:?} must not mount even with passphrase_ok" + ); + } // The two real mounts. assert_eq!( mount_plan(true, true, PreambleLoad::Provisioned, true), @@ -1051,13 +1081,54 @@ mod tests { MountPlan::Encrypted, "first-boot setup also ends in the encrypted mount" ); + // #866: the one state that used to select a plaintext root. Setup was + // skipped, interrupted, or could not reach the operator -- so there is + // no key, and the only honest answer is no persistent mount. assert_eq!( mount_plan(true, true, PreambleLoad::Unprovisioned, false), - MountPlan::Plain, - "unprovisioned dev path stays byte-compatible" + MountPlan::RamfsFallback, + "unprovisioned with no verified passphrase mounts nothing (#866)" ); } + #[test] + fn no_input_state_selects_a_persistent_mount_without_a_key() { + // The property #866 asks for, stated over the WHOLE input space rather + // than the states someone remembered to enumerate: every combination of + // the four inputs either produces the AES-XTS mount or produces no + // persistent mount at all. `MountPlan` no longer has a third answer, + // and this fails to compile rather than fails to assert if one returns. + for emmc_ok in [false, true] { + for secure_boot_ok in [false, true] { + for preamble in [ + PreambleLoad::NotRead, + PreambleLoad::ReadFailed, + PreambleLoad::Corrupt, + PreambleLoad::Unprovisioned, + PreambleLoad::Provisioned, + ] { + for passphrase_ok in [false, true] { + let plan = mount_plan(emmc_ok, secure_boot_ok, preamble, passphrase_ok); + if plan == MountPlan::Encrypted { + assert!( + passphrase_ok + && emmc_ok + && secure_boot_ok + && matches!( + preamble, + PreambleLoad::Provisioned | PreambleLoad::Unprovisioned + ), + "encrypted mount requires a derived key on a verified boot \ + over a readable preamble: emmc={emmc_ok} \ + secure={secure_boot_ok} pre={preamble:?} pass={passphrase_ok}" + ); + } + } + } + } + } + } + #[test] fn boot_state_defaults_preamble_to_not_read() { let state = BootState::new(); diff --git a/docs/capability-inventory.toml b/docs/capability-inventory.toml index c46642a4..4580c1c6 100644 --- a/docs/capability-inventory.toml +++ b/docs/capability-inventory.toml @@ -21,7 +21,7 @@ notes = "Selected PL0 image, fault, graceful-kill, fork/exec/brk, and guard-page id = "memory-fs" modules = ["block", "cache", "vfs", "devfs", "lfs", "lfs_imap", "lfs_segment", "lfs_checkpoint", "lfs_writer", "lfs_compact", "emmc", "ramfs", "encryption"] tier = "kernel-wired" -notes = "LFS mounts at boot, encrypted when provisioned but still plaintext under the live Unprovisioned compatibility path (#866); no witness marker asserts persistence behavior. #360 owns the current ambiguous InvalidSuperblock auto-format/data-loss path, #867 owns the 48 KiB direct-block file ceiling, #870 owns unverified MSDC RX-count semantics, #837 owns the XTS logical-block/tweak description, and #878 owns authenticated/versioned integrity and rollback rejection beyond XTS confidentiality." +notes = "LFS mounts at boot only through the AES-XTS wrapper; the plaintext Unprovisioned compatibility mount is gone (#866), so an unprovisioned device with no verified passphrase falls back to the initramfs rather than creating a plaintext root. No witness marker asserts persistence behavior. #360 owns the current ambiguous InvalidSuperblock auto-format/data-loss path, #867 owns the 48 KiB direct-block file ceiling, #870 owns unverified MSDC RX-count semantics, #837 owns the XTS logical-block/tweak description, and #878 owns authenticated/versioned integrity and rollback rejection beyond XTS confidentiality." [[capability]] id = "time" diff --git a/docs/target-test-ledger.toml b/docs/target-test-ledger.toml index a36edbaf..3ed6623a 100644 --- a/docs/target-test-ledger.toml +++ b/docs/target-test-ledger.toml @@ -333,7 +333,7 @@ witness = "boot.sh" [[module]] name = "kinit_plan" -tests = 29 +tests = 30 mechanism = "host" fidelity = "The boot decisions here are pure functions over observed state, so host tests prove them exactly — including #360's encrypted-format gate, whose load-bearing case is a device provisioned in an EARLIER boot being refused. What host tests cannot reach is whether kinit.rs feeds these functions the right state on real hardware: `provisioned_this_boot` is set inside the non-QEMU first-boot-setup arm, which no host or QEMU profile executes. boot.sh witnesses kinit, not that arm."