Embedded systems often sit at an uncomfortable intersection: constrained resources, long service lives, physical consequences, and software that is difficult to update once deployed. We can test these systems extensively and still miss a rare sequence of events. That's where formal verification becomes interesting.
This article follows my practical notes on setting up Microkit in QEMU, defining protection domains, and connecting those domains with channels. Those tutorials show how to assemble a small system. Here I want to explore a different question: what can we actually claim about its correctness and security?
Testing Gives Examples; Proofs Establish Properties
Testing asks whether a particular execution behaves as expected. It is essential: boot the image, exercise the interfaces, observe the outputs, and inspect failure cases. But even a large test suite samples a limited set of possible executions.
Formal verification starts by stating a property precisely and then proving, under explicit assumptions, that the model or implementation satisfies it. That does not mean every conceivable property is proven. The value comes from narrowing the gap between what we intend a component to do and what we can justify it will do.
A proof is only as relevant as its specification, assumptions, and connection to the deployed system.
Why seL4 Is a Useful Case Study
seL4 is a microkernel with a substantial body of machine-checked verification work. Its architecture emphasizes explicit authority through capabilities and a comparatively small kernel interface. Those features help make isolation and access-control reasoning tractable.
It is important to distinguish several claims:
- Functional correctness concerns whether an implementation refines its formal specification.
- Security properties, such as integrity or information-flow properties, require their own definitions and proof obligations.
- System assurance must also account for boot firmware, hardware, drivers, application code, configuration, operational procedures, and assumptions outside the verified kernel.
A verified kernel is not a blanket proof that every application running above it is secure.
A Concrete Refinement Claim
The seL4 verification story is more specific than saying that the kernel has been "mathematically proven secure." In the classic functional-correctness result, an abstract specification of kernel behavior is related to a more concrete executable specification, and then to the C implementation using machine-checked refinement proofs in Isabelle/HOL. Roughly, the proof argues that the implementation's observable behavior is consistent with the abstract specification, subject to its assumptions and the supported verified configuration.
That is a powerful claim, but it is not equivalent to proving the absence of every vulnerability. If the abstract specification permits an operation, refinement does not make that operation safe in every application context. Nor does a kernel proof automatically cover unverified device firmware, all assembly code, every hardware configuration, or the software running in user space.
This matters when we read a security claim. We should ask: which artifact was proved against which specification, for which configuration, and under which assumptions? A verified property is not a synonym for a verified product.
Capabilities, Mappings, and Authority
A capability is an unforgeable kernel-mediated reference that conveys specific authority over an object. Possessing a capability and possessing a usable virtual address are related but distinct concerns: memory access ultimately depends on the configured address-space mappings and permissions, which are established through kernel-managed authority.
For a simplified two-domain design, imagine a sensor domain and an analysis domain:
| Resource or path | Sensor domain | Analysis domain |
|---|---|---|
| Sensor-private memory | Read/write | No mapping |
| Analysis-private memory | No mapping | Read/write |
| Explicit shared buffer | Write, as configured | Read, as configured |
| Notification channel | Send, as configured | Receive, as configured |
This is an illustrative policy, not a Microkit system description or evidence of a completed experiment. A real implementation needs concrete memory-region definitions, virtual mappings, permissions, channel identifiers, and a review of any device access or shared state. Notification channels signal events; they do not by themselves transfer arbitrary memory contents. Shared memory must be explicitly arranged if the domains exchange data through a buffer.
The interesting negative requirement is: the analysis domain cannot directly write the sensor domain's private memory. To support it, we must inspect the mappings and authority that could permit the write, including any shared aliases or privileged intermediaries. Merely observing that ordinary code does not perform a write is insufficient.
A Testable Isolation Hypothesis
Suppose the analysis domain intentionally attempts a store to a virtual address that is not mapped with write permission in its address space. On an appropriately configured AArch64 system, the expected result is a synchronous data-abort exception rather than a successful modification of sensor-private memory. The exact fault report and subsequent behavior depend on the kernel, Microkit fault-handling configuration, and build.
That test is useful for catching an accidental mapping or permission error. It does not establish noninterference for every execution, nor does it rule out indirect influence through authorized IPC, shared buffers, devices, timing, or other channels.
For a reproducible follow-up experiment, I would collect:
- The exact Microkit SDK and seL4 version, board, and configuration.
- The system description and a table of effective mappings and rights.
- A permitted communication test proving the intended path works.
- A denied-write test with the fault output and an independent check that protected data remains unchanged.
- A statement separating tested behavior from properties inherited from seL4's published proofs.
That evidence can support a narrow, falsifiable engineering claim. A formal information-flow or integrity claim would require an explicit model and proof obligations beyond this QEMU demonstration.
The Limits of the Trusted Computing Base
Kernel verification is most valuable when the rest of the design respects the boundary it establishes. A DMA-capable device, a shared memory region with overly broad rights, a buggy trusted service, or an incorrect system description can undermine a higher-level isolation objective even if the kernel behaves exactly as specified.
The trusted computing base is therefore a design decision, not just a property of the kernel binary. Reducing privileged code and documenting authority are concrete ways to make the argument easier to inspect. In systems using Microkit, that means treating the system description and the interfaces between protection domains as reviewable security artifacts.
Where Microkit Fits
Microkit makes it practical to describe a system in terms of protection domains, memory regions, and explicit communication relationships. Its system description becomes an architectural artifact that engineers can review alongside source code.
Consider a design with a sensor-facing domain and an analysis domain. Rather than allowing every component to share a large address space, we can document the memory and communication pathways each domain needs. That is valuable even before writing a formal proof: it makes authority visible and limits accidental coupling.
But a well-structured Microkit configuration is not automatically a formally verified application. We still need to validate configuration choices, interfaces, runtime behavior, and assumptions about the hardware and environment.
A Practical Assurance Workflow
For a small QEMU-based experiment, I would begin with five checkpoints:
- State the intended property. For example: the analysis domain must not directly modify the sensor domain's private memory.
- Identify the enforcement boundary. Which mapping, capability, or interface prevents that operation?
- Review the system description. Record the domains, memory mappings, channels, and any deliberately shared resources.
- Exercise the boundary. Build the system, test permitted communication, and attempt an unauthorized operation in a controlled test environment.
- Separate observation from proof. A failed access attempt is useful evidence, but it is not a mathematical proof that no violating execution exists.
This distinction is worth maintaining in design reviews and technical writing. We should describe exactly what was demonstrated, what is inherited from verified components, and what remains an engineering assumption.
What I Would Verify Next
The next practical exercise is to take a minimal pair of Microkit protection domains, document their allowed communication, and deliberately test a denied memory-access path in QEMU. That will give us an observable boundary to discuss without overstating the scope of the kernel's formal guarantees.
The larger lesson is that formal methods do not replace engineering judgment. They make some of our most important claims precise enough to challenge—and, where the evidence supports it, to prove.