Avoid warning about empty string arguments to functions config_option()
and config_string() in newer cmake versions.
Both behaviour versions (with and without policy) are safe for how we
are using those arguments. Setting the policy when it exists removes the
warning.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
To ease verification, in the SysReplyRecv case of handleSyscall, add
the explicit check for preemption, even though the call to
handleInvocation should not be preemptible.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Make the function validFaultHandler available to the assert in
sendFaultIPC in faulthandler.c.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Set missing cap fault info (lookup_fault_missing_capability_new(0)) in
lookupReply and move handleFault to caller, so that lookupReply is an
actual lookup function without random side effects.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Update the tcbLookupFailure field to be the current lookup fault, if
there is a current cap fault.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
The inline assembly blocks for vmlaunch and vmresume in the 32-bit
restore_vmx() function manually pop guest state into all general-purpose
registers.
Previously, these registers were not included in the inline assembly
clobber list. If a VM entry fails, execution falls through to the
vmlaunch_failed() C function. Because the compiler is unaware that the
registers were overwritten, it may generate code for the failure handler
that relies on destroyed state.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Previously, the assembly block in restore_vmx() passed a few C
variables as generic register inputs ("r"):
```
: [reg]"r"(&vcpu->gp_registers[VCPU_EAX]),
[launched]"r"(&vcpu->launched),
...
[guest_msr]"r"(&vcpu->guest_msr_registers[VCPU_GS]),
[host_msr]"r"(&vcpu->host_msr_registers[n_vcpu_msr_register])
```
This allowed the compiler to place them in any general-purpose register.
GCC happened to allocate them in a non-conflicting order with respect to
how CPU registers used in the assembly block. But on LLVM 22.1.5, it
assigned them to the exact registers the assembly block was manually
writing to via movq.
This caused the pointers to be overwritten before use, leading to a
guest hang when the registers were restored with garbage values by
a kernel built with LLVM.
I've updated the code to refer to the variables by name rather than by
registers to fix the problem.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
User context already has a kernelSP, which is used.
Also, the 64-bit also doesn't has this, so probably a leftover.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Node 20 is deprecated. Bump GitHub action dependencies to versions that
run on more recent node.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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>
