seL4/CAVEATS.md

Known caveats in the seL4 API and implementation

Implementation Correctness

The following seL4 architectures have platforms with a C-level functional correctness proof. Proof support for further platforms within these architectures is on the roadmap and expected in 2025.

• AArch32: Armv7-a with and without hypervisor extensions, no SMMU, with fast path
  • Platforms (non-hyp): sabre (no FPU), imx8mm-evk (with FPU)
  • Platforms (hyp, no FPU): tk1, exynos5
• AArch64: Armv8-a with hypervisor extensions only, no SMMU, with fast path
  • Platforms: tx2
• RISC-V: 64-bit only, no fast path
  • Platforms: hifive
• x64: without VT-x and VT-d, no fast path
  • Platforms: pc99

This proof covers the functional behaviour of the C code of the kernel. It does not cover machine code, compiler, linker, boot code, cache and TLB management. Compiler and linker can be removed from this list by additionally running the binary verification tool chain for seL4 for AArch32 or RISC-V. The proof shows that the seL4 C code implements the formal abstract API specification of seL4 and is free from standard C implementation defects such as buffer overruns or NULL pointer dereferences.

For AArch32 without hypervisor extensions and without FPU, and for RISC-V, there are additional proofs that this specification satisfies the following high-level security properties:

• integrity (no write without authority),
• confidentiality (no read without authority), and
• intransitive non-interference (isolation, modulo timing channels, between adequately configured user-level components).

The security property proofs depend on additional assumptions on the correct configuration of the system. See the l4v repository on GitHub for more details.

Similar proofs for AArch64 with hypervisor extensions are in progress.

For AArch32, there additionally exist proofs for correct user-level system initialisation. See the l4v repository for details.

Note that seL4 currently performs lazy FPU and VCPU switching, which can introduce information flow timing channels. An API-change proposal (RFC) to improve this behaviour is currently in progress.

Verified Configurations

For the precise configuration of the verified platforms above, see the corresponding files in the seL4 configs/ directory.

The proofs are generally sensitive to changes in configuration parameters, and will break if these are changed. For some parameters, the proofs are explicitly set up to be robust, such as the number of domains NUM_DOMAINS, and the domain schedule. More such parameters are on the roadmap to be added and documented here.

If in doubt, edit the corresponding _verified config files and re-run the proofs as specified in the l4v repository.

Real Time

The default version of seL4 must be configured carefully for use in real-time requirements. It has a small number of potentially long-running kernel operations that are not preemptible (e.g., endpoint deletion, certain scheduling states, frame and CNode initialisation). These can (and must) be avoided by careful system configuration if low latency is required.

MCS

The MCS configuration of the kernel addresses many of these real-time problems and provides principled access control for execution time, but its formal verification is currently still in progress. For RISC-V, design-level proofs have completed, and C-level proofs are in progress. Similar proofs for AArch64 are planned.

The MCS configuration is supported by the seL4 foundation and should generally be stable, with small API changes to be expected while verification is ongoing and the configuration is used in more systems. See open requests for comments (RFCs) for MCS for what is currently being discussed.

Note that the kernel worst-case execution time (WCET) configuration values in the kernel platform definitions are defaults only and need to be determined based on the specific use case -- for instance, static systems can be set up to have low latency and WCET, whereas dynamic systems or systems where untrusted code has authority to perform longer-running kernel operations may need higher values.

SMP

A symmetric multi-processor (SMP) configuration for seL4 exists and is supported by the seL4 foundation, but currently without formal verification. While generally stable, there are a small number of known open issues, in particular when the kernel is compiled with clang. We recommend gcc for working with SMP configurations of seL4.

The combination of SMP and hypervisor extensions is supported and should be generally stable, but like the plain SMP configuration it is not formally verified.

The combination of SMP and MCS is supported and is receiving active development, but it is less explored and less tested. It should still be considered experimental. There are no supported Armv7-a boards for SMP+MCS, only Armv8-a, RISC-V, and Intel. It is tested with gcc on hifive, tqma8xqp1gb, odroidc4, zynqmp, tx1, tx2, pc99-32, and pc99-64.

The combination of SMP, MCS, and hypervisor extensions is currently supported on AArch64 only. It is less tested with lower code coverage; currently with gcc only, on odroidc4, tx1, and tx2.

The combination of SMP and domain scheduler is not supported. The SMP configuration is not expected to satisfy strong intransitive non-interference for information flow.

See the seL4 issue tracker and the sel4test issue tracker for details using the labels MCS and SMP for finding issues on these configurations.

As these are unverified configurations, standard C implementation defects are possible and not excluded as in verified seL4 configurations.

Supporting a static multi-kernel configuration with formal verification is on the roadmap for the AArch64 architecture, with initial work begun. We expect multi-kernel configurations to be more robust than SMP configurations, because they are simpler and closer to the current sequential seL4 proofs.

In a multi-kernel configuration, each CPU core runs a separate instance of seL4, with each kernel instance getting access to disjoint subsets of memory of the machine. User-level memory can be shared as device-untyped memory, which the kernel manages but does not access. These configurations can already be set up without kernel changes by providing suitable device tree overlays to each kernel instance. Further work is planned to make such configurations easier to use and more robust against unsafe use/configurations, e.g. by managing IRQ controller access for each instance.

Re-using Address Spaces

Before an ASID/page directory/page table can be reused, all frame caps installed in it should be revoked. The kernel will not do this automatically for the user.

If, for instance, page cap c is installed in the address space denoted by a page directory under ASID A, and the page directory is subsequently revoked or deleted, and then a new page directory is installed under that same ASID A, the page cap c will still retain some authority in the new page directory, even though the user intention might be to run the new page directory under a new security context. The authority retained is to perform the unmap operation on the page the cap c refers to, as well as cache maintenance operations on the architectures that support these.

Intel VT-d (I/O MMU) support

Intel VT-d support in seL4 was tested for the following chipsets:

• Intel Q35 Express
• Intel 5500

On other chipsets with Intel VT-d support, seL4 might:

• complain and disable IOMMU support
• hang during bootstrapping
• have some weird behaviour during runtime

In any of these cases, the workaround is to disable VT-d support, either:

• in the BIOS, or
• by including disable_iommu into the MultiBoot (e.g. GRUB) command line as described in the seL4 documentation