seL4/seL4: seL4 13.0.0

Abstract

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 . 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 maintenance. Enables user level access to DC CVAU, DC CIVAC, DC CVAC, and IC IVAU which are cache maintenance operations for the data caches and instruction caches underlying Normal memory and also access to the read-only cache-type register CTR_EL0 that provides cache type information. The ArmV8-A architecture allows access from EL0 as fast cache maintenance operations improves DMA performance in user-level device drivers. These instructions are a subset of the available cache maintenance instructions as they can only address lines by virtual address (VA). They also require that the VA provided refers to a valid mapping with a