Changes Arch_finaliseCap and Mode_finaliseCap to return the same finaliseCap_ret_t type
as finaliseCap. This allows the Arch and Mode specific functions to define cleanup
information of its capabilities if necessary, just like the generic capabilities can
in finaliseCap.
Moves the explicit call of `deletedIRQHandler` in `emptySlot` into a new
`postCapDeleted` function that is a generic function to call after a capability
has been deleted.
Currently `deletedCap` only implementes the IRQ case.
Changes finaliseCap to return a generic definition of cleanup information that
needs to be done, instead of just encoding an IRQ number. The post deletion information
is encoded as a `cap_t` due to the capability type already being a union of all
the possible information. Aside from providing a properly generic mechanism the motivation
is to support a similar cleanup phase for I/O ports in the future.
Provides the ability to enable the IBRS hardware Spectre mitigation strategies, as well
as completes the software mitigation by disabling jump tables in compilation. The
hardware mitigations are largely provided "for completeness" in the hopes that they
eventually become less expensive. For the moment there is no reason to turn on any
beyond STIBP if running in multicore
(1) Use NODE_STATE() to access per-core kernel data.
(2) Allocate kernel stack in src/arch/arm/64/head.S.
(3) Use the TPIDR_EL1 to contain the kernel stack pointer
as well as the logical core ID. The kernel stack must
be 4-KiB aligned, and the lowest 12 bits of TPIDR_EL1
are for the logical core ID.
(4) Define the LD_EX, ST_EX, and OP_WIDTH as "ldxr", "stxr",
and "w".
(5) Add irq_remote_call_ipi and irq_reschedule_ipi
Prevents the kernel from writing to read only memory. This shouldn't happen, but catching
such attempts aids debugging and costs nothing to have neabled.
Introduces a kernel option that, when enabled, reduces the kernel window in a user address
space to just be Static Kernel Image and Microstate (SKIM), instead of the full kernel
address space. This isolates the important kernel data from the user preventing a
Meltdown style attack being able to violate secrecy. The kernel text and read only data,
i.e. anything that is static from boot, is not secret and can be allowed in the SKIM window
and potentially read by the user. Additionally to switch to and from the actual kernel
address space a small amount of state needs to also be in the SKIM window.
This is only an implementation for x86-64, although the same design is applicable to ia32
This performs a double address space switch to invalidate an ASID using a single hand
written asm block instead of setCurrentCR3. The purpose of this is to ensure that the
only requirements on the temporary address space that we switch to is that the kernel
code is still mapped in at the same location. As we ensure our old cr3 value is in
register we can ensure, unlike with calling getCurrentCR3 that no stack or other
temporary memory is required.
Introduces a separate definition for vspace root that the kernel runs on. Having this
be distinct from the global vspace root allows for potential future distinction
between the global root (that is copied into all user address spaces) and the address
space that the kernel runs in.
Currently the kernel address space and paging structures are used as the global ones.
This commit renames the paging structures from Global to Kernel to reflect this and
allows for separate global structures to be introduced in the future.
When PCIDs are not enabled the low 12 bits of CR3 are not all ignored as bits 3 and 4 control
memory typing of the translation. To prevent setting these to 'random' values we should leave
the low bits of CR3 0 when not using PCIDs.
A new makeCR3 wrapper is defined that is used instead of cr3_new that, based on CONFIG_SUPPORT_PCID,
either fills in the PCID or 0 as required.
This introduces functions for specifically manipulating the user vspace root, either as an
abstract root or the specific CR3 value, in a way that is separated from the current vspace
root. Currently they are one and the same, but this separation allows for having the kernel
translation (and hence the active vspace root) be different the currently active user.
node_info is a per-core data structure and should have always been padded and aligned to
a cache line to ensure there is no false sharing of cache lines
Global state in this context is state/datastructures that need to be available at all times,
both in user and kernel mode, by the hardware for correct operation. The purpose of creating
a separate per-node structure for it is so that there is the option of treating it specially
in the future from other per node state
The IRQ stack represents state that needs to be available in all contexts, both when user
code is running and when kernel code is running. Separating its definition from all the
other mode state provides the option in the future for treating it differently.
Provides an option that, on kernel init, enables user reading of the performance
monitoring counters. This is a step towards removing the dependence on
seL4_DebugRun for user level benchmarking/profiling
The UL_CONST macro provides a way to declare a constant that may or may not have a UL
suffix. In the case of assembly the UL suffix will be an error to many assemblers and
is not needed.
This defines a CURRENT_CPU_INDEX() macro that resolves to a constant 0 in the absence of
SMP, or a call to getCurrentCPUIndex in the presence of SMP. This provides a way to use
per-core data structures, without additional guards, in a way that is nearly invisible
to verification
Restricting virtual addresses to essentially be only addresses without bit 47 set
allows us to not need to check that an address passed in by the user is canonical
or not. Any address that is in danger of not being canonical (has bit 47 set but
not bits 48 to 63) will all by higher than USER_TOP and will not be permitted.
In f6d367e8df virtual addresses were changed from 48
bits to 49 bits, but this does not seem necessary and the commit does not have enough
detail to justify the change. As such it is being changed back to 48 bits in this
commit, which is far less confusing and results on the bitfield generated functions
switching on bit 47 to determine sign extension (instead of bit 48), which matches
what the hardware description says should be done.
- for arm generic timer platforms, we remove resetTimer ->
resetGenericTimer indirection and simply include generic_timer.h
- this reduces boiler plate for platforms that share timer drivers, as
they simply include the one header
- there is far more timer code in the RT kernel, which motivates this
change