seL4 Version 13.0.0 Release

2024-07-01

Announcing the release of seL4 13.0.0. This release has security-relevant fixes that affect
configurations or areas of the kernel that have not been formally verified. It is recommended
to upgrade.

This is a breaking release.

Security-relevant Changes

Fixed a kernel-crashing NULL pointer dereference when injecting an IRQ for a non-associated VCPU on SMP
configurations. This can be triggered from user-level by any thread that has access to or can create non-associated
VCPU objects. While HYP+SMP is not a verified configuration and is not thoroughly tested, it is generally assumed to
be working. If you are using this configuration, it is strongly recommended to upgrade.
- Affected configurations: only unverified HYP+SMP configurations on Arm platforms are affected.
- Affected versions: seL4 versions 12.0.0 and 12.1.0.
- Exploitability: Any thread that can create or that has access to an unassociated VCPU can cause the crash. In static
  systems, only the system initialiser thread can create VCPUs and the standard capDL system initialiser will not
  trigger the issue. VMMs could have the authority to dissociate an existing VCPU from a TCB if they have both
  capabilities. That is, a malicious VMM could cause a crash, but generally VMMs are trusted, albeit not verified
  code. Guest VMs generally do not have sufficient authority to exploit this vulnerability.
- Severity: Critical. This crashes the entire system.
Fixed a kernel-crashing cache maintenance operation on AArch64 (Armv8). On AArch64, when seL4 runs in EL1 the kernel
would fault with a data abort in seL4_ARM_Page_Invalidate_Data and seL4_ARM_VSpace_Invalidate_Data when the user
requested a dc ivac cache maintenance operation on a page that is not mapped writeable. If you are using seL4 in EL1
on AArch64, it is strongly recommended to upgrade.
- Affected configurations: unverified AArch64 configurations of seL4 with hypervisor extensions off (kernel runs in
  EL1). AArch32 configurations and configurations where seL4 runs in EL2 are not affected.
- Affected versions: all previous versions since 5.0.0
- Exploitability: Any thread that has a VSpace capability or page capability to a page that is not mapped writable can
  cause the data abort. Most Microkit and CAmkES systems do not give their component access to these capabilities, but any component with Untyped capabilities could create threads with enough capabilities to trigger the issue.
- Severity: Critical. This crashes the system.
Fixed a cache issue on Arm where cleared memory was not flushed to RAM, but only to the point of unification. This
means that uncached access was able to still see old memory content.
- Affected configurations: Arm platforms that distinguish flushing to PoU from flushing to RAM
- Affected versions: all previous versions since 4.0.0
- Exploitability: Low. The issue is trivially observable by mapping the same frame as cached and uncached.
  However, it is unlikely to be exploitable in a real system, because re-using memory over security boundaries
  is already excluded, so information leakage happens only within the same domain.
- Severity: Medium. It breaks functional correctness in the sense that a cleared frame may not yet be cleared when
  viewed as uncached. It does not break any functional kernel behaviour.

Platforms

Added support for the ARM Cortex A55
Added support for the imx8mp-evk platform
Added support for additional RPI4 variants
Added support for the Odroid C4
Added support for the Avnet MaaXBoard
Added support for arm_hyp on qemu-arm-virt platfrom with cortex-a15 CPU
Added support for qemu-riscv-virt
Added support for the Pine64 Star64
Added support for the TQMa8XQP 1GiB module
Remove imx31/kzm platform support. This platform is being removed as it is sufficiently old and unused.
Remove ARM1136JF_S and ARMv6 support. This architecture version is being removed as it is sufficiently old and
unused. See RFC-8.
Remove ARMv6 specific configs: KernelGlobalsFrame and KernelDangerousCodeInjectionOnUndefInstr. This removes the
constant seL4_GlobalsFrame from libsel4 as well as the IPC buffer in GlobalsFrame caveat from CAVEATS.md
rpi3+rpi4: Mark first memory page as reserved

Arm

