Missed from https://github.com/seL4/seL4/pull/1641.
I think the issue is that x86-64 is not built with VT-X
in any of the CI runs, so we should fix that.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
The IPC queue changes for MCS in commit 771c9e43ce has decreased the
TCB size slightly, which brings TCB_SIZE_BITS down for config
combinations that have MCS + SMP + HYP + benchmarking enabled.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Apply the changes from commit 771c9e43ce to the signal fast path,
which was missed there.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- Introduce functions to append and dequeue to/from endpoint and
notification queues, in order to make verification feasible. Handle
linked list manipulations with the same functions that were
previously used for the ready and release queues, together with a new
function that allows for a new item to be inserted into the queue
after another item that is already in the queue.
- Remove tcbEPNext and tcbEPPrev pointers from the MCS version, and
instead use tcbSchedNext and tcbSchedPrev pointers, given that no
thread can be simultaneously in any two of the endpoint,
notification, ready, or release queues.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
The original `restore_vmx()` inline assembly passes the vmlaunch_failed
function pointer as a standard register constraint ("r"). Consequently,
the compiler allocates this pointer to a general-purpose register before
the assembly block begins.
However, immediately prior to executing vmlaunch or vmresume, the kernel
restores the guest's state via a sequence of popq instructions that
overwrite every general-purpose register. If the VM entry fails (e.g.,
due to an invalid VMCS state), execution falls through to the failure
path, which then attempts to jump to the register originally holding the
function pointer.
Because this register was just overwritten with guest-controlled data,
the kernel will jump to an arbitrary memory address dictated by the
guest. A malicious guest OS can exploit this by placing a payload
address in the targeted register and intentionally corrupting its VMCS
state (e.g. by compromising the userspace VMM) to force an entry
failure, achieving full VM escape and arbitrary code execution in the
kernel.
This patch fixes the vulnerability by using a RIP-relative `lea`
instruction to calculate the handler's address dynamically at the exact
moment of failure, entirely bypassing the clobbered registers.
I've managed to trigger this bug by compiling the kernel with LLVM. On
a VM Entry fail, the kernel would just crash because it jumped to a
random location. But after the fix, it no longer crashes and was able to
print out the error message in `vmlaunch_failed()`.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
When a notification is bound to an IRQ that arrives on a different
core than where the VCPU is running, x86 uses a special IPI to
notify the other core about this. (For performance reasons you
would try to avoid this setup. Nevertheless, it should work.)
When an IpiRemoteCall_VMCheckBoundNotification arrives during a
VM exit, the notification reply set by VMCheckBoundNotification()
gets overwritten by the handleVmexit() reply, leading to lost
notification events. This happens when VMCheckBoundNotification()
gets called by the IPI handling code within NODE_LOCK_SYS.
As there is no way to postpone the VM exit handling and the IPI
code doesn't know whether it races with a VM exit, doing nothing
if the current task is the target is the safest choice:
Either the IPI itself caused a VM exit, or there was a VM exit
happening already.
To handle the first case, explicitly call VMCheckBoundNotification()
in handleVmexit(). This must be done while holding the kernel lock,
as the other core can release the lock any moment after it received
our IPI reply.
In the latter case, pending notifications will be detected and
returned to user space by the next seL4_VMEnter() call.
Fix tested by Alessandro Legnani.
Resolves issue #1148.
Signed-off-by: Indan Zupancic <indan@nul.nu>
The System V AMD64 ABI requires the stack pointer (%rsp) to be 16-byte
aligned immediately before a `call` instruction. In `kernel_exception`,
pushing three 8-byte control registers (%cr2, %cr3, %cr4) after
`INT_SAVE_STATE` misaligned the stack prior to calling
`handleKernelException`.
This commit adds an 8-byte padding before pushing the control registers
to maintain 16-byte alignment.
Previously, compiling the kernel with LLVM and UBSAN enabled resulted in
a recursive exception loop if a UB was encountered elsewhere in kernel
code. The misaligned stack would trigger UBSAN during exception
printing, causing an exception within the exception handler that
looped infinitely.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
This drops subsection for riscv so that subsections for rv32/64
belong to same level as those of x86 and arm32/64.
Signed-off-by: Yanfeng Liu <yfliu2008@qq.com>
Currently, the kernel permits userspace VMMs to enable and use the
VMX-preemption timer by allowing writes to the following VMCS fields:
- VMX_GUEST_PREEMPTION_TIMER_VALUE (count)
- VMX_CONTROL_PIN_EXECUTION_CONTROLS (timer enable bit)
- VMX_CONTROL_EXIT_CONTROLS (save current count on context switch bit)
It also forwards the timer expiry event as a VM exit.
But it does not tell userspace how fast the timer will count down,
making it impossible to use. This commit exposes the timer's scale
via `seL4_X86_VCPU_ReadMSR`.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
- separate the update of the release queue in tcbReleaseEnqueue from
the setting of ksReprogramTimer, so that verification may reason
uniformly abbout the update of the queue.
- use local variables in sendIPC and receiveIPC to avoid repeated
accesses of the heap.
- move the update of the replyTCB field in receiveIPC so that the
updates related to the thread state are grouped together, to more
closely align with the Haskell specification.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
a7 is not changed by seL4_Yield, so the original declaration is correct.
However, in some loops GCC 14.2 may drop the load to a7 if a7 or
memory are not declared as clobbered in the assembly block. This is a
problem if *other* code does write to a7. For some reason GCC 14.2 does
not recognise those other loads. GCC 14.3 and GCC 15 both work as
expected.
The problem manifests in SCHED0011 in sel4test.
This change works around the GCC 14.2 problem because GCC 14.2 is the
standard Debian trixie compiler and it is likely that people will hit
the problem even if we say that GCC 14.2 should not be used.
The workaround uses the same implementation of seL4_Yield as the Arm and
x86/x64 versions do: inline call to sys_null with an empty asm volatile
declaring memory as clobbered. The memory clobber declaration eliminates
the miscompilation, and overall the implementations are now consistent.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
When we renamed CHANGES to CHANGES.md, the copyright info from
reuse/dep5 for CHANGES was not transferred.
Remove CHANGES from .reuse/dep5 and add info to CHANGES.md directly.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Fixed incorrect arguments descriptions for X86PageMapEPT, to make it
consistent with other invocations that take an EPT and guest physical
address such as X86EPTPTMap.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
The call to setThreadState within suspend is
moved to the end of the function, in order to
preserve invariants about the queues.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Previously TCB_WriteRegisters/ReadRegisters ignored the count parameter
and unconditionally copied the entire seL4_UserContext, this leads to
unnecessary overhead for VMM operations.
This addresses issue #1085
Signed-off-by: Yifei Zhan <yifei@zhan.science>
For preprocess checks on pull requests, check against the base_ref of
the pull request (e.g. master) instead of against the seL4 revision in
the verification manifest.
If base_ref has advanced over the verification manifest revision, we do
not want to see that difference again on pull requests, but only the
difference the pull request causes itself.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The call to rescheduleRequired within scheduleTCB is performed only when
the scheduler action is ResumeCurrentThread, and therefore will only set
the scheduler action to ChooseNewThread. This removes the call to
rescheduleRequired and replaces it with the direct update to the
scheduler action.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The upstream action in the ci-actions repository has changed slightly
and leaves the PDF in a different location.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Make verification and release builds equal by setting the default for
KernelArmHypEnableVCPUCP14SaveAndRestore to OFF. The option is still
available to set in non-verification builds, only the default changes.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add GIC_VERSION cmake option (default 2) to select between GICv2 and
GICv3 for the qemu-arm-virt platform. GICv3 support requires waking
the redistributor on QEMU and configuring interrupt security grouping
for the hypervisor.
Resolves: seL4/seL4#1170
Signed-off-by: Kent McLeod <kent@kry10.com>
Allow userspace reads to `VMX_CONTROL_SECONDARY_PROCESSOR_CONTROLS`
field of VMCS. seL4 already allow writes to the field so no reason to
not allow reads.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Previously, X86_64_VTX_64BIT_GUESTS forced the VCPU into 64-bit mode by
hardcoding the IA-32e bit in VM-Entry Controls. This prevented userspace
from starting a VCPU in real mode, which break cases where you want the
guest to be able to manage its own mode transitions. Such as booting
an UEFI firmware.
This change allows the guest to manage its own mode transitions
(real -> protected -> long mode). The X86_64_VTX_64BIT_GUESTS config is
now scoped strictly to enabling 64-bit features like MSR access.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Allow userspace reads and writes to `VMX_CONTROL_ENTRY_CONTROLS` field
of VMCS. Which is primarily used for enabling long mode and loading of
certain MSRs on VM Entry. As far as I know this field only controls the
behaviour of the VCPU and would not allow userspace to violate any
kernel properties such as disabling external interrupt exiting or EPT.
The effects of bits in this field are defined in
Chapter 27.8 "VM-ENTRY CONTROL FIELDS" of the
Intel SDM Order Number: 325462-090US February 2026.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Allow CR0.PE and CR0.PG to be cleared if "Unrestricted Guest" mode is
supported by the host CPU. This mode allows guest software to run in
unpaged protected mode or in real-address mode. From [1] with Indan's
feedback applied.
[1] https://github.com/seL4/seL4/pull/1438
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Co-authored-by: Heyang Zhou <hello@su3.io>
When original.family >= 0xF, the extended model was incorrectly
assigned to ci->display.family instead of ci->display.model. This
matches the Intel implementation and AMD CPUID specification.
Signed-off-by: Weixie Cui <cuiweixie@gmail.com>
Made-with: Cursor
Previously, CMake defaults to adding various flags to the compile
options, such as `-O3`, `-DNDEBUG`, and `-g`. Here is an excerpt from
CMakeCache.txt:
//Flags used by the C compiler during RELEASE builds.
CMAKE_C_FLAGS_RELEASE:STRING=-O3 -DNDEBUG
//Flags used by the C compiler during RELWITHDEBINFO builds.
CMAKE_C_FLAGS_RELWITHDEBINFO:STRING=-O2 -g -DNDEBUG
We instead change the CMAKE_BUILD_TYPE to 'None' so that CMake
doesn't try to be clever and append extra compile flags. Anything
that depends on seL4 will be unaffected as CMake variables are scoped.
This should have no meaningful change to the kernel's generated code,
as the compile flags were being overridden anyway.
Relevant parts of the build.ninja file for comparison:
- Now, `-DRELEASE=ON`:
FLAGS = -march=armv8-a -D__KERNEL_64__ -std=c99 -Wall -Werror
-Wstrict-prototypes -Wmissing-prototypes -Wnested-externs
-Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull
-nostdinc -ffreestanding -fno-stack-protector
-fno-asynchronous-unwind-tables -fno-common -O2 -nostdlib
-fno-pic -fno-pie -mgeneral-regs-only -mno-outline-atomics
-E -CC -I/sel4test-manifest/build/kernel/generated_prune
- Before, `-DRELEASE=ON`:
FLAGS = -march=armv8-a -D__KERNEL_64__ -O3 -DNDEBUG -std=c99 -Wall
-Werror -Wstrict-prototypes -Wmissing-prototypes
-Wnested-externs -Wmissing-declarations -Wundef
-Wpointer-arith -Wno-nonnull -nostdinc -ffreestanding
-fno-stack-protector -fno-asynchronous-unwind-tables
-fno-common -O2 -nostdlib -fno-pic -fno-pie
-mgeneral-regs-only -mno-outline-atomics -E -CC
-I/sel4test-manifest/build/kernel/generated_prune
Note the lack of -O3 -DNDEBUG options.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
This was done way back in 2017: 0abc72027, but somehow
was missed from CMakeLists.txt and hyp_traps.S files.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Only call the command on CMake files that may be the first file
evaluated from the project. Remove from all other files.
Signed-off-by: Kent McLeod <kent@kry10.com>
The AArch64 FPU trap helpers were modifying both CPTR_EL2.TFP and
CPTR_EL2.TCPAC when enabling or disabling FPU trapping. However, only
TFP controls trapping of FP/SIMD instructions from EL0/EL1 to EL2.
TCPAC traps accesses to CPACR_EL1 and is unrelated to FPU instruction
execution. Trapping CPACR_EL1 is unnecessary for seL4’s FPU handling
and can interfere with other architectural features that are
controlled via CPACR_EL1.
In particular, CPACR_EL1 is an Architectural Feature Access Control
Register and is not limited to FP/SIMD. For example, Morello uses
CPACR_EL1.CEN to enable CHERI instructions. Trapping CPACR_EL1 via
TCPAC would therefore require special handling or could break guests
that legitimately modify CPACR_EL1 for non-FPU features.
Since seL4 only needs to trap FP/SIMD instructions if FPU is disabled
per TCB/VM, it is sufficient to control CPTR_EL2.TFP alone. Remove the
modification of TCPAC from enableTrapFpu()/disableTrapFpu() and leave
CPACR_EL1 accesses untrapped.
This aligns the implementation with the architectural intent of the
AArch64 FP/SIMD trapping model and avoids assuming that CPACR_EL1 is
used solely for FPU control.
See Issue #1601 for more context and discussion.
Signed-off-by: Hesham Almatary <hesham.almatary@cl.cam.ac.uk>
This eases verification by using a local variable
which remains unchanged during execution of the
function.
This preserves semantics since refill_unblock_check
will not modify the tcbSchedContext field of any TCB.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
At the moment, the seL4 microkit does not setup TLS variable
support. The workaround has been to `#define __thread` (blank)
before including `<sel4/sel4.h>` in `<microkit.h>`, which causes
issues if `<microkit.h>` is included *after* `<sel4/sel4.h>`,
often with obscure linker errors to `__emutls_**` symbols.
Instead we add a libsel4 config option that allows us to build
it with __thread copied out. We introduce an LIBSEL4_THREAD_LOCAL
macro in a similar way to the existing LIBSEL4_INLINE macro.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
