MID-087: Utilization of Formally Verified OS (Micro-)Kernels

Mitigation Level: Leading

Description

Formal verification is the process of proving, typically with an aid of automated or semi-automated tooling, that a particular code module or function satisfies the desired requirements. Depending on the size and complexity of the code to be verified, formal verification can be a time-consuming effort requiring significant expertise. One way developers to leverage formal verification at lower cost is to use pre-existing code that has already been formally verified.

Critical security functions of a device’s OS kernel that have undergone formal verification have been inter-process communication (IPC), hardware interactions, managing the kernel stack and data spaces, handling process interrupts, and more. One example of a formally verified microkernel is seL4, whose implementation on ARM and RISCV64 has proofs demonstrating that the proper use of the kernel will enforce integrity and confidentiality, which are core security properties. What this means in the case of seL4 is that the kernel will always operate in a predictable way in accordance with its specification, and never in any other way. Since its specification guarantees process separation and inter-process tamper protection, users can be sure that this will never occur on their kernel.

While formally verified microkernels can be used as traditional kernels, with userspace processes running on top of the kernel, they can also be used as a hypervisor for the device. When used as a hypervisor, the microkernel will run a virtualized environment as a dedicated set of processes, with the virtualized environment likely having its own kernel and userspace. This allows for a more traditional operating system to be run on devices using microkernels in instances where the traditional OS’s functionality is required, but with the added benefit of isolating the environment from other processes on the device (such as other virtual environments or dedicated processes).

Limitations: Only properties that were scoped into the formal OS kernel specification, verification, and/or generator can be guaranteed to be in the resulting OS kernel, and only for the versions of a kernel compiled with specific configuration options and when running on specific hardware configurations. Kernels like seL4 often have a number of optional features and can run on hardware configurations that would invalidate the formal proof. Users will need carefully check the assumptions.

Limitations: While a formally verified kernel would ensure certain properties (such as information flow isolation), these will need to be meaningfully leveraged in the system design in order to provide the desired value. For example, a system design that places all software into a single userspace partition under seL4 would not benefit from seL4’s theoretical capability to isolate partitions. Another design that sets up two partitions but then creates channels allowing the two partitions to communicate in unrestricted fashion, would not fare much better.

Consideration: A strong design would often combine a formally verified microkernel, isolating critical functionality into separate partitions, then making sure the code in those partitions is itself formally verified (see MID-089), or at least implemented using a memory-safe programming language (see MID-005) with cross-partition and external communication channels filtered by formally verified parsers (see MID-088).

IEC 62443 4-2 Mappings

None

References

[1] seL4 Project a Series of LF Projects, LLC. “The seL4 Microkernel.” sel4.systems. Accessed: Mar. 18, 2025. [Online]. Available: https://sel4.systems/

[2] K. Fisher, J. Launchbury, R. Richards. “The HACMS program: Using formal methods to eliminate exploitable bugs.” royalsocietypublishing.org. Accessed: Mar. 18, 2025. Available: https://royalsocietypublishing.org/doi/10.1098/rsta.2015.0401

[3] What is Proved and What is Assumed. sel4.systems. Accessed: Mar. 18, 2025. [Online]. Available: https://sel4.systems/Info/FAQ/proof.html

[4] G. Heiser. “The seL4 Microkernel An Introduction.” sel4.systems. Accessed: Mar. 18, 2025. Available: https://sel4.systems/About/seL4-whitepaper.pdf

[5] M. Doran, N. Kandalaft. “Embedded Virtualization on RISC-V with seL4” ieee.org. Accessed: Mar. 18, 2025. Available: https://ieeexplore.ieee.org/document/10316016/