seL4’s AArch64 Security Proof Closes a Major Gap

Picture a small Arm-based computer running a safety-critical controller beside a third-party application. The attraction is clear: one compact device can host several jobs. The difficult part is showing that a flaw in one program cannot become a bridge into the other.

That is why Proofcraft’s August 2026 announcement matters. The team has completed the security proofs for seL4 on AArch64, the 64-bit Arm architecture. This is not a claim that a test suite happened to find no bugs. It is a machine-checked mathematical argument that, under defined assumptions and a correct system configuration, the kernel enforces strong isolation between applications.

seL4 starts with a very small trusted core

seL4 is a microkernel: a deliberately small operating-system kernel that keeps only the most fundamental mechanisms in privileged code. Device drivers, communication services, and other operating-system features can run outside that core as user-level components. That design leaves less code in the part of the system that every application must trust.

Access is controlled with capabilities. A capability is an unforgeable token that refers to a particular kernel object and carries rights such as read, write, send, or receive. The kernel checks the capability whenever a component requests an operation.

A conceptual policy might look like this:

untrusted_app:
 read: own_memory
 send: trusted_service_endpoint

trusted_service:
 read/write: own_memory
 receive: untrusted_app

This is not seL4 configuration syntax. It is a small sketch of the idea: the untrusted application can communicate through an explicitly granted endpoint, but it has no capability for the trusted service’s private memory. The proof depends on this policy being designed and installed correctly. A kernel cannot repair an access rule that gives the wrong component the wrong authority.

The proof stack arrives one layer at a time

Formal verification means describing software and its desired behavior in precise mathematics, then using a proof assistant—a program that checks logical proof steps—to establish that the two match. seL4’s assurance story is built as a stack rather than a single stamp of approval.

The first major layer is functional correctness. It says that the verified C implementation behaves according to the abstract seL4 specification. Proofcraft completed that AArch64 milestone on April 1, 2024. The next layer was integrity, completed for AArch64 in April 2025: an application cannot modify protected data without the required authority.

Confidentiality addresses the opposite direction. It says an application cannot learn information from another application without permission. Availability is the related guarantee that an application cannot block another component from using resources it is authorized to use. Taken together, these properties describe an operating-system boundary that does more than prevent accidental memory writes. It restricts who may change, observe, or interfere with the state of other components.

How do you prove that secret information did not escape?

The confidentiality proof relies on a demanding idea called noninterference. Rather than looking only for a direct read from a secret memory page, the proof compares two hypothetical executions of the system. The executions are identical except for some secret data. If an unauthorized observer sees the same allowed behavior in both runs, then that secret did not influence what the observer could learn.

This style of reasoning matters because information can hide in places that do not look like ordinary application memory. A kernel might accidentally leave data in shared state, a saved register, or a buffer that is reused during a context switch. The proof has to show that these storage channels do not carry forbidden information between security domains.

AArch64 made that work more involved. Its verified seL4 configuration includes hypervisor support, which allows the kernel to host guest operating systems, along with FPU support. An FPU, or floating-point unit, performs arithmetic on decimal-style numerical values. The processor registers used by an FPU hold state outside normal memory. A VCPU, or virtual central processing unit, represents processor state presented to a guest operating system.

Those registers can retain information across context switches unless the kernel handles them correctly. The AArch64 confidentiality proof therefore had to account for VCPU and FPU state, not only pages and capability tables. This is a good example of why security verification is more than checking a few permission branches: the proof must follow information through the machine’s less visible corners.

What changes for AArch64 systems?

AArch64 is an architecture, not one particular board. A verified result applies to supported combinations of hardware, kernel configuration, and features. It does not automatically cover every Arm chip or every possible build option.

Within those verified configurations, the milestone gives system designers a stronger foundation for placing critical and untrusted workloads on the same device. A compromised application may still misuse an interface that the system intentionally grants it, and its own bugs remain its own bugs. What it should not be able to do is turn an absent capability into unauthorized access to another component’s data or authority.

That containment is useful in embedded controllers, secure gateways, robotics, industrial equipment, and systems that need to host a virtual machine beside more trusted software. The kernel becomes a mathematically checked enforcement point rather than a boundary supported mainly by testing and review.

The assumptions are part of the result

A formal proof is strongest when its boundary is stated plainly. seL4’s proof assumes that the underlying hardware behaves according to its specification, that the small amount of handwritten assembly is correct, and that low-level cache and address-translation management work as required. The proof also starts after the kernel has been loaded and placed into a consistent initial state, so boot code remains a separate concern.

Direct memory access, usually called DMA, is another important boundary. DMA lets a device read or write memory without each transfer being performed by the CPU. A device that can overwrite kernel memory can defeat isolation unless it is controlled, trusted, or covered by additional verification.

The confidentiality theorem also does not promise protection from every side channel. A side channel is an indirect signal, such as how long an operation takes, that can reveal information without a forbidden memory read. The current proof covers the channels represented in its model, including in-kernel storage channels, but timing channels require separate analysis and protection.

System initialization is another layer still. The security theorem can state what must be true about capabilities and information-flow policies, while initialization mechanisms help ensure the running system actually receives that intended configuration.

The word complete should therefore be read precisely. The AArch64 security proof completes a major part of seL4’s assurance stack: the verified kernel can enforce confidentiality alongside its functional-correctness and integrity results, under explicit assumptions. It is not a guarantee that every application, driver, boot path, or hardware device is secure by association. It is something more useful: a much firmer floor beneath the work of building the rest of the system.