Ignition logo

Rust ยท deterministic boot simulator

Watch a machine boot,
one stage at a time.

Ignition is a deterministic boot sequence simulator in pure, safe Rust with zero dependencies. It models the whole chain from firmware power-on to kernel hand-off, and the parts that are genuinely testable, the MBR parser, the boot config parser, and the ELF-like kernel loader, are real code checked by a correctness gate. Step firmware, stage 1, stage 2, the partition table, the filesystem, the config, the segment load, the real to protected mode switch, and the jump. Or feed it a malformed disk and watch a parser refuse it.

Step the boot View on GitHub
How to use this playground
  1. Step advances the boot by exactly one stage. Watch the highlighted stage pill, the new console line, and the panels below fill in.
  2. Run plays the remaining stages automatically, about one every 700 ms. Press it again to pause.
  3. Reset returns the machine to power-on so you can start again.
  4. The Disk image menu swaps the disk. Pick a malformed image to watch a specific parser or the loader reject it instead of loading a corrupt kernel.
Guided tour: start with the valid image and press Step seven times to reach the kernel header. Keep stepping and watch the memory map fill, one segment at a time, with the pure bss segment showing its zero-filled bytes. Two more steps flip the CPU chip from real mode to protected mode and jump to the entry point, where the stub kernel prints its proof of life. Then choose bad ELF magic from the menu, reset, and step through again to see the loader refuse the image.

Boot simulator

Step the boot chain one stage at a time, or pick a malformed disk and watch a parser reject the image.

Boot transcript
CPU real mode to A20 masked
Parsed headers
Memory map after load
14boot stages
3kernel segments
8memory regions
6disk images
16 MiBsimulated RAM

The parsers are real, and gated

The partition table parser, the boot config parser, and the ELF-like kernel loader are not mock-ups. They parse real bytes and enforce real invariants, checked by the gate in tests/gate.rs, a bounded stress harness in tests/stress.rs, and unit tests in each module. Five claims are proven.

# the five gate claims (cargo test)
1 load correctness     RAM after load equals a reference built from the parsed
                       headers, byte for byte, bss beyond filesz is zeroed
2 validation          bad signature, bad magic, out-of-range, overlapping,
                       or truncated images are rejected, and RAM stays all zero
3 determinism         a valid disk yields an identical log and memory map
4 A/B atomicity       a corrupt slot A falls back to B; RAM equals a B reference,
                       which can only hold if the failed load wrote nothing
5 memmap soundness    regions come out sorted, disjoint, and inside RAM

Claim 4 is the sharp one: the fallback can only match an independent reference for slot B if the rejected slot A load wrote nothing, so the atomicity of the rejection is proven by the feature that depends on it.

A corrupt kernel falls back, atomically

The ab-demo disk has a corrupt slot A. The loader rejects it, writes nothing, and boots the backup slot B instead. This is a real transcript, trimmed.

$ cargo run -- ab-demo
[igfs] superblock ok, config 93 bytes, slot A 162 bytes, slot B 162 bytes
[slot] slot A failed to load (kernel image error: bad kernel magic:
       found [58, 49, 4d, 47]), trying slot B
[elf] slot B KIMG v1, entry 0x100000, 3 segment(s)
[load] segment 0: 19 bytes file + 0 bytes bss at 0x100000 [r-x]
[load] segment 2: 0 bytes file + 4096 bytes bss at 0x102000 [rw-]
[cpu] A20 enabled, entered protected mode
[handoff] jump to entry 0x100000 in protected mode
[kernel] 'IGNITED' running from slot B, read 8 memory map region(s), boot complete

How it compares

Ignition is a model, not a bootable artifact, and that line is drawn on purpose.

GRUB, coreboot, U-Boot

Real bootloaders that run on bare metal and actually start a machine. They are the ground truth, and precisely because they run on hardware they cannot be exercised with cargo test or stepped inside a web page.

Ignition

The readable teaching model of the same chain. The partition, config, and ELF-like loader are real parsers that enforce real invariants and are checked by a gate, while the machine around them, the disk, the flat memory, and the CPU mode, is simulated. It adds an A/B slot design so a corrupt primary kernel falls back to a backup, and the fallback proves the rejection wrote nothing.

The parts that are real code

Each of these parses real bytes, enforces real invariants, and is covered by the gate in tests/gate.rs.

parser MBR partition table

parse_mbr validates the 0x55AA boot signature and every partition entry, so a disk with a bad signature is refused at stage 1.

parser Boot config

parse_config reads the kernel path, the cmdline, and the timeout from the config text and validates them before the loader runs.

parser IGFS superblock

parse_superblock names the config and the two kernel slots A and B, and validates every extent against the partition bounds.

loader ELF-like kernel image

parse_header, parse_program_headers, validate_segments, and load place each segment at its virtual address and zero the bss beyond the file size. build_image is the exact inverse.

loader A/B slots

A corrupt primary slot is rejected atomically and the loader boots the backup, proven by the fallback RAM equalling an independent slot B reference.

machine Memory map and mode switch

Every boot leaves a sorted, disjoint memory map inside RAM, and the CPU makes the real mode to protected mode transition with A20 enabled before the jump to the entry point.

Use it

# boot the bundled demo disk and print the whole chain
cargo run -- demo
cargo run -- ab-demo             # A slot corrupt, watch the fallback to B
cargo run -- boot IMAGE          # boot a disk image file

# unit tests, the correctness gate, and the stress harness
cargo test
IGNITION_FUZZ_OPS=5000 cargo test