When we back out of the lock via IPI stall in ipiStallCoreCallback(),
the FaultIP/NextIP are not updated yet and the lock exit code will set
the wrong program counter.
Moving the FaultIP/NextIP before the lock makes sure that all exit
paths will restore to the correct program counter.
Even though this write happens outside the lock, it does not introduce
a race. The only possible interference would be a TCBWriteRegisters
syscall from another core along the lines of the following: other core
enters syscall, current core gets to lock, makes FaultIP adjustment,
other core exists syscall, current core overwrites effect. This path is
not possible, because the TCBWriteRegisters call on the other core
first leads to a stall on this core before it proceeds, which
means this core will be on idle and cannot attempt to enter the lock.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
extra_bi_size and extra_bi_offset should always be same at
this point, so the condition is never true. This commit removes
the scope and adds an assersion instead.
Signed-off-by: Terry Bai <tianyi.bai@unsw.edu.au>
'extra_bi_size' is meant to report the full size of all the bootinfo
blocks, but excluded the body size of trailing padding block in the
original implementation. Plus the padding is not necessary to exist.
Therefore, this fix removes the trailing padding block and initialises
`extra_bi_size` to 0 to make boot info consistent across architectures.
Signed-off-by: Terry Bai <tianyi.bai@unsw.edu.au>
This value was inconsistent across platforms, and one
should use seL4_UserVSpaceTop instead.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
This is a consistent, inclusive-top value that is conveying
similar information to that of seL4_UserTop. We are adding
this so as to not break existing userspace, but it will make
it easier for userspace to deal with other platforms.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Restore the schedule queue check of commit c64867e from PR #352,
which was accidentally undone when adding a similar check for the
release queue in PR #1486.
Resolves issue #1645.
Signed-off-by: Indan Zupancic <indan@nul.nu>
The check for both label and condition is there to handle cases like:
enum invocation_label {
Invalid,
#if A
LabelOne,
#endif
#if B
LabelOne,
#endif
}
Co-authored-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Currently causes compile errors. It should match seL4_DebugCapIdentify,
except return affinity instead of cap type.
Signed-off-by: Indan Zupancic <indan@nul.nu>
This is useful for sel4test et al for testing that a certain
PD has been succesfully migrated between cores, or that it
is running on a particular core.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
The actual libsel4 wrappers and kernel code only ever exists
when CONFIG_ENABLE_SMP_SUPPORT exists, so there's no point
also defining the syscall code as well.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
The struct types for the MADT entries have alignment requirements set by
the compiler. But since these entries are tightly packed by the BIOS,
entry `n-1` can cause entry `n` to be unaligned. So if you compile the
kernel with LLVM and UBSAN on, the kernel can crash depending on how
your BIOS packed the MADT.
This commit updated the code so that for each entry the kernel copies
it into a stack allocated buffer to respect the compiler alignment
requirements.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Previously the kernel trusted the ACPI MADT entries length provided by
the BIOS. This commit added checks to make sure that they are correct
before any parsing steps happen.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Set the default for KernelArmVtimerUpdateVOffset to OFF. This is the
setting supported in verification builds, and it is also the setting
used in most projects.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Use the new build matrix from ci-action that supports build subgroups
for armv8a. This should speed up the hw-build from >50min to about
12:30min, now bounded by the riscv group, not armv8a.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
By splitting the u32 into 2x u16 we lower the alignment requirements
of the compiler. So now sizeof(acpi_madt_iso_t) is equal to the true
size.
Fixes an early boot triple fault caused by UBSAN alignment checks during
MADT parsing.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
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>
