Formal Verification Proves No Rights Escalation in Fuchsia Zircon Capability Model Using Isabelle/HOL

Researchers have constructed an Isabelle/HOL model of capability delegation drawn from Zircon, the microkernel of Google Fuchsia, and proved that transfers never escalate rights beyond those held by the source.

The model represents processes, handles, capability masks, channels, and VMO objects. It encodes the rule that a process may act on a kernel object only through a handle whose rights mask determines allowed operations. The central property verified is attenuation: after any transfer the recipient cannot obtain a right absent from the sender’s original mask.

Key theorems proved for all reachable states include channel_transfer_no_escalation, channel_write_requires_transfer, channel_write_moves_sender_handle, and zx_handle_duplicate_no_escalation. The model also shows that a direct MMIO write into vmo_store can violate isolation even while the capability check remains in place, providing an explicit negative witness.

The formalization deliberately stays within a compact teaching fragment. It abstracts zx_channel_write and zx_channel_write_etc to a single MOVE operation, omits byte payloads and DUPLICATE disposition arrays, and freezes state on error. Dependencies such as WRITE implying READ are marked as pedagogical simplifications not present in real Zircon.

Comparison with seL4 underscores different goals: seL4 delivers full refinement from specification to binary, whereas this work isolates the monotonic attenuation layer and shows it can be machine-checked without modeling the entire kernel. The artifact comprises six Isabelle theories and is rebuildable via isabelle build -d . Zircon.

The study notes that similar rights discipline matters for hypervisors handling device passthrough and MMIO regions, making the verified fragment relevant beyond Fuchsia itself.