Lean verification: prove 164 more functions and fix the kernel bugs the proofs found - #591
Merged
Merged
Conversation
A strict audit found six functions counted as substantive because they appeared in an open ... renaming line or a local simp attribute list, with no theorem statement about them. Each now has one: - ct_select_usize returns its first operand on true and its second on false, on a 32-bit or 64-bit usize; ct_select_u32 and ct_select_u64 the same for every pair of operands. - ct_clz_u64 returns 64 for zero and otherwise the shift n with 2^63 <= x * 2^n < 2^64, given the Rust meaning of wrapping_neg, which the extraction leaves opaque; ct_is_zero_u64 is one exactly at zero under the same hypothesis. - the IOMMU index_for is the nine-bit slice above the level shift for levels one to six and fails at level zero; fits_address_width is exact for every width. - is_block is present-and-huge on x86_64 and valid-and-not-table on aarch64. Each theorem was checked against a mutant of the generated code.
The classifier counted a function as substantive when its name appeared anywhere outside the wrapper theorems, and comments were the only thing it stripped. An open ... renaming line, a local simp attribute list or a #print axioms line was enough, and six functions counted that way with no theorem about them. It now reads only the statements of non-wrapper theorems, following the names a file gives a function through open ... renaming and abbrev. The previous commit proved those six, so the count stays at the floor.
probe_at maps 4 KiB of a remapping unit, but the IOTLB register sits at IRO * 16 + 8 and the fault records at FRO * 16, with IRO and FRO read from ECAP and CAP and reaching past 16 KiB. invalidate_iotlb_global and take_fault wrote and read at those offsets, and RemapUnit's accessors checked the window only with debug_assert!, so in a release build a unit reporting IRO or FRO of 256 or more got volatile MMIO reads and writes outside the mapping. probe_at now refuses such a unit with ProbeError::RegistersOutsideWindow, using registers_fit, and the accessors assert the window in every build. A unit with a register set larger than a page is refused rather than mapped in full. registers_fit is extracted. Its refinement reads the IRO, FRO and NFR fields exactly, states registers_fit holds exactly when both register sets end inside the window, and proves that for an accepted unit the IOTLB register and every fault record end inside the page.
Runs registers_fit over every IRO and a spread of FRO and NFR values against the byte bounds. The test does not build against the old probe, which had no window check.
check_bti_landing_pad accepted 0xD503201F, the NOP that BtiGuard::None emits, and on a core with FEAT_BTI an indirect branch to a NOP in a guarded page raises a Branch Target exception. It also rejected PACIASP and PACIBSP, which the architecture treats as BTI c. The decision is now is_bti_landing_pad in pad.rs, which accepts BTI c, BTI j, BTI jc, PACIASP and PACIBSP, and the check reads the word and asks it. A bare BTI, which accepts no branch type, stays rejected. is_bti_landing_pad is extracted. Its refinement gives the accepted set exactly and proves every BtiGuard but None emits a landing pad. The BtiGuard refinement drops its theorem about the old accepted list.
Calls the kernel landing-pad check on BTI c, j, jc, PACIASP, PACIBSP, the NOP and a bare BTI. The test fails against the check that accepted the NOP.
get_all_stack_regions packed each CPU's kernel stack and IST stacks back to back, while get_guard_regions takes a guard page below and above each one. So the kernel stack's upper guard was the first page of IST stack 0, and each IST stack's upper guard the first page of the next: verify_stack_integrity would report a live neighbouring stack as a compromised guard, or, with the guards unmapped, a stack would lose its top page. The stacks now start at stack_slot_offset, which leaves a guard page below the first stack, between every two and above the last. stack_slot_offset is extracted. Its refinement gives the offsets exactly, proves any two slots are separated by a full guard page, and that the area with its guards fits the per-CPU stride.
Checks every stack slot's guard pages against every other slot and the area against the per-CPU stride. The test does not build against the old layout, which had no stack_slot_offset.
Pid directories were numbered pid * 1000 + 100 and their entries (pid << 20) | k. Pid 0's directory got 100, the root sys entry's inode, and pid 0's status entry got 1, which procfs_lookup dispatches as the /proc root. Pid 131072's directory got 131072100, the inode of pid 125's task entry. A pid directory is now pid << 20, its entries keep k from 1 to 103, and only pids from 1 get a directory, so every pid inode lies above the root entries (at most 105) and no two collide. The refinement is restated: pid_dir_inode is none exactly for a pid of zero or below, pid * 2^20 otherwise, at least 2^20, and never an entry inode (q << 20) | k of any pid.
Checks that pids below one have no directory inode and that the inodes of pids 1 to 4095 sit above the root entries with clear entry bits. Both tests fail against the pid * 1000 + 100 numbering.
pci_config_address shifted the device and function into place without masking them, so device 32 on bus 0 produced the address of device 0 on bus 1 and a configuration read or write went to another device. PciAddress::new does not check its fields, so only from_bdf callers were in range. Device is now masked to five bits and function to three. The extractions are regenerated. The refinement, verified here, states the word for every input, reads each field back, and proves an out-of-range device stays on its bus.
Runs pci_config_address over every device and function number and checks the fields read back. The test fails against the unmasked encoder.
AcpiRsdp::verify_extended_checksum passed a revision 2 RSDP that carried none of the ACPI 2.0 fields as the ACPI 1.0 check alone, never summed the three reserved bytes at offsets 33 to 35, and never checked length. The ACPI parser's RsdpExtended::validate_extended_checksum does all three, so the two checkers disagreed. The multiboot parser now keeps the reserved bytes, and from revision 2 the check requires every extended field, a length of at least 36, and the 36 bytes summing to zero. The refinement states the check exactly for every shape of the fields, and that a revision 2 RSDP missing a field or shorter than 36 bytes fails. No kernel code calls the check yet.
Builds a revision 2 RSDP with a correct extended checksum, then tampers with a reserved byte, drops the extended fields and shortens the length; only the intact one passes. The test does not build against the old structure, which had no reserved bytes.
Four methods added or multiplied values that firmware or a wrapping counter controls with an overflow-checked operator, which with overflow-checks on in every profile halts the kernel: MemoryDescriptor::size_bytes and end_address on a descriptor reaching the top of the address space or claiming 2^52 pages, PercpuRegion::end and contains on a region flush against the top, IoApicInfo::gsi_max on a MADT base above 0xFFFFFFE8, and MmioStatsSnapshot::total_operations past u64::MAX. Each now saturates; PercpuRegion::contains measures the offset from the base, so the last page holds its own bytes. size_bytes uses an explicit bound rather than saturating_mul, which the extraction leaves opaque. The extractions are regenerated. The committed memory descriptor refinement and the pending per-CPU, I/O APIC and snapshot refinements, verified here, state the saturated values and that none of the calls can fail.
Runs the memory descriptor, per-CPU region, I/O APIC and MMIO snapshot methods at the top of their ranges. All three tests fail against the overflow-checked arithmetic.
ParsedSection::is_symtab accepted SHT_DYNSYM as well as SHT_SYMTAB, so ElfLoader::get_symbol_table, which returns the first section it accepts, returned .dynsym on an image that places it before .symtab. get_dynsym already exists for that section, and the bootloader's copy accepts SHT_SYMTAB alone. get_symbol_table has no caller today. The refinement states is_symtab holds exactly for type 2 and refuses a dynamic symbol table.
Includes the loader's section type and checks section types 0 to 63. The test fails against the check that accepted SHT_DYNSYM.
Bit 7 of a text attribute is blink with the attribute controller's default setting, which nothing in the tree changes. ColorCode::new, ColorCode::with_blink and the boot make_attr shifted the whole background into bits 4 to 7, so a bright background set bit 7 and drew blinking text on the dark one, and the boot bg_color read bit 7 as a background bit where ColorCode::background treats it as blink. The background is now masked to three bits everywhere, so a bright background is drawn dark and only with_blink sets bit 7. ColorCode::new is added to the vga_constants extraction. Its refinement proves the packed byte for all 256 colour pairs and that the cell never blinks; the vga_colors refinement, verified here, states the three-bit background for make_attr and bg_color.
Runs make_attr over every background and checks bit 7 stays clear and bg_color reads back three bits. The test fails against the helpers that used the whole nibble.
The UEFI_REVISION constants put the minor version in the upper byte of the low half, so 2.8 was 0x00020800 and read back as minor 2048, while 2.3.1 alone used the specification's tens-and-units form and sorted below 2.1. detect_firmware_info stored a third encoding, 0x00020008, beside the version string "2.8". A comparison of a firmware's real revision with these constants would have ordered versions wrongly. The constants are now built by uefi_revision, (major << 16) | minor * 10 + patch, and detect_firmware_info stores UEFI_REVISION_2_8. uefi_revision is extracted beside the firmware record. The refinement proves it never fails, gives the specification's packing whenever the tens-and-units field fits sixteen bits, reads back through the record as the major and minor field it packed, and yields 0x0002001F, 0x00020050 and 0x00020064 for 2.3.1, 2.8 and 2.10.
Checks every UEFI_REVISION constant against the specification's value, that they sort in version order, and that the firmware record reads UEFI_REVISION_2_8 back as major 2, minor 80. All three fail against the old constants.
requires_authentication tested the time-based and enhanced authenticated-write flags but not AUTHENTICATED_WRITE_ACCESS (0x10). UEFI 2.3.1 deprecates that flag, but firmware still reports it on variables written before, and a write to such a variable must still carry an authentication descriptor. A set carrying only 0x10 was answered as needing no authentication, while the same set with 0x20 added was answered as needing it. The extraction is regenerated. The refinement, verified here, restates the predicate as bit 4, 5 or 7 of the word for every word, and records that 0x10 alone now needs authentication.
Checks that AUTHENTICATED_WRITE_ACCESS, TIME_BASED_AUTHENTICATED_WRITE_ACCESS and ENHANCED_AUTHENTICATED_ACCESS each make a set need authentication, alone and on top of DEFAULT_NV_BS_RT, and that the other defined flags do not. Fails against the old requires_authentication, which ignored 0x10. The revision test is reformatted with the crate's rustfmt.
hidden_only set include_hidden, which every fresh configuration already has, and the scanner read that field only to drop hidden files when it was false. ScanConfig::new().hidden_only() was ScanConfig::new(), so a scan meant to list hidden files returned every visible file as well. The configuration gains only_hidden, hidden_only sets it, and the scanner asks admits_hidden, which requires include_hidden for a hidden file and a clear only_hidden for a visible one. admits_hidden is extracted beside the builders. The refinement proves it reads the two flags for every configuration, that after hidden_only any configuration admits exactly the hidden files, and that the fresh configuration admits every file but no visible one after hidden_only.
Checks that a fresh scan configuration admits hidden and visible files, that hidden_only admits hidden files and drops visible ones, and that turning include_hidden off drops hidden files and keeps visible ones. The old code had no admits_hidden, so the test does not build against it; its inline filter, !(!include_hidden && hidden), admitted a visible file under ScanConfig::new().hidden_only(), which the second check rejects.
EfiTime::is_valid bounded the day by 31 in every month, so 2021-02-31 passed and to_unix_timestamp read it as 2021-03-03. It now bounds the day by days_in_month, with a 29 day February in Gregorian leap years. to_unix_timestamp counted years forward from 1970 only. is_valid accepts years from 1900, and for those the loop was empty, so 1969-12-31 converted to the same second as 1970-12-31. A second loop now counts years from the date up to 1970 back from the epoch, so 1969-12-31 is -86400 and 1900-01-01 is -2208988800. The extraction is regenerated. The refinement, verified here and committed for the first time, characterises is_valid exactly on the UEFI ranges with the calendar day bound, runs all three loops of to_unix_timestamp to completion for every month from one to twelve, proves no step overflows, and pins the epoch, 2000-03-01, 1969-12-31, 1900-01-01 and the February 29 cases.
Checks that is_valid refuses days past the end of the month, including February 29 outside leap years and in 2100, and accepts the last day of each case; and that to_unix_timestamp gives 0 at the epoch, -86400 for 1969-12-31, -2208988800 for 1900-01-01 and the known values for 1970-12-31 and 2000-03-01. Both tests fail against the old code.
On a 64 bit target is_user_space accepts exactly the ranges whose unbounded end is at most 2^47 - 1, never fails, refuses 2^47 for every length, and refuses the page sized range naming the topmost user page while accepting that range less its last byte. The prose says why the top page stays refused: a SYSCALL in its last bytes would SYSRET to a non-canonical address, the hazard Linux avoids the same way.
iva_offset is the ten-bit IRO field of ECAP in sixteen byte units and iotlb_offset is eight bytes past it; neither fails for any ECAP. The IOTLB register fits the one mapped page exactly when IRO is at most 255, and IRO 256 lands at byte 4104. The prose records that the bound is enforced by registers_fit in probe_at, which used to be missing.
fault_recording_offset is the ten-bit FRO field of CAP in sixteen byte units and fault_recording_count is the NFR field plus one, between 1 and 256; neither fails for any word. The first record leaves the mapped page exactly when FRO reaches 256. The prose records that registers_fit in probe_at now refuses such a unit, where only a debug_assert stood.
TypesStack recorded that the first IST stack began at the kernel stack's top, so the page get_guard_regions took as the kernel stack's upper guard was the IST stack's first page. The layout now places stacks through stack_slot_offset. The recording theorem is renamed to what it still proves, that the top is the base plus 64 KiB, and a new theorem joins it with stack_slot_offset: the kernel stack at slot 0 tops out exactly one page below the IST stack at slot 1.
get_ticks returns the relaxed load unchanged, increment_ticks succeeds exactly when fetch_add of one succeeds whatever the old value, so the counter wraps rather than panicking in the timer interrupt, and reset_ticks stores the value the static starts with. The prose records that reset_ticks cannot be squared with the monotone clock of Nonos.Timer and that nothing calls it.
PhysAddr and VirtAddr align_down and align_up cleared low bits with !(align - 1), which rounds only when align is a power of two. Aligning ten down to three gave eight, which is_aligned then refused, and an alignment of zero underflowed and halted, where is_aligned answers false. Every caller passes a page size today. Both now round with the remainder: align_down subtracts it, align_up adds what is missing to the next multiple, and an alignment of zero leaves the address unchanged. align_up overflows only when the rounded address is past u64::MAX. is_aligned uses is_multiple_of, the same test, as clippy asks. The extractions are regenerated. The refinements, verified here and committed for the first time, prove for every address and non-zero alignment that align_down is the largest multiple at or below and align_up the smallest at or above when it fits, that both pass is_aligned and lie within one alignment, and restate the old witnesses.
Checks, over alignments including 3, 7, 12 and 4097, that PhysAddr align_down and align_up return an address that passes is_aligned and lies within one alignment on the right side, the three and page witnesses for VirtAddr, and that an alignment of zero leaves both unchanged. All three fail against the old masks.
PortStatsSnapshot::total_ops and total_bytes summed counters with +. The counters wrap in fetch_add, so a snapshot can hold any values, and with overflow checks on in every profile a sum past u64::MAX aborted the kernel. PortStats::total_ops, which PortManager reports, did the same over four live loads. The snapshot sums now saturate, as the MMIO snapshot's do, and PortStats::total_ops takes a snapshot and asks it. The extraction is regenerated. The refinement, verified here and committed for the first time, proves both totals never fail and are the saturated sums of their fields, with io_delays never counted.
Checks that the port snapshot's byte and operation totals saturate at u64::MAX on the first sum past it and count the four operation kinds but not I/O delays. Fails against the old unchecked sums.
Zeroed aarch64 and riscv64 user contexts hold no register and are what the entry guards refuse; the zeroed FPU states round to nearest with no flag and, on aarch64, enable no trap where a zero MXCSR traps every condition. rflags sanitisation keeps exactly the bits outside the privileged positions and resumes user code with IOPL 0 and interrupts on. Syscall arguments read the register at their index and refuse index six and above; the CPL is the low two bits of CS; page fault info reads one bit per flag and agrees with the dispatch model; signal errors map to their errnos. Each file was checked against a mutant of its generated code that makes a theorem false.
MAIR attribute indices fit ATTRINDX, are injective and name the byte each type encodes; an empty page table entry is the decoding of zero and maps nothing. The VT-d capability readers take exactly their bits: caching mode, write buffer flush, the domain count, the address width, the best leaf level and the fault record reason and source. The MMIO range check admits exactly the non-empty windows that do not overflow, and align4 rounds up to a multiple of four and halts only when that leaves the word. Each file was checked against a mutant of its generated code that makes a theorem false.
GIC and PLIC bases are stored and read where they are created; the IRQ reservation table reads and sets bit gsi mod 64 of word gsi div 64 and refuses lines past 256; MADT overrides read both polarity and trigger bits. HPET timer registers sit 0x20 apart, never alias and fit below 0x500 for the 32 reportable timers. The APIC divider encodes each supported divisor as the SDM reads it and the calibration stays in its bounds. MSI-X entries split the address losslessly, device ids match on vendor and device alone, and the I2C, PIO and bridge readers are exact. Each file was checked against a mutant of its generated code that makes a theorem false.
AML controllers are valid exactly when base and size are nonzero; SDT entry counts cover the table and never read past it; SRAT processor entries read bit zero and the little endian domain; the L2 associativity decode matches the CPUID table. Nine UEFI memory types are neither usable nor reserved, recorded as a hazard for a future caller. The civil calendar is the Gregorian rule and its months add up to the year; BCD converts both ways below one hundred; the RTC periodic rate is the datasheet code and divider output. Each file was checked against a mutant of its generated code that makes a theorem false.
Buddy, heap and region statistics give the free memory as the saturating or truncated difference and fill the total; a region total past u64::MAX is refused, not wrapped. The semaphore, seqlock and ring index arithmetic refine the tier-one models, including the seqlock counter wrapping and the ring refusing a zero capacity. Field element constants denote zero and one, entropy byte counts are the ceiling of bits over eight, and the constructors keep their arguments. Each file was checked against a mutant of its generated code that makes a theorem false.
ct_is_zero_u64 calls u64::wrapping_neg, which the extraction leaves opaque, and the full build's axiom listing names it. The theorem that reads it takes two's complement negation as a stated hypothesis, so the axiom carries no weight in a proof; ASSUMPTIONS.md now says so, and stated_axioms.py passes on a clean full build.
align, ct, ed_field, elf, iommu, paging, rv_flags, signal, uefi_attrs and vectors were committed without the Cargo.lock that every other extraction crate carries. Each names only its own package, so the lockfile pins nothing external; it keeps the crates alike and stops a build from leaving them untracked.
Contributor
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
Release-mode integer wrapping can bypass new IOMMU bounds checks, and oversized RSDP payload bytes remain unchecked.
Review effort: Balanced
Findings: 1
Open (2)
What changed in this PR
Expands Lean verification coverage, adds extraction roots and regression tests, and fixes kernel defects uncovered by proofs.
Changes:
- Adds substantive Lean properties and tighter proof accounting.
- Fixes firmware, memory, IOMMU, PCI, procfs, BTI, VGA, and alignment defects.
- Adds host regression tests and missing extraction lockfiles.
| File | Description |
|---|---|
verification/extraction/vectors/Cargo.lock |
Adds extraction lockfile. |
verification/extraction/uefi_attrs/Cargo.lock |
Adds extraction lockfile. |
verification/extraction/tree/layout_stack_slots/src/memory/mod.rs |
Mirrors memory module. |
verification/extraction/tree/layout_stack_slots/src/memory/layout/mod.rs |
Mirrors layout modules. |
verification/extraction/tree/layout_stack_slots/src/memory/layout/manager/mod.rs |
Includes stack-slot source. |
verification/extraction/tree/layout_stack_slots/src/lib.rs |
Adds extraction wrapper. |
verification/extraction/tree/layout_stack_slots/Cargo.toml |
Defines extraction crate. |
verification/extraction/tree/layout_stack_slots/Cargo.lock |
Locks extraction crate. |
verification/extraction/tree/iommu_regs_window/src/lib.rs |
Adds register-window wrapper. |
verification/extraction/tree/iommu_regs_window/src/arch/x86_64/mod.rs |
Mirrors x86 module. |
verification/extraction/tree/iommu_regs_window/src/arch/x86_64/iommu/regs/offsets/mod.rs |
Includes offset logic. |
verification/extraction/tree/iommu_regs_window/src/arch/x86_64/iommu/regs/mod.rs |
Mirrors register modules. |
verification/extraction/tree/iommu_regs_window/src/arch/x86_64/iommu/mod.rs |
Mirrors IOMMU module. |
verification/extraction/tree/iommu_regs_window/src/arch/mod.rs |
Mirrors architecture module. |
verification/extraction/tree/iommu_regs_window/Cargo.toml |
Defines extraction crate. |
verification/extraction/tree/iommu_regs_window/Cargo.lock |
Locks extraction crate. |
verification/extraction/sweep/vga_constants/src/lib.rs |
Exposes color constructor. |
verification/extraction/sweep/variable_firmware/src/lib.rs |
Exposes revision packing. |
verification/extraction/sweep/utils_types/src/lib.rs |
Exposes hidden-file predicate. |
verification/extraction/sweep/bti_pad/src/lib.rs |
Adds BTI extraction wrapper. |
verification/extraction/sweep/bti_pad/Cargo.toml |
Defines BTI extraction. |
verification/extraction/sweep/bti_pad/Cargo.lock |
Locks BTI extraction. |
verification/extraction/signal/Cargo.lock |
Adds extraction lockfile. |
verification/extraction/rv_flags/Cargo.lock |
Adds extraction lockfile. |
verification/extraction/paging/Cargo.lock |
Adds extraction lockfile. |
verification/extraction/lean/NonosExtraction/WalkerAlignRefinement.lean |
Proves four-byte alignment. |
verification/extraction/lean/NonosExtraction/VgaColors.lean |
Regenerates VGA model. |
verification/extraction/lean/NonosExtraction/VariableFirmware.lean |
Models revision packing. |
verification/extraction/lean/NonosExtraction/ValidationSimdLevelRefinement.lean |
Proves SIMD widths. |
verification/extraction/lean/NonosExtraction/UtilsTypes.lean |
Models hidden-only scans. |
verification/extraction/lean/NonosExtraction/Uefi.lean |
Models authentication flags. |
verification/extraction/lean/NonosExtraction/TypesStatsSnapshot.lean |
Models saturating totals. |
verification/extraction/lean/NonosExtraction/TypesSnapshotRefinement.lean |
Proves empty DMA statistics. |
verification/extraction/lean/NonosExtraction/TypesRegionStatsRefinement.lean |
Proves saturating free memory. |
verification/extraction/lean/NonosExtraction/TypesPteRefinement.lean |
Proves empty PTE semantics. |
verification/extraction/lean/NonosExtraction/TypesProtectionRefinement.lean |
Proves protection predicates. |
verification/extraction/lean/NonosExtraction/TypesPercpu.lean |
Models safe region arithmetic. |
verification/extraction/lean/NonosExtraction/TypesFirmwareRefinement.lean |
Proves empty firmware handoff. |
verification/extraction/lean/NonosExtraction/TypesBridgeRefinement.lean |
Characterizes default bridge. |
verification/extraction/lean/NonosExtraction/TrampolinePerApRefinement.lean |
Proves boot-context construction. |
verification/extraction/lean/NonosExtraction/TablesMemoryDesc.lean |
Models saturating descriptors. |
verification/extraction/lean/NonosExtraction/SignalErrorRefinement.lean |
Proves errno mappings. |
verification/extraction/lean/NonosExtraction/Riscv64FpuContextRefinement.lean |
Proves zeroed FPU state. |
verification/extraction/lean/NonosExtraction/RegistryVersionRefinement.lean |
Proves version construction. |
verification/extraction/lean/NonosExtraction/RegistersPlicRefinement.lean |
Proves PLIC base preservation. |
verification/extraction/lean/NonosExtraction/RedistributorDeviceRefinement.lean |
Proves redistributor addresses. |
verification/extraction/lean/NonosExtraction/ProcfsTypesRefinement.lean |
Updates inode documentation. |
verification/extraction/lean/NonosExtraction/ProcfsPidInode.lean |
Models collision-free inodes. |
verification/extraction/lean/NonosExtraction/PortStatsSnapshot.lean |
Models saturating port totals. |
verification/extraction/lean/NonosExtraction/PlonkTypesRefinement.lean |
Proves empty PLONK values. |
verification/extraction/lean/NonosExtraction/PioTypesRefinement.lean |
Proves PIO widths. |
verification/extraction/lean/NonosExtraction/PciTypesMsixRefinement.lean |
Proves MSI-X construction. |
verification/extraction/lean/NonosExtraction/PciInfoRefinement.lean |
Proves I/O-window detection. |
verification/extraction/lean/NonosExtraction/PagingRefinement.lean |
Proves block predicates. |
verification/extraction/lean/NonosExtraction/PacKeyRefinement.lean |
Proves PAC key construction. |
verification/extraction/lean/NonosExtraction/MteModeRefinement.lean |
Proves MTE encodings. |
verification/extraction/lean/NonosExtraction/MemoryFrameAllocTypesRange.lean |
Regenerates alignment model. |
verification/extraction/lean/NonosExtraction/MainModeRefinement.lean |
Proves microkernel mode. |
verification/extraction/lean/NonosExtraction/LayoutStackSlots.lean |
Models guarded stack offsets. |
verification/extraction/lean/NonosExtraction/IommuProtectionRefinement.lean |
Proves IOMMU permissions. |
verification/extraction/lean/NonosExtraction/IommuDomainIdRefinement.lean |
Proves domain identifiers. |
verification/extraction/lean/NonosExtraction/HpetProtectionRefinement.lean |
Proves HPET decoding. |
verification/extraction/lean/NonosExtraction/HeapTypesStatsRefinement.lean |
Proves heap free-memory behavior. |
verification/extraction/lean/NonosExtraction/DriversPciTypesAddress.lean |
Models masked PCI addresses. |
verification/extraction/lean/NonosExtraction/DistributorDeviceRefinement.lean |
Proves distributor addresses. |
verification/extraction/lean/NonosExtraction/DispatchArgsRefinement.lean |
Proves syscall argument placement. |
verification/extraction/lean/NonosExtraction/DiagCplRefinement.lean |
Proves CPL decoding. |
verification/extraction/lean/NonosExtraction/DataStatsRefinement.lean |
Proves zeroed ACPI statistics. |
verification/extraction/lean/NonosExtraction/DataProcessorRefinement.lean |
Proves processor construction. |
verification/extraction/lean/NonosExtraction/DataIoapicRefinement.lean |
Proves saturated GSI maximum. |
verification/extraction/lean/NonosExtraction/DataIoapic.lean |
Models saturated GSI arithmetic. |
verification/extraction/lean/NonosExtraction/CtPrimitivesRefinement.lean |
Updates constant-time proof status. |
verification/extraction/lean/NonosExtraction/CoreSection.lean |
Models strict symbol tables. |
verification/extraction/lean/NonosExtraction/ContractArgsRefinement.lean |
Proves indexed syscall arguments. |
verification/extraction/lean/NonosExtraction/ContextCpuContextRefinement.lean |
Proves initial CPU context. |
verification/extraction/lean/NonosExtraction/ConstantsAddressPacking.lean |
Models masked PCI packing. |
verification/extraction/lean/NonosExtraction/ChainErrorRefinement.lean |
Proves recoverable errors. |
verification/extraction/lean/NonosExtraction/CensusBufRefinement.lean |
Proves empty line buffer. |
verification/extraction/lean/NonosExtraction/CapBehaviourRefinement.lean |
Proves capability bits. |
verification/extraction/lean/NonosExtraction/CacheTypesRefinement.lean |
Proves cache counter initialization. |
verification/extraction/lean/NonosExtraction/BtiPad.lean |
Models BTI landing pads. |
verification/extraction/lean/NonosExtraction/BtiGuardRefinement.lean |
Proves BTI guard encodings. |
verification/extraction/lean/NonosExtraction/AlgIdTypesRefinement.lean |
Proves algorithm identifiers. |
verification/extraction/lean/NonosExtraction/AddrVirt.lean |
Regenerates virtual alignment. |
verification/extraction/lean/NonosExtraction/AddrPhys.lean |
Regenerates physical alignment. |
verification/extraction/lean/NonosExtraction/Aarch64ContextTypesRefinement.lean |
Proves zeroed AArch64 contexts. |
verification/extraction/iommu/Cargo.lock |
Adds extraction lockfile. |
verification/extraction/elf/Cargo.lock |
Adds extraction lockfile. |
verification/extraction/ed_field/Cargo.lock |
Adds extraction lockfile. |
verification/extraction/ct/Cargo.lock |
Adds extraction lockfile. |
verification/extraction/crates.json |
Registers new extraction roots. |
verification/extraction/ASSUMPTIONS.md |
Records wrapping-negation assumption. |
verification/extraction/align/Cargo.lock |
Adds extraction lockfile. |
userland/kernel_proofs/src/vga_attr/tests.rs |
Tests VGA attribute masking. |
userland/kernel_proofs/src/vga_attr/mod.rs |
Wires VGA regression tests. |
userland/kernel_proofs/src/uefi_revision/tests.rs |
Tests UEFI revision encoding. |
userland/kernel_proofs/src/uefi_revision/mod.rs |
Wires revision tests. |
userland/kernel_proofs/src/uefi_attrs/tests.rs |
Tests authentication flags. |
userland/kernel_proofs/src/uefi_attrs/mod.rs |
Wires attribute tests. |
userland/kernel_proofs/src/scan_hidden/tests.rs |
Tests hidden-only scans. |
userland/kernel_proofs/src/scan_hidden/mod.rs |
Wires scan tests. |
userland/kernel_proofs/src/rsdp_address/tests.rs |
Tests RSDP validation. |
userland/kernel_proofs/src/rsdp_address/mod.rs |
Documents RSDP regressions. |
userland/kernel_proofs/src/procfs_inode/tests.rs |
Tests inode uniqueness. |
userland/kernel_proofs/src/procfs_inode/mod.rs |
Documents inode regressions. |
userland/kernel_proofs/src/pci_address/tests.rs |
Tests PCI field masking. |
userland/kernel_proofs/src/pci_address/mod.rs |
Includes PCI address helper. |
userland/kernel_proofs/src/lib.rs |
Registers new test modules. |
userland/kernel_proofs/src/layout_slots/tests.rs |
Tests stack guards. |
userland/kernel_proofs/src/layout_slots/mod.rs |
Wires stack-layout tests. |
userland/kernel_proofs/src/layout_slots/manager/mod.rs |
Includes stack-slot source. |
userland/kernel_proofs/src/layout_slots/constants/mod.rs |
Includes layout constants. |
userland/kernel_proofs/src/iommu_window/tests.rs |
Tests IOMMU bounds. |
userland/kernel_proofs/src/iommu_window/mod.rs |
Wires IOMMU tests. |
userland/kernel_proofs/src/firmware_arith/tests.rs |
Tests saturating arithmetic. |
userland/kernel_proofs/src/firmware_arith/mod.rs |
Wires arithmetic tests. |
userland/kernel_proofs/src/elf/loader/core/mod.rs |
Includes section implementation. |
userland/kernel_proofs/src/elf_section_tests.rs |
Tests symbol-table filtering. |
userland/kernel_proofs/src/efi_time/tests.rs |
Tests EFI calendar conversion. |
userland/kernel_proofs/src/efi_time/mod.rs |
Wires EFI time tests. |
userland/kernel_proofs/src/bti_pad/tests.rs |
Tests valid landing pads. |
userland/kernel_proofs/src/bti_pad/mod.rs |
Wires BTI tests. |
userland/kernel_proofs/src/addr_align/tests.rs |
Tests arbitrary alignments. |
userland/kernel_proofs/src/addr_align/mod.rs |
Wires alignment tests. |
src/memory/mmio/types/stats_snapshot.rs |
Saturates MMIO totals. |
src/memory/layout/types/percpu.rs |
Fixes top-address regions. |
src/memory/layout/manager/stack_slots.rs |
Defines guarded stack offsets. |
src/memory/layout/manager/percpu.rs |
Applies stack offsets. |
src/memory/layout/manager/mod.rs |
Registers stack-slot module. |
src/memory/addr/virt.rs |
Fixes virtual alignment. |
src/memory/addr/phys.rs |
Fixes physical alignment. |
src/fs/utils/types.rs |
Implements hidden-only configuration. |
src/fs/utils/scan_config.rs |
Applies hidden-file predicate. |
src/fs/procfs/pid/entry.rs |
Shares inode shift constant. |
src/fs/procfs/pid_inode.rs |
Fixes process inode numbering. |
src/elf/loader/core/section.rs |
Restricts full symbol tables. |
src/drivers/pci/constants/address_packing.rs |
Masks PCI fields. |
src/boot/vga/colors.rs |
Masks VGA backgrounds. |
src/arch/x86_64/vga/constants.rs |
Fixes color-code packing. |
src/arch/x86_64/uefi/types/attributes.rs |
Recognizes legacy authentication. |
src/arch/x86_64/uefi/tables/time.rs |
Fixes calendar validation. |
src/arch/x86_64/uefi/tables/memory_desc.rs |
Saturates descriptor arithmetic. |
src/arch/x86_64/uefi/manager/init.rs |
Uses canonical revision constant. |
src/arch/x86_64/uefi/constants/revisions.rs |
Standardizes revision encoding. |
src/arch/x86_64/port/stats_types.rs |
Reuses saturated snapshot total. |
src/arch/x86_64/port/stats_snapshot.rs |
Saturates port totals. |
src/arch/x86_64/multiboot/state/parse/firmware.rs |
Parses RSDP reserved bytes. |
src/arch/x86_64/multiboot/modules_acpi.rs |
Strengthens RSDP checksum checks. |
src/arch/x86_64/iommu/unit/report/failure.rs |
Reports window-bound failures. |
src/arch/x86_64/iommu/unit/probe.rs |
Rejects oversized register layouts. |
src/arch/x86_64/iommu/unit/access.rs |
Makes MMIO checks unconditional. |
src/arch/x86_64/iommu/regs/window.rs |
Validates register extents. |
src/arch/x86_64/iommu/regs/mod.rs |
Exposes window validation. |
src/arch/x86_64/acpi/data/ioapic.rs |
Saturates GSI maximum. |
src/arch/aarch64/security/bti/pad.rs |
Defines valid BTI pads. |
src/arch/aarch64/security/bti/landing.rs |
Uses shared BTI validation. |
src/arch/aarch64/security/bti.rs |
Registers BTI pad module. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
RemapUnit's accessors checked offset + width <= UNIT_WINDOW. An offset near usize::MAX wraps that sum to a small value wherever overflow checks are off, so the check passed and the volatile access went outside the mapped page; with overflow checks on, as in the kernel profiles, the same offset panicked in the accessor instead of failing its bound. Each accessor now checks offset <= UNIT_WINDOW - width, which cannot wrap for any offset. Reported in review of #591.
Runs the kernel's RemapUnit accessors against a buffer standing in for the mapped page: the last 32 and 64 bit registers in the window read back, and offsets past it, including ones near usize::MAX that wrap offset + width, are refused. The second test fails against the old check.
verify_extended_checksum accepted any declared length of 36 or more while summing only the 36 bytes the structure keeps. The extended checksum covers the length the table declares, so a longer declaration left the bytes past 36 unchecked and still passed. Only the 36 byte structure is supported, so any other length is now refused. Reported in review of #591. The extraction is regenerated and the refinement restates the check as a length of exactly 36; the theorem for short tables now covers every length other than 36.
Checks that a revision 2 RSDP whose 36 bytes sum to zero but whose declared length is 37, 40, 4096 or u32::MAX fails the extended check. Fails against the old length test, which accepted any length of 36 or more.
Contributor
Author
|
Review follow-ups: the IOMMU register accessors bound offsets by subtraction so no offset can wrap past the check, and the ACPI 2.0 RSDP check accepts only the 36 byte length the parser keeps. Fixed in 3cd4611. Each accessor now checks offset <= UNIT_WINDOW - width instead of offset + width <= UNIT_WINDOW, so no offset can wrap past the bound. The kernel profiles build with overflow checks on, so the old sum would have panicked rather than wrapped, but that still turned a bad offset into a crash inside the accessor and a build without overflow checks did wrap. c7a1b01 adds a kernel_proofs test that runs the accessors against a buffer standing in for the page; it fails against the old check for offsets near usize::MAX. Fixed in 224bc6f. The structure keeps only the 36 bytes of an ACPI 2.0 RSDP, so the extended check now refuses any declared length other than 36 instead of accepting longer ones with unchecked bytes. The Lean refinement is restated to a length of exactly 36, and 175d2e5 adds a test that lengths 37, 40, 4096 and u32::MAX are refused which fails against the old check. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this does
This continues the Lean work merged in #590. It raises the number of kernel functions with a real proved property from 330 to 494, tightens the counter so a function only counts when a theorem actually states something about it and fixes 15 kernel defects that the proofs brought to light. Every fix comes with a host test that fails against the old code.
Numbers
All percentages are of the 11,450 functions in src/. The target is 1,717 functions with a property beyond their wrapper.
Main reports 336 with the old counter. The 330 above is what main scores under the stricter counter this PR introduces, so the two columns are measured the same way. The floors in proven_functions.py are raised to 987 and 494 and the gap ceiling stays at zero. No gate was lowered.
A stricter counter
proven_functions.py used to count a function as substantive whenever its name appeared anywhere in a refinement file, prose included. It now reads only theorem statements, follows "open ... renaming" and abbreviations to the names they stand for, and ignores the theorems that only show a wrapper calls its method. At the time of the change that dropped six functions the old counter had credited: the three constant-time select functions, ct_is_zero_u64, ct_clz_u64, the IOMMU second-level index and address-width checks, and the two page table block predicates. Each of them now has a theorem of its own.
Kernel fixes
Each fix is its own commit. The extraction is regenerated in the same commit and the theorem that recorded the defect is restated to the fixed behaviour. A separate kernel_proofs commit follows with a test that includes the kernel file by path and fails against the old code. Every restated theorem was also checked against a deliberately broken copy of the new generated code, and fails on it.
Security relevant:
Lower severity:
Kept on purpose, and said so in the proof: is_user_space refuses the topmost user page, which avoids the SYSRET return to a non-canonical address, the same choice Linux makes. Recorded but not changed: reset_ticks does not fit the model of a clock that only moves forward, and nothing calls it.
Refinements committed
74 refinement files that were written earlier but never committed were checked one by one. Each compiles against the current tree with no error, warning or sorry, was read for padding and dashes, and was run against a broken copy of its generated code: a changed literal, a flipped boolean or operator, or for simple constructors and readers a swapped or zeroed field. Every one of them fails under its broken copy. Two of them recorded the address rounding and port statistics defects fixed above. The rest are committed in five groups by area: CPU context and syscall registers, memory attributes and IOMMU capabilities, interrupt controllers and PCI, firmware tables and clocks, and allocator statistics with the pure synchronisation models. Fifteen other files had nothing worth proving, being empty skeletons, duplicates of committed crates, or stubs, and were left out.
5 older refinements were restated because the defects they recorded are now fixed: the invalidation and fault register offsets, the per-CPU stack region, the user space bound, and the tick counter.
Housekeeping
Checks run locally