Enabled access to seL4_VCPUReg_VMPIDR and seL4_VCPUReg_VMPIDR_EL2 for all hypervisor configurations. Previously
this register was only accessible for SMP kernel configurations. Non-SMP configurations can still require access when
wanting to control the value of MPIDR that the guest reads. Note that the initial value for new seL4_ARM_VCPUs for
this register is 0 which isn't a legal value for MPIDR_EL1 on AArch64. It may be necessary for the register to be
explicitly initialized by user level before launching a thread associated with the new seL4_ARM_VCPU.
Allow changing the VCPU of active thread: call vcpu_switch in associateVCPUTCB. This guarantees that the correct
VCPU will be activated when the kernel finishes execution. Previously, changing the VCPU of the current thread would
result in no VCPU being active.
benchmarking: use write-through kernel log buffer
arm_hyp: Access SPSR via non-banked instructions
generic_timer: force timer to de-assert IRQ.
No special handling for edge-triggered IRQs.
- Clearing the pending state only has an effect if the IRQ state is active-and-pending, which happens for
  edge-triggered interrupts if another edge happens on the IRQ line for the currently active interrupt. This window is
  small enough to ignore, at worst user space will get another notification, which is harmless.
If unnecessary notifications are unwanted, the pending state should be cleared during seL4_IRQHandler_Ack(), as
that covers a much bigger window. However, edge-triggered interrupts are not expected to happen often. Making all
interrupt handling slightly faster and the code simpler is the better trade-off.
Make write-only mapping message consistent. There is a warning when creating a write-only mapping on AArch32/AArch64.
This message is now the same in all variants.

AArch32

Implement KernelArmExportPTMRUser and KernelArmExportVTMRUser options for Arm generic timer use access on AArch32.
AArch32 VM fault messages now deliver original (untranslated) faulting IP in a hypervisor context, matching
AArch64 behaviour.
Fix single stepping on ARMv7
TLB: only perform TLB lockdown for Cortex A8.
- The code previously used the same instructions for Cortex A8 and A9, but the Cortex A8 instructions are undocumented
  for A9, and A9 provides a slightly different TLB interface. As far as we can tell, the instructions were simply
  ignored by the supported A8 platforms, so there was no current correctness issue. Since the instructions had no
  effect, we removed A9 TLB lockdown support. This potential issue was discovered and reported by the UK's National
  Cyber Security Centre (NCSC).
TLB: guard TLB lockdown count.
- lockTLBEntry uses the global tlbLockCount as input without checking bounds. This is fine, because the function
  is called at most 2 times per core, but this is only apparent when checking the entire possible calling context.
  Make this bound obvious locally by doing nothing if the function is called with values of tlbLockCount of 2 or
  greater. This is safe, because TLB lockdown is a performance change only. Also add an assert for debug mode, because
  we want to know if calling context ever changes. This potential issue was reported by The UK's National Cyber
  Security Centre (NCSC).

AArch64

Add AARCH64_verified.cmake config for functional correctness on AArch64
Rename libsel4 config option AARCH64_VSPACE_S2_START_L1 to CONFIG_AARCH64_VSPACE_S2_START_L1 to be namespace
compliant.
Added SMC Capability (smc_cap) and SMC forwarding for AArch64 platforms. See
RFC-9.
Remove VSpace object types in AArch64: seL4_ARM_PageDirectory and seL4_ARM_PageUpperDirectory. See also the
corresponding RFC. The functionality
previously provided by these types will be provided by the existing seL4_ARM_PageTable object type. This allows for
a simpler API and enables a smaller kernel implementation that will be easier to verify. libsel4 provides a source
compatibility translation that maps the old libsel4 names and constants the new ones in
<sel4/sel4_arch/deprecated.h>. There are some exceptional cases where kernel behavior has changed:
- A Page directory and page table are now the same kind of object and can be mapped at any page table level.
  If the lookup for the provided address stops at a slot that can map a page directory, it will map the object as a
  page directory. If there already is a page directory mapped, the lookup will proceed to the next level and it will
  map as a page table instead of returning an error.
Removed user address space reserved slots restriction on 40bit PA platforms when KernelArmHypervisorSupport is set.
This change is reflected in the definition of the seL4_UserTop constant that holds the largest user virtual address.
Added support for GICv3 virtualization, tested on iMX8QXP
Implemented a signal fastpath on AArch64. Must be enabled explicitly with the KernelSignalFastpath config option.
Implemented a virtual memory fault fastpath on AArch64. Must be enabled explicitly with the KernelExceptionFastpath config option.
Add option KernelAArch64UserCacheEnable for user cache ...