seL4 Configurations

When enabled this configuration option prevents the usage of any other options that would compromise the verification story of the kernel. Enabling this option does NOT imply you are using a verified kernel.

Enable MCS feature for seL4.

Root CNode Size (2^n slots) The acceptable range is 12-27 and 12-26, for 32-bit and 64-bit respectively. The root CNode needs at least enough space to contain up to BI_CAP_DYN_START.

Maximum number of objects that can be created in a single Retype() invocation.

Max number of untyped capabilities given to initial boot thread. Additional caps won’t be handed to the system.

Kernel timer tick period in milliseconds.

Number of kernel timer ticks until a thread is preempted.

Budget of booth thread: Number of milliseconds until the boot thread is preempted.

Maximum number of work units (delete/revoke iterations) until the kernel checks for pending interrupts (and preempts the currently running syscall if interrupts are pending).

Maximum size in bits of chunks of memory to zero before checking a preemption point.

The number of scheduler domains in the system

A C file providing the symbols ksDomSchedule and ksDomeScheudleLength to be linked with the kernel as a scheduling configuration.

The number of priority levels per domain.

Multiplier to scale kernel WCET estimate by: the kernel WCET estimate is used to ensure a thread has enough budget to get in and out of the kernel. When running in a simulator the WCET estimate, which is tuned for hardware, may not be sufficient. This option provides a hacky knob that can be fiddled with when running inside a simulator.

Enable debug facilities (symbols and assertions) in the kernel

Builds the kernel with support for a userspace debug API, which can allows userspace processes to set breakpoints, watchpoints and to single-step through thread execution.

Allow the kernel to print out messages to the serial console during bootup and execution.

seL4 does not properly check for and handle spurious interrupts. This can result in unnecessary output from the kernel during debug builds. If you are CERTAIN these messages are benign then use this config to turn them off.

In debug mode, seL4 prints diagnostic messages to its serial output describing, e.g., the cause of system call errors. This setting determines whether ANSI escape codes are applied to colour code these error messages. You may wish to disable this setting if your serial output is redirected to a file or pipe.

On a double fault the kernel can try and print out the users stack to aid debugging. This option determines how many words of stack should be printed.

On ia32 platforms, this option disables the L2 hardware prefetcher, the L2 adjacent cache line prefetcher, the DCU prefetcher and the DCU IP prefetcher. On the cortex a53 this disables the L1 Data prefetcher.

Enable IPC fastpath. Can be disabled for performance analyses.

This option is a heuristic to attempt to detect when the FPU is no longer in use, allowing the kernel to save the FPU state out so that the FPU does not have to be enabled/disabled every thread switch. Every time we restore a thread and there is active FPU state, we increment this setting and if it exceeds this threshold we switch to the NULL state.

Enable benchamrks including logging and tracing info. Setting this value > 1 enables a 1MB log buffer and functions for extracting data from it at user level. NOTE this is only tested on the sabre and will not work on platforms with < 512mb memory. This is not fully implemented for x86.
none -> No Benchmarking features enabled.
generic -> Enable global benchmarks config variable with no specific features.
track_kernel_entries -> Log kernel entries information including timing, number of invocations and arguments for system calls, interrupts, user faults and VM faults.
tracepoints -> Enable manually inserted tracepoints that the kernel will track time consumed between.
track_utilisation -> Enable the kernel to track each thread’s utilisation time.

The maximum number of different trace point identifiers which can be used. Use TRACE_POINT_START(k) and TRACE_POINT_STOP(k) macros for recording data, where k is an integer between 0 and this value - 1

Select the kernel optimisation level. This should only be changed as part of performance analysis. -O2 is required for normal use.

Enable -fwhole-program when linking kernel. This should work modulo gcc bugs, which are not uncommon with -fwhole-program. Consider this feature experimental!

Adds a system call that allows users to specify code to be run in kernel mode. Useful for profiling.

This describes the log2 size of the kernel stack. Great care should be taken as there is no guard below the stack so setting this too small will cause random memory corruption

