This is useful for all x86 IOMMU work, which otherwise has
to duplicate the definitions of VTD_PT_INDEX_BITS in userspace
code. Follow the same pattern as many other existing code in
the libsel4 headers where the kernel depends on it.
Note we can't define seL4_IOPageTableBits in terms of Index + Entry
because the capDL tool does the c-preprocessor to make a YAML file
containing the constant, and it won't do evaluation.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Previously, this would just print a 'halting via unknown'
in debug mode when an SError occurred and SError ignore was
not turned on. This changes the trap code so that we print
out the known cause of the trap.
KERNEL INVALID VECTOR ENTRY!
Vector: 0x580 (SError 64-bit EL0/EL1)
Fault attributed to program counter: 0x221dc0
ESR: 0xbf000000 FAR: 0x2881c98000824100
halting...
Kernel entry via Unknown (0)
This was encountered after some rust-seL4 changes to the
initialiser for Microkit related to untyped mappings broke
boot: https://github.com/seL4/microkit/issues/541
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
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>
