seL4 Project Status

The seL4 project contains a lot of different features and components that work across different hardware platforms and configurations. This page tries to give an overview of what exists, its development status, what level of support it has, who is responsible for maintaining it and where to find more information.

Verification Status

See status about Verified Configurations

Features

Architectures

Features Description Status Maintained by
Arm Arm architecture support. ArmV6, ArmV7, ArmV8, 32 and 64bit Data61
x86 x86 architecture support. ia32 and x86_64 (32/64bit) Data61
RISC-V RISC-V architecture support. riscv32, riscv64, imac extensions, sv32 and sv39 virtual memory Data61

Virtualization extensions

Features Description Status Maintained by
Aarch64 hyp Support for running seL4 in EL2, Aarch64 on ArmV8 Supported on the following platforms: FIXME Data61
arm hyp Support for running seL4 in hyp mode, on ArmV7 Supported on the following platforms: FIXME Data61
Intel VT-x Support for using x86 hardware virtualization on seL4. Supported on the following platforms: FIXME Data61
RISC-V hyp mode Support for utilizing RISC-V Hyp extensions on seL4. [More information](https://github.com/SEL4PROJ/sel4-riscv-vmm-manifest/blob/master/README.md) Experimental branches exist for RISCV HE v0.4 Data61

Multicore

Features Description Status Maintained by
Arm multicore support Support for Arm SMP Supported on the following platforms/cores: FIXME Data61
x86 multicore support Support for x86 SMP Supported on the following platforms/cores: FIXME Data61
RISC-V multicore support Support for RISC-V SMP Supported on the following platforms/cores: HiFive Unleashed Data61

Mixed criticality

Features Description Status Maintained by
MCS Verification support Verification of the MCS extenstions to seL4 Under development. Data61
MCS Hyp support MCS + Hyp extensions on seL4 ?. Data61
MCS SMP support MCS + SMP on seL4 ?. Data61
MCS Fastpath support Fastpath operations require a Scheduling Context donation to occur. ?. Data61

Fastpath

Features Description Status Maintained by
seL4_Call() Fastpath seL4_Call operations that meet certain criteria will use the fastpath. Supported on all platforms Data61
seL4_ReplyRecv() Fastpath seL4_ReplyRecv operations that meet certain criteria will use the fastpath. Supported on all platforms Data61

IOMMU

Features Description Status Maintained by
Intel VT-d x86 IOMMU support on seL4 via additional page table object definitions. Supported on the following platforms/cores: FIXME Data61
Jetson TK1 SMMU Supported on seL4 via additional page table object definitions. Only applies to Jetson TK1 platform. Data61
Arm SMMUv2 Generic Arm SMMU support on seL4 via additional page table object definitions. Under development. Data61

Hardware platforms

See status about Supported platforms.

Components

Components are parts of the project that are more likely to be independent or substituted with other components. They can also be used as building blocks in parts of a wider system.

Verified configurations

A veried configuration is a CMake settings file that is expected to produce a unique kernel image that can be used as an input to he L4.verified project for verification. See Verified Configurations for more information. A verified configuration can be imported into a CMake build system that targets seL4 to set valid verification compatible configuration options. It can also be used to produce a standalone kernel image.

Components Description Status Maintained by
[ARM_HYP verification configuration](https://github.com/seL4/seL4/blob/master/configs/ARM_HYP_verified.cmake) Build configuration settings for ARM_HYP verification target active Data61
ARM_MCS verification configuration Build configuration settings for ARM_MCS verification target active (but ARM_MCS verification support is Coming Soon) Data61
ARM verification configuration Build configuration settings for ARM verification target active Data61
RISCV64 verification configuration Build configuration settings for RISCV64 verification target active (but RISCV64 verification support is Coming Soon) Data61
X64 verification configuration Build configuration settings for X64 verification target active Data61

libsel4

The libsel4 contains the interface that seL4 provides to user-level threads, including system calls, capability types, and definitions of the key data structures (e.g., boot_info).

Manual

The manual contains the source files for generating the seL4 reference manual.

Kernel drivers

Timer

Components Description Status Maintained by
allwinner,sun4i-a10-timer allwinnera20 timer seL4 driver Inactive, currently used by the unmaintained alwinnera20 platform Data61
samsung,exynos4210-mct exynos5 timer seL4 driver that wraps Arm Generic timer Active, currently used by the exynos5 platforms Data61
arm,cortex-a9-global-timer Arm cortex-a9 global timer seL4 driver Active, currently used by the cortex-a9 platforms Data61
qcom,kpss-timer apq8064 timer seL4 driver Inactive, currently used by the currently unmaintained apq8064 seL4 platform Data61
ti,am335x-timer am335x timer seL4 driver Active, currently used by the am335x seL4 platforms Data61
samsung,exynos4412-mct exynos4 timer seL4 driver Active, currently used by the exynos4 seL4 platform Data61
fsl,imx31-epit i.MX31 EPIT timer seL4 driver Active, currently used by the kzm seL4 platform Data61
ti,omap3430-timer omap3 timer seL4 driver Active, currently used by the omap3 seL4 platform Data61
arm,armv7-timer;arm,armv8-timer Arm generic timer seL4 driver Active, currently used by several Arm seL4 platforms Data61
fsl,imx31-gpt i.MX31 GPT timer seL4 driver Active, currently used by the kzm seL4 platform Data61
arm,cortex-a9-twd-timer Arm cortex-a9 private timer seL4 driver Active, currently used by the cortex-a9 seL4 platforms Data61
pc99,pit x86 PIT timer seL4 driver Active, currently used by the pc99 seL4 platform Data61

Serial

Components Description Status Maintained by
brcm,bcm2835-aux-uart Raspberry Pi serial seL4 driver active, currently used by the rpi3 seL4 platform Data61
samsung,exynos4210-uart exynos4210 serial seL4 driver active, currently used by the exynos4 seL4 platform Data61
amlogic,meson-gx-uart odroidc2 serial seL4 driver active, currently used by the odroidc2 seL4 platform Data61
arm,pl011 Arm standard serial seL4 driver active, currently used by several seL4 platforms Data61
xlnx,xuartps Xilinx serial seL4 driver active, currently used by some zynq* seL4 platforms Data61
fsl,imx**-uart i.MX serial seL4 driver active, currently used by some imx* seL4 platforms Data61
qcom,msm-uartdm apq8064 serial seL4 driver Inactive, currently used by the currently unmaintained apq8064 seL4 platform Data61
nvidia,tegra20-uart;ti,omap3-uart;snps,dw-apb-uart Simple Arm serial seL4 driver Active, currently used by nvidia- and beagle- based seL4 platforms Data61
x86,serial Intel COM port serial seL4 driver Active, currently used by the pc99 seL4 platform Data61

Interrupt controllers

Components Description Status Maintained by
ti,am33xx-intc am335x interrupt controller seL4 driver active, currently used by am335x seL4 platforms Data61
brcm,bcm2836-armctrl-ic Broadcom Raspberry Pi interrupt controller seL4 driver active, currently used by the rpi3 seL4 platform Data61
hifive-plic HiFive interrupt controller seL4 driver active, currently used by the hifive seL4 platform Data61
fsl,imx31-avic i.MX31 interrupt controller seL4 driver active, currently used by the kzm seL4 platform Data61
ti,omap3-intc omap3 interrupt controller seL4 driver active, currently used by the omap3 seL4 platform Data61
arm,gic-v2 Arm GICv2 interrupt controller seL4 driver active, currently used by several seL4 platforms Data61
arm,gic-v3 Arm GICv2 interrupt controller seL4 driver active, currently used by several seL4 platforms Data61
x86,pic Intel 8259 Programmable Interrupt Controller (PIC) seL4 driver active, currently used by the pc99 seL4 platform Data61
x86,ioapic Intel IOAPIC seL4 driver active, currently used by the pc99 seL4 platform Data61
x86,lapic Intel Local APIC seL4 IRQ and timer driver active, currently used by the pc99 seL4 platform Data61

IOMMUs

Components Description Status Maintained by
tk1,smmu Tegra K1 System MMU (SMMU) seL4 driver Active, currently used by the tk1 seL4 platform Data61
intel,vtd Intel VT-d (IOMMU) seL4 driver Active, currently used by the pc99 seL4 platform Data61

Device trees

Components Description Status Maintained by
am335x-boneblack.dts am335x-boneblack platform device tree (dts) sourced from Linux kernel path: am335x-boneblack active Data61
am335x-boneblue.dts am335x-boneblue platform device tree (dts) sourced from Linux kernel path: am335x-boneblue active Data61
rpi3.dts rpi3 platform device tree (dts) sourced from Linux kernel path: bcm2837-rpi-3-b active Data61
exynos4.dts exynos4 platform device tree (dts) sourced from Linux kernel path: exynos4412-odroidx active Data61
exynos5250.dts exynos5250 platform device tree (dts) sourced from Linux kernel path: exynos5250-arndale active Data61
exynos5410.dts exynos5410 platform device tree (dts) sourced from Linux kernel path: exynos5410-odroidxu active Data61
exynos5422.dts exynos5422 platform device tree (dts) sourced from Linux kernel path: exynos5422-odroidxu4 active Data61
kzm.dts kzm platform device tree (dts) sourced from Linux kernel path: imx31-bug active Data61
sabre.dts sabre platform device tree (dts) sourced from Linux kernel path: imx6q-sabrelite active Data61
wandq.dts wandq platform device tree (dts) sourced from Linux kernel path: imx6q-wandboard-revd1 active Data61
imx7sabre.dts imx7sabre platform device tree (dts) sourced from Linux kernel path: imx7d-sdb active Data61
omap3.dts omap3 platform device tree (dts) sourced from Linux kernel path: omap3-beagle active Data61
apq8064.dts apq8064 platform device tree (dts) sourced from Linux kernel path: qcom-apq8064-ifc6410 active Data61
allwinnera20.dts allwinnera20 platform device tree (dts) sourced from Linux kernel path: sun7i-a20-cubietruck active Data61
tk1.dts tk1 platform device tree (dts) sourced from Linux kernel path: tegra124-jetson-tk1 active Data61
zynq7000.dts zynq7000 platform device tree (dts) sourced from Linux kernel path: zynq-zc706 active Data61
odroidc2.dts odroidc2 platform device tree (dts) sourced from Linux kernel path: amlogic/meson-gxbb-odroidc2 active Data61
hikey.dts hikey platform device tree (dts) sourced from Linux kernel path: hisilicon/hi6220-hikey active Data61
tx1.dts tx1 platform device tree (dts) sourced from Linux kernel path: nvidia/tegra210-p2371-2180 active Data61
ultra96.dts ultra96 platform device tree (dts) sourced from Linux kernel path: xilinx/avnet-ultra96-rev1 active Data61
zynqmp.dts zynqmp platform device tree (dts) sourced from Linux kernel path: xilinx/zynqmp-zcu102-rev1.0 active Data61
imx8mq-evk.dts imx8mq-evk platform device tree (dts) sourced from Linux kernel path: freescale/fsl-imx8mq-evk active Data61
imx8mm-evk.dts imx8mm-evk platform device tree (dts) sourced from Linux kernel path: freescale/fsl-imx8mm-evk active Data61
rockpro64.dts rockpro64 platform device tree (dts) sourced from Linux kernel path: rockchip/rk3399-rockpro64 active Data61

Testing and Benchmarking

Testing

In addition to its verification, there is also an seL4 test suite sel4test that can be built for a particular seL4 configuration. The test suite is self-hosted and starts as the initial roottask on seL4.

Benchmarking

A suite of benchmarks for measuring different seL4 operations are provided by sel4bench. This project is also built as a self-hosted root-task application on seL4.

Configurations

seL4 has several different options available for configuring seL4 to execute in different scenarios. Many of these options are only expected to used during application or kernel development and may not be suitable for a final release deployment that wants to leverage seL4’s full capabilities.

Due to the experimental nature of many of the options, there may be undocumented incompatabilities when trying to configure several options together. seL4test, seL4bench or other user level examples can be used to test a baseline level of configuration correctness.

Generic configuration options

Configurations Description Status Maintained by
KernelVerificationBuild When enabled this configuration option prevents the usage of any other options thatwould compromise the verification story of the kernel. Enabling this option does NOTimply you are using a verified kernel. Always set. (Default: ON) Data61
KernelIsMCS Enable MCS feature for seL4. Available on all MCS supported platforms (Default: Off) Data61
KernelRootCNodeSizeBits 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. Always set (Default: 12) Data61
KernelRetypeFanOutLimit Maximum number of objects that can be created in a single Retype() invocation. Always set. (Default: 256) Data61
KernelMaxNumBootinfoUntypedCaps Max number of untyped capabilities given to initial boot thread. Additional caps won't be handed to the system. Always set. (Default: 230 caps) Data61

Scheduling configuration options

Configurations Description Status Maintained by
KernelTimerTickMS Kernel timer tick period in milliseconds. Only available on non-MCS kernels. (Default: 2 milliseconds) Data61
KernelTimeSlice Number of kernel timer ticks until a thread is preempted. Only available on non-MCS kernels. (Default: 5 ticks) Data61
KernelBootThreadTimeSlice Budget of booth thread: Number of milliseconds until the boot thread is preempted. Available on all MCS supported platforms. (Default: 5 milliseconds) Data61
KernelMaxNumWorkUnitsPerPreemption Maximum number of work units (delete/revoke iterations) until the kernel checks forpending interrupts (and preempts the currently running syscall if interrupts are pending). Always set. (Default: 100) Data61
KernelResetChunkBits Maximum size in bits of chunks of memory to zero before checking a preemption point. Always set. (Default: 8 bits) Data61
KernelNumDomains The number of scheduler domains in the system Always set. (Default: 1 domain) Data61
KernelDomainSchedule A C file providing the symbols ksDomSchedule and ksDomeScheudleLength to be linked with the kernel as a scheduling configuration. Always set. (Default: src/config/default_domain.c) Data61
KernelNumPriorities The number of priority levels per domain. Always set, Valid range 1-256. (Default: 256) Data61
KernelWcetScale 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. Enabled if KernelIsMCS. (Default: 1) Data61

Debug configuration options

Configurations Description Status Maintained by
KernelDebugBuild Enable debug facilities (symbols and assertions) in the kernel Disabled if KernelVerificationBuild is set. (Default: ON) Data61
HardwareDebugAPI 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. Requires platform support. (Default: Off) Data61
KernelPrinting Allow the kernel to print out messages to the serial console during bootup and execution. Disabled if KernelVerificationBuild is set. (Default: Set to initial value of KernelDebugBuild) Data61
KernelIRQReporting 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. Enabled if KernelPrinting is set. (Default: On) Data61
KernelColourPrinting 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. Enabled if KernelPrinting is set. (Default: On) Data61
KernelUserStackTraceLength 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. Enabled if KernelPrinting is set. (Default: 16) Data61
KernelDebugDisablePrefetchers 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. Available if KernelArchX86 OR KernelPlatformHikey is set. (Default: Off) Data61

Performance analysis and profiling configuration options

Configurations Description Status Maintained by
KernelFastpath Enable IPC fastpath. Can be disabled for performance analyses. Always set. (Default: ON) Data61
KernelFPUMaxRestoresSinceSwitch 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 beenabled/disabled every thread switch. Every time we restore a thread and there isactive FPU state, we increment this setting and if it exceeds this threshold weswitch to the NULL state. Only set if the system is using the FPU. (Default: 64 switches) Data61
KernelBenchmarks 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.
(FIXME: Which config supported?) Disabled if KernelVerificationBuild is set. (Default: None) Data61
KernelMaxNumTracePoints 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 Requires KernelBenchmarksTracepoints is set. (Default: 1) Data61
KernelOptimisation Select the kernel optimisation level. This should only be changed as part of performance analysis. -O2 is required for normal use. Always set. (Default: -O2) Data61
KernelFWholeProgram Enable -fwhole-program when linking kernel. This should work modulo gcc bugs, which are not uncommon with -fwhole-program. Consider this feature experimental! Always set. (Default: OFF) Data61
KernelDangerousCodeInjection Adds a system call that allows users to specify code to be run in kernel mode. Useful for profiling. Can only be set if: NOT KernelARMHypervisorSupport;NOT KernelVerificationBuild;NOT KernelPlatformHikey;NOT KernelSkimWindow. (Default: Off) Data61
KernelStackBits This describes the log2 size of the kernel stack. Great care should be taken asthere is no guard below the stack so setting this too small will cause randommemory corruption Always set. (Default: 12 bits) Data61

Target hardware architecture/platform options

Configurations Description Status Maintained by
KernelPlatform Hardware platform to target. This setting influences other kernel configuration values. Supported platforms can be found [here](http://127.0.0.1:4000/status/sel4#hardware-platforms). Data61
KernelSel4Arch Architecture mode for building the kernel. Supported values: (aarch32, aarch64, arm_hyp, riscv32, riscv64, x86_64, ia32). Data61
KernelHaveFPU Set if the platform and toolchain supports floating point unit. Set on x86, Unset on RISC-V, toolchain + verirification dependent on Arm Data61
KernelMaxNumNodes Max number of CPU cores to boot. Always set. (Default: 1 node) Data61

x86

Configurations Description Status Maintained by
KernelX86MicroArch Select the x86 micro architecture. x86 Option. Supported options:nehalem, generic, westmere, sandy, ivy, haswell, broadwell, skylake. (Default: nehalem) Data61
KernelIRQController (x86) Select the IRQ controller seL4 will use. Code for others may still be included if needed to disable at run time. x86 Option. Supported options: PIC, IOAPIC. (Default: IOAPIC) Data61
KernelMaxNumIOAPIC 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. x86 Option. (Default: 1) Data61
KernelLAPICMode Select the mode local APIC will use: XAPIC, X2APIC x86 Option. Not all machines support X2APIC mode (Default: XAPIC) Data61
KernelUseLogcalIDs 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. x86 Option. (Default: OFF) Data61
KernelCacheLnSz (x86) Define cache line size for x86. x86 Option. (Default: 64) Data61
KernelVTX (x86) VT-x support compiled into the kernel. x86 Option. (Default: Off) Data61
KernelIOMMU (x86) IOMMU support for VT-d enabled chipset. x86 Option. (Default: ON) Data61
KernelMaxRMRREntries 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. x86 Option. (Default: 32) Data61
KernelMaxVPIDs 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. x86 Option. (Default: 1024) Data61
KernelHugePage (x86) Add support for 1GB huge page. x86 Option. Not all recent processor models support this feature (Default: On) Data61
KernelSupportPCID Add support for PCIDs (aka hardware ASIDs). x86_64 Option. Not all recent processor models support this feature (Default: On) Data61
KernelSyscall (x86) 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. x86 Option. The kernel only ever supports one method at a time: syscall, sysenter (Default: syscall) Data61
KernelFPU (x86) 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.
x86 Option. (Default: XSAVE) Data61
KernelXSave (x86) 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.
x86 Option. (Default: XSAVEOPT) Data61
KernelXSaveFeatureSet (x86) 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.
x86 Option. (Default: 3) Data61
KernelFSGSBase (x86) 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. x86 Option. (Default x86_64: fsgsbase, ia32: gdt) Data61
KernelMultibootGFXMode (x86) 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 x86 Option. Options: none, text, linear (Default: none) Data61
KernelMultibootGFXDepth (x86) The bits per pixel of the linear graphics mode ot request. Value of zero indicates no preference. x86 Option. (Default: 32) Data61
KernelMultibootGFXWidth (x86) 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. x86 Option. (Default: 0) Data61
KernelMultibootGFXHeight (x86) 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. x86 Option. (Default: 0) Data61
KernelMultiboot1Header (x86) Inserts a header that indicates to the bootloader that the kernel supports a multiboot 1 boot header x86 Option. (Default: On) Data61
KernelMultiboot2Header (x86) 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 x86 Option. (Default: On) Data61
KernelSkimWindow (x86) 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 x86_64 Option. (Default: On) Data61
KernelExportPMCUser (x86) 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. x86 Option. (Default: Off) Data61
KernelExportPMCUser (x86) 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. x86 Option. (Default: Off) Data61
KernelX86DangerousMSR 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. x86 Option. (Default: Off) Data61
KernelX86IBRSMode 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. x86 Option. (Default: ibrs_none) Data61
KernelX86IBPBOnContextSwitch 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. x86 Option. (Default: OFF) Data61
KernelX86RSBOnContextSwitch 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. x86 Option. (Default: OFF) Data61

Arm

Configurations Description Status Maintained by
KernelDangerousCodeInjectionOnUndefInstr Replaces the undefined instruction handler with a call to a function pointer in r8. This is an alternative mechanism to the code injection syscall. This option is mainly used for benchmarking the kernel on ARMv6 platforms and has no effect on non-ARMv6 platforms. Arm option. (Default: OFF) Data61
KernelDebugDisableL2Cache Do not enable the L2 cache on startup for debugging purposes. Arm option. (Default: OFF) Data61
KernelDebugDisableL1ICache Do not enable the L1 instruction cache on startup for debugging purposes. Arm option. (Default: OFF) Data61
KernelDebugDisableL1DCache Do not enable the L1 data cache on startup for debugging purposes. Arm option. (Default: OFF) Data61
KernelDebugDisableBranchPrediction 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. Arm option. (Default: OFF) Data61
KernelArmHypervisorSupport Utilise Arm virtualisation extensions to build the kernel as a hypervisor. Arm option. (Default: the value of ARM_HYP (TRUE or FALSE)) Data61
KernelArmHypervisorSupport Utilise Arm virtualisation extensions to build the kernel as a hypervisor. Arm option. (Default: the value of ARM_HYP (TRUE or FALSE)) Data61
KernelArmHypEnableVCPUCP14SaveAndRestore 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. Arm option. (Default: ON) Data61
KernelArmErrata430973 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. Arm option. (Default: OFF) Data61
KernelArmErrata773022 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. Arm option. (Default: OFF) Data61
KernelArmSMMU Enable the System MMU on the Tegra TK1 SoC. Arm option. (Default: OFF) Data61
KernelArmEnableA9Prefetcher 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. Arm option. (Default: OFF) Data61
KernelArmExportPMUUser Grant user access to the performance monitoring unit. While useful for benchmarking, this option opens the possibility of timing channels. Arm option. (Default: OFF) Data61
KernelArmDisableWFIWFETraps Disable the trapping of WFI and WFE instructions by configuring the Hyp Configuration Registor (HCR) of a VCPU. Arm option. (Default: OFF) Data61
KernelARMSMMUInterruptEnable 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. Arm option. (Default: OFF) Data61
KernelAArch32FPUEnableContextSwitch 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). Arm option. (Default: ON) Data61