Hardware platform to target. This setting influences other kernel configuration values.

Architecture mode for building the kernel.

Set if the platform and toolchain supports floating point unit.

Max number of CPU cores to boot.

Do not enable the L2 cache on startup for debugging purposes.

Do not enable the L1 instruction cache on startup for debugging purposes.

Do not enable the L1 data cache on startup for debugging purposes.

Do not enable branch prediction (also called program flow control) on startup for debugging purposes. This makes execution time more deterministic at the expense of dramatically decreasing performance.

Utilise Arm virtualisation extensions to build the kernel as a hypervisor.

Utilise Arm virtualisation extensions to build the kernel as a hypervisor.

The kernel does not save or restore VCPUs’ CP14 accesses. As a result, accessing VPU threads’ CP14 context triggers a trap, which allows the kernel to intercept the access and deliver it as a fault message to the VM monitor.

Enable a workaround for 430973 Cortex-A8 (r1p0..r1p2) erratum An error occurs if an instruction contains Arm/Thumb interworking branch that is replaced by a different instruction from the same virtual address.

Enable a workaround for 773022 Cortex-A15 (r0p0..r0p4) erratum. An error occurs on rare sequences of instructions which results on the loop buffer delivering incorrect instructions. The workaround is to disable the loop buffer.

Enable the System MMU on the Tegra TK1 SoC.

Enable the prefetcher on Arm Cortex-A9 core. The Cortex-A9 has L1 and L2 prefetchers, which are disabled by default. This config option enables those prefetchers, requiring the kernel to be executed in the secure mode. Arm document indicates that the bit used for enabling those prefetchers is no longer supported from version r4p1 of the Cortex-A9. However, the correctness of that is uncertain.

Grant user access to the performance monitoring unit. While useful for benchmarking, this option opens the possibility of timing channels.

Disable the trapping of WFI and WFE instructions by configuring the Hyp Configuration Registor (HCR) of a VCPU.

Enable system MMU (SMMU) interrupts. System MMU interrupts currently only serve for debugging purpose because they are not forwarded to user level. Enabling this will cause some SMMU fault types to print out a message in the kernel. High frequency faults can result in all time spent in the kernel printing fault messages.

Enable hardware VFP and SIMD context switch. This enables the VFP and SIMD context switch on platforms with hardware support, allowing the user to execute hardware VFP and SIMD operations in a multithreading environment, instead of relying on software emulation of FPU/VFP from the C library (e.g. mfloat-abi=soft).

Select the x86 micro architecture.

Select the IRQ controller seL4 will use. Code for others may still be included if needed to disable at run time.

Configure the maximum number of IOAPIC controllers that can be supported. SeL4 will detect IOAPICs regardless of whether the IOAPIC will actually be used as the final IRQ controller.

Select the mode local APIC will use: XAPIC, X2APIC

Use logical IDs to broadcast IPI between cores. Not all machines support logical IDs. In xAPIC mode only 8 cores can be addressed using logical IDs.

Define cache line size for x86.

VT-x support compiled into the kernel.

IOMMU support for VT-d enabled chipset.

Sets the maximum number of Reserved Memory Region Reporting structures we support recording from the ACPI tables. These structures are used for setting up passthrouh IOMMU mappings for legacy devices.

The kernel maintains a mapping of 16-bit VPIDs to VCPUs. This option should be sized as small as possible to save memory, but be at least the number of VCPUs that will be run for optimum performance.

Add support for 1GB huge page.

Add support for PCIDs (aka hardware ASIDs).

Which syscall method that the kernel supports. This config should be set to the most efficient one that is support by the hardware the system will run on.

Choose the method that FPU state is stored in. This directly affects the method used to save and restore it.
FXSAVE -> This chooses the legacy 512-byte region used by the fxsave and fxrstor functions
XSAVE -> This chooses the variable xsave region, and enables the ability to use any of the xsave variants to save and restore. The actual size of the region is dependent on the features enabled.

