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 | seL4 Foundation |
| x86 | x86 architecture support. | ia32 and x86_64 (32/64bit) | seL4 Foundation |
| RISC-V | RISC-V architecture support. | riscv32, riscv64, imac extensions, sv32 and sv39 virtual memory | seL4 Foundation |
Virtualization extensions
| Features | Description | Status | Maintained by |
|---|---|---|---|
| Aarch64 hyp | Support for running seL4 in EL2, Aarch64 on ArmV8 | Supported on the following platforms: FIXME | seL4 Foundation |
| arm hyp | Support for running seL4 in hyp mode, on ArmV7 | Supported on the following platforms: FIXME | seL4 Foundation |
| Intel VT-x | Support for using x86 hardware virtualization on seL4. | Supported on the following platforms: FIXME | seL4 Foundation |
| 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.6 | seL4 Foundation |
Multicore
| Features | Description | Status | Maintained by |
|---|---|---|---|
| Arm multicore support | Support for Arm SMP | Supported on the following platforms/cores: FIXME | seL4 Foundation |
| x86 multicore support | Support for x86 SMP | Supported on the following platforms/cores: FIXME | seL4 Foundation |
| RISC-V multicore support | Support for RISC-V SMP | Supported on the following platforms/cores: HiFive Unleashed | seL4 Foundation |
Mixed criticality
| Features | Description | Status | Maintained by |
|---|---|---|---|
| MCS Verification support | Verification of the MCS extenstions to seL4 | Under development. | seL4 Foundation |
| MCS Hyp support | MCS + Hyp extensions on seL4 | ?. | seL4 Foundation |
| MCS SMP support | MCS + SMP on seL4 | ?. | seL4 Foundation |
| MCS Fastpath support | Fastpath operations require a Scheduling Context donation to occur. | ?. | seL4 Foundation |
Fastpath
| Features | Description | Status | Maintained by |
|---|---|---|---|
| seL4_Call() Fastpath | seL4_Call operations that meet certain criteria will use the fastpath. | Supported on all platforms | seL4 Foundation |
| seL4_ReplyRecv() Fastpath | seL4_ReplyRecv operations that meet certain criteria will use the fastpath. | Supported on all platforms | seL4 Foundation |
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 | seL4 Foundation |
| Jetson TK1 SMMU | Supported on seL4 via additional page table object definitions. | Only applies to Jetson TK1 platform. | seL4 Foundation |
| Arm SMMUv2 | Generic Arm SMMU support on seL4 via additional page table object definitions. | Under development. | seL4 Foundation |
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 | seL4 Foundation |
| ARM_MCS verification configuration | Build configuration settings for ARM_MCS verification target | active (but ARM_MCS verification support is Coming Soon) | seL4 Foundation |
| ARM verification configuration | Build configuration settings for ARM verification target | active | seL4 Foundation |
| RISCV64 verification configuration | Build configuration settings for RISCV64 verification target | active (but RISCV64 verification support is Coming Soon) | seL4 Foundation |
| X64 verification configuration | Build configuration settings for X64 verification target | active | seL4 Foundation |
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 | seL4 Foundation |
| samsung,exynos4210-mct | exynos5 timer seL4 driver that wraps Arm Generic timer | Active, currently used by the exynos5 platforms | seL4 Foundation |
| arm,cortex-a9-global-timer | Arm cortex-a9 global timer seL4 driver | Active, currently used by the cortex-a9 platforms | seL4 Foundation |
| qcom,kpss-timer | apq8064 timer seL4 driver | Inactive, currently used by the currently unmaintained apq8064 seL4 platform | seL4 Foundation |
| ti,am335x-timer | am335x timer seL4 driver | Active, currently used by the am335x seL4 platforms | seL4 Foundation |
| samsung,exynos4412-mct | exynos4 timer seL4 driver | Active, currently used by the exynos4 seL4 platform | seL4 Foundation |
| ti,omap3430-timer | omap3 timer seL4 driver | Active, currently used by the omap3 seL4 platform | seL4 Foundation |
| arm,armv7-timer;arm,armv8-timer | Arm generic timer seL4 driver | Active, currently used by several Arm seL4 platforms | seL4 Foundation |
| arm,cortex-a9-twd-timer | Arm cortex-a9 private timer seL4 driver | Active, currently used by the cortex-a9 seL4 platforms | seL4 Foundation |
| pc99,pit | x86 PIT timer seL4 driver | Active, currently used by the pc99 seL4 platform | seL4 Foundation |
Serial
| Components | Description | Status | Maintained by |
|---|---|---|---|
| brcm,bcm2835-aux-uart | Raspberry Pi serial seL4 driver | active, currently used by the rpi3 seL4 platform | seL4 Foundation |
| samsung,exynos4210-uart | exynos4210 serial seL4 driver | active, currently used by the exynos4 seL4 platform | seL4 Foundation |
| amlogic,meson-gx-uart | odroidc2 serial seL4 driver | active, currently used by the odroidc2 seL4 platform | seL4 Foundation |
| arm,pl011 | Arm standard serial seL4 driver | active, currently used by several seL4 platforms | seL4 Foundation |
| xlnx,xuartps | Xilinx serial seL4 driver | active, currently used by some zynq* seL4 platforms | seL4 Foundation |
| fsl,imx**-uart | i.MX serial seL4 driver | active, currently used by some imx* seL4 platforms | seL4 Foundation |
| qcom,msm-uartdm | apq8064 serial seL4 driver | Inactive, currently used by the currently unmaintained apq8064 seL4 platform | seL4 Foundation |
| 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 | seL4 Foundation |
| x86,serial | Intel COM port serial seL4 driver | Active, currently used by the pc99 seL4 platform | seL4 Foundation |
Interrupt controllers
| Components | Description | Status | Maintained by |
|---|---|---|---|
| ti,am33xx-intc | am335x interrupt controller seL4 driver | active, currently used by am335x seL4 platforms | seL4 Foundation |
| brcm,bcm2836-armctrl-ic | Broadcom Raspberry Pi interrupt controller seL4 driver | active, currently used by the rpi3 seL4 platform | seL4 Foundation |
| hifive-plic | HiFive interrupt controller seL4 driver | active, currently used by the hifive seL4 platform | seL4 Foundation |
| ti,omap3-intc | omap3 interrupt controller seL4 driver | active, currently used by the omap3 seL4 platform | seL4 Foundation |
| arm,gic-v2 | Arm GICv2 interrupt controller seL4 driver | active, currently used by several seL4 platforms | seL4 Foundation |
| arm,gic-v3 | Arm GICv2 interrupt controller seL4 driver | active, currently used by several seL4 platforms | seL4 Foundation |
| x86,pic | Intel 8259 Programmable Interrupt Controller (PIC) seL4 driver | active, currently used by the pc99 seL4 platform | seL4 Foundation |
| x86,ioapic | Intel IOAPIC seL4 driver | active, currently used by the pc99 seL4 platform | seL4 Foundation |
| x86,lapic | Intel Local APIC seL4 IRQ and timer driver | active, currently used by the pc99 seL4 platform | seL4 Foundation |
IOMMUs
| Components | Description | Status | Maintained by |
|---|---|---|---|
| tk1,smmu | Tegra K1 System MMU (SMMU) seL4 driver | Active, currently used by the tk1 seL4 platform | seL4 Foundation |
| intel,vtd | Intel VT-d (IOMMU) seL4 driver | Active, currently used by the pc99 seL4 platform | seL4 Foundation |
Device trees
| Components | Description | Status | Maintained by |
|---|---|---|---|
| am335x-boneblack.dts | am335x-boneblack platform device tree (dts) sourced from Linux kernel path: am335x-boneblack | active | seL4 Foundation |
| am335x-boneblue.dts | am335x-boneblue platform device tree (dts) sourced from Linux kernel path: am335x-boneblue | active | seL4 Foundation |
| rpi3.dts | rpi3 platform device tree (dts) sourced from Linux kernel path: bcm2837-rpi-3-b | active | seL4 Foundation |
| exynos4.dts | exynos4 platform device tree (dts) sourced from Linux kernel path: exynos4412-odroidx | active | seL4 Foundation |
| exynos5250.dts | exynos5250 platform device tree (dts) sourced from Linux kernel path: exynos5250-arndale | active | seL4 Foundation |
| exynos5410.dts | exynos5410 platform device tree (dts) sourced from Linux kernel path: exynos5410-odroidxu | active | seL4 Foundation |
| exynos5422.dts | exynos5422 platform device tree (dts) sourced from Linux kernel path: exynos5422-odroidxu4 | active | seL4 Foundation |
| sabre.dts | sabre platform device tree (dts) sourced from Linux kernel path: imx6q-sabrelite | active | seL4 Foundation |
| wandq.dts | wandq platform device tree (dts) sourced from Linux kernel path: imx6q-wandboard-revd1 | active | seL4 Foundation |
| imx7sabre.dts | imx7sabre platform device tree (dts) sourced from Linux kernel path: imx7d-sdb | active | seL4 Foundation |
| omap3.dts | omap3 platform device tree (dts) sourced from Linux kernel path: omap3-beagle | active | seL4 Foundation |
| apq8064.dts | apq8064 platform device tree (dts) sourced from Linux kernel path: qcom-apq8064-ifc6410 | active | seL4 Foundation |
| allwinnera20.dts | allwinnera20 platform device tree (dts) sourced from Linux kernel path: sun7i-a20-cubietruck | active | seL4 Foundation |
| tk1.dts | tk1 platform device tree (dts) sourced from Linux kernel path: tegra124-jetson-tk1 | active | seL4 Foundation |
| zynq7000.dts | zynq7000 platform device tree (dts) sourced from Linux kernel path: zynq-zc706 | active | seL4 Foundation |
| odroidc2.dts | odroidc2 platform device tree (dts) sourced from Linux kernel path: amlogic/meson-gxbb-odroidc2 | active | seL4 Foundation |
| hikey.dts | hikey platform device tree (dts) sourced from Linux kernel path: hisilicon/hi6220-hikey | active | seL4 Foundation |
| tx1.dts | tx1 platform device tree (dts) sourced from Linux kernel path: nvidia/tegra210-p2371-2180 | active | seL4 Foundation |
| ultra96.dts | ultra96 platform device tree (dts) sourced from Linux kernel path: xilinx/avnet-ultra96-rev1 | active | seL4 Foundation |
| zynqmp.dts | zynqmp platform device tree (dts) sourced from Linux kernel path: xilinx/zynqmp-zcu102-rev1.0 | active | seL4 Foundation |
| imx8mq-evk.dts | imx8mq-evk platform device tree (dts) sourced from Linux kernel path: freescale/fsl-imx8mq-evk | active | seL4 Foundation |
| imx8mm-evk.dts | imx8mm-evk platform device tree (dts) sourced from Linux kernel path: freescale/fsl-imx8mm-evk | active | seL4 Foundation |
| rockpro64.dts | rockpro64 platform device tree (dts) sourced from Linux kernel path: rockchip/rk3399-rockpro64 | active | seL4 Foundation |
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) | seL4 Foundation |
| KernelIsMCS | Enable MCS feature for seL4. | Available on all MCS supported platforms (Default: Off) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelRetypeFanOutLimit | Maximum number of objects that can be created in a single Retype() invocation. | Always set. (Default: 256) | seL4 Foundation |
| 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) | seL4 Foundation |
Scheduling configuration options
| Configurations | Description | Status | Maintained by |
|---|---|---|---|
| KernelTimerTickMS | Kernel timer tick period in milliseconds. | Only available on non-MCS kernels. (Default: 2 milliseconds) | seL4 Foundation |
| KernelTimeSlice | Number of kernel timer ticks until a thread is preempted. | Only available on non-MCS kernels. (Default: 5 ticks) | seL4 Foundation |
| KernelBootThreadTimeSlice | Budget of booth thread: Number of milliseconds until the boot thread is preempted. | Available on all MCS supported platforms. (Default: 5 milliseconds) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelResetChunkBits | Maximum size in bits of chunks of memory to zero before checking a preemption point. | Always set. (Default: 8 bits) | seL4 Foundation |
| KernelNumDomains | The number of scheduler domains in the system | Always set. (Default: 1 domain) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelNumPriorities | The number of priority levels per domain. | Always set, Valid range 1-256. (Default: 256) | seL4 Foundation |
| 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) | seL4 Foundation |
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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
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). | seL4 Foundation |
| KernelSel4Arch | Architecture mode for building the kernel. | Supported values: (aarch32, aarch64, arm_hyp, riscv32, riscv64, x86_64, ia32). | seL4 Foundation |
| KernelHaveFPU | Set if the platform and toolchain supports floating point unit. | Set on x86, Unset on RISC-V, toolchain + verirification dependent on Arm | seL4 Foundation |
| KernelMaxNumNodes | Max number of CPU cores to boot. | Always set. (Default: 1 node) | seL4 Foundation |
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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelLAPICMode | Select the mode local APIC will use: XAPIC, X2APIC | x86 Option. Not all machines support X2APIC mode (Default: XAPIC) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelCacheLnSz (x86) | Define cache line size for x86. | x86 Option. (Default: 64) | seL4 Foundation |
| KernelVTX (x86) | VT-x support compiled into the kernel. | x86 Option. (Default: Off) | seL4 Foundation |
| KernelIOMMU (x86) | IOMMU support for VT-d enabled chipset. | x86 Option. (Default: ON) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelHugePage (x86) | Add support for 1GB huge page. | x86 Option. Not all recent processor models support this feature (Default: On) | seL4 Foundation |
| KernelSupportPCID | Add support for PCIDs (aka hardware ASIDs). | x86_64 Option. Not all recent processor models support this feature (Default: On) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelMultibootGFXDepth (x86) | The bits per pixel of the linear graphics mode ot request. Value of zero indicates no preference. | x86 Option. (Default: 32) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelMultiboot1Header (x86) | Inserts a header that indicates to the bootloader that the kernel supports a multiboot 1 boot header | x86 Option. (Default: On) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
Arm
| Configurations | Description | Status | Maintained by |
|---|---|---|---|
| KernelDebugDisableL2Cache | Do not enable the L2 cache on startup for debugging purposes. | Arm option. (Default: OFF) | seL4 Foundation |
| KernelDebugDisableL1ICache | Do not enable the L1 instruction cache on startup for debugging purposes. | Arm option. (Default: OFF) | seL4 Foundation |
| KernelDebugDisableL1DCache | Do not enable the L1 data cache on startup for debugging purposes. | Arm option. (Default: OFF) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelArmHypervisorSupport | Utilise Arm virtualisation extensions to build the kernel as a hypervisor. | Arm option. (Default: the value of ARM_HYP (TRUE or FALSE)) | seL4 Foundation |
| KernelArmHypervisorSupport | Utilise Arm virtualisation extensions to build the kernel as a hypervisor. | Arm option. (Default: the value of ARM_HYP (TRUE or FALSE)) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelArmSMMU | Enable the System MMU on the Tegra TK1 SoC. | Arm option. (Default: OFF) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |
| KernelArmDisableWFIWFETraps | Disable the trapping of WFI and WFE instructions by configuring the Hyp Configuration Registor (HCR) of a VCPU. | Arm option. (Default: OFF) | seL4 Foundation |
| 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) | seL4 Foundation |
| 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) | seL4 Foundation |