The XSAVE area supports multiple instructions to save and restore to it. These instructions are dependent upon specific CPU support. See Chapter 13 of Volume 1 of the Intel Architectures SOftware Developers Manual for discussion on the init and modified optimizations.
XSAVE -> Original XSAVE instruction. This is the only XSAVE instruction that is guaranteed to exist if XSAVE is present
XSAVEC -> Save state with compaction. This compaction has to do with minimizing the total size of XSAVE buffer, if using non contiguous features, XSAVEC will attempt to use the init optimization when saving
XSAVEOPT -> Save state taking advantage of both the init optimization and modified optimization
XSAVES -> Save state taking advantage of the modified optimization. This instruction is only available in OS code, and is the preferred save method if it exists.

XSAVE can save and restore the state for various features through the use of the feature mask. This config option represents the feature mask that we want to support. The CPU must support all bits in this feature mask. Current known bits are
0 - FPU
1 - SSE
2 - AVX
FPU and SSE is guaranteed to exist if XSAVE exists.

There are three ways to to set FS/GS base addresses: IA32_FS/GS_GDT, IA32_FS/GS_BASE_MSR, and fsgsbase instructions. IA32_FS/GS_GDT and IA32_FS/GS_BASE_MSR are availble for 32-bit. IA32_FS/GS_BASE_MSR and fsgsbase instructions are available for 64-bit.

The type of graphics mode to request from the boot loader. This is encoded into the multiboot header and is merely a hint, the boot loader is free to ignore or set some other mode

The bits per pixel of the linear graphics mode ot request. Value of zero indicates no preference.

The width of the graphics mode to request. For a linear graphics mode this is the number of pixels. For a text mode this is the number of characters, value of zero indicates no preference.

The height of the graphics mode to request. For a linear graphics mode this is the number of pixels. For a text mode this is the number of characters, value of zero indicates no preference.

Inserts a header that indicates to the bootloader that the kernel supports a multiboot 1 boot header

Inserts a header that indicates to the bootloader that the kernel supports a multiboot 2 boot header. This is can be enabled together with a multiboot 1 header and the boot loader may use either one

Prevent against the Meltdown vulnerability by using a reduced Static Kernel Image and Micro-state window instead of having all kernel state in the kernel window. This only needs to be enabled if deploying to a vulnerable processor

Grant user access to the Performance Monitoring Counters. This allows the user to read performance counters, although not control what the counters are and whether or not they are counting. Nevertheless whilst this is useful for evalulating performance this option opens timing and covert channels.

Grant user access to the Performance Monitoring Counters. This allows the user to read performance counters, although not control what the counters are and whether or not they are counting. Nevertheless whilst this is useful for evalulating performance this option opens timing and covert channels.

rdmsr/wrmsr kernel interface. Provides a syscall interface for reading and writing arbitrary MSRs. This is extremely dangerous as no checks are performed and exists to aid debugging and benchmarking.

Indirect Branch Restricted Speculation mode Used to prevent a user from manipulating the branch predictor to manipulate speculative execution of other processes. On current processors IBRS has a prohibitive performance penalty and it is recommended that it be disabled such that software mitigations are used instead. Software mitigation is done by disabling jump tables (the only form of indirect jump in seL4 except for ‘ret’) and flushing the RSB on vmexit. Flushing the RSB at other times is not needed as seL4 does not switch kernel stacks and so is not vulnerable to RSB underflow. The STIBP is essentially software mitigation but enables the single thread isolation for branch predictions. This is only needed if attempting to protect user level process from each other in a multicore environment.

Performs a IBPB on every context switch to prevent Spectre attacks between user processes. This is extremely expensive and is recommended you only turn this on if absolutely necessary. Note that in a multicore environment you should also enable STIBP to prevent other cores retraining the branch predictor even after context switch.

Flushes the RSB on context switch to prevent Spectre attacks between user processes. Whilst not nearly as expensive as an IBPB it is not enabled by default as it is largely pointless to flush the RSB without also doing an IBPB as the RSB is already a harder attack vector.