sel4/sel4

The seL4 microkernel

The seL4 microkernel

This project contains the source code of seL4 microkernel.

For details about the seL4 microkernel, including details about its formal correctness proof, please see the sel4.systems website and associated FAQ.

DOIs for citing recent releases of this repository:

• 

We welcome contributions to seL4. Please see the website for information on how to contribute.

This repository is usually not used in isolation, but as part of the build system in a larger project.

seL4 Basics

• Tutorials
• Documentation
• seL4 libraries
• seL4Test
• Debugging guide
• Benchmarking guide
• Virtualization on seL4
• Host Build Dependencies
• Porting seL4

Community

• Forums:
  • Discourse
  • seL4 Announce
  • seL4 Devel
• Suggested projects
• Community projects

See the contact links on the seL4 website for the full list.

Reporting security vulnerabilities

If you believe you have found a security vulnerability in seL4 or related software, we ask you to follow our vulnerability disclosure policy.

Manual

A hosted version of the manual for the most recent release can be found here.

A web version of the API can be found here

Repository Overview

• include and src: C and ASM source code of seL4
• tools: build tools
• libsel4: C bindings for the seL4 ABI
• manual: LaTeX sources of the seL4 reference manual

Build Instructions

See the seL4 website for build instructions.

Status

A list of releases and current project status can be found under seL4 releases.

• Roadmap: new features in development
• Hardware Support: information about hardware platform ports
• Kernel Features: information about available kernel features
• Userland Components and Drivers: available device drivers and userland components

License

See the file LICENSE.md.

sel4's Issues

irq_t / interrupt_t implicit conversion

In file included from seL4/src/api/faults.c:16:
In file included from seL4/include/api/syscall.h:15:
In file included from seL4/include/machine.h:18:
In file included from seL4/include/plat/pc99/plat/machine/hardware.h:15:
seL4/include/plat/pc99/plat/machine/interrupt.h:53:17: warning: implicit conversion from enumeration type 'interrupt_t' (aka 'enum _interrupt_t') to different enumeration type 'irq_t' (aka 'enum _irq_t') [-Wenum-conversion]
    irq_t ret = x86KSPendingInterrupt;
          ~~~   ^~~~~~~~~~~~~~~~~~~~~
seL4/include/plat/pc99/plat/machine/interrupt.h:78:29: warning: implicit conversion from enumeration type 'irq_t' (aka 'enum _irq_t') to different enumeration type 'interrupt_t' (aka 'enum _interrupt_t') [-Wenum-conversion]
        x86KScurInterrupt = servicePendingIRQ();
                          ~ ^~~~~~~~~~~~~~~~~~~

issue when building for tegra k1

Hi,

When trying to build for the Tegra K1, I got the following issue. To reproduce the issue:

1. make beagle_debug_xml_defconfig
2. make oldconfig
3. make menuconfig edit the platform and select the Tegra
4. make

In file included from /home/sel4/tegra-test/stage/arm//include/platsupport/io.h:24:0,
from /home/sel4/tegra-test/stage/arm//include/platsupport/timer.h:17,
from /home/sel4/tegra-test/libs/libplatsupport/src/arch/arm/generic_timer.c:18:
/home/sel4/tegra-test/stage/arm//include/platsupport/clock.h:27:36: fatal error: platsupport/plat/clock.h: No such file or directory
compilation terminated.

Streamline kernel/libsel4 and remove its libc dependencies

Currently libsel4 has support for more than just interfacing to the kernel, it should be simplified and also it would be desirable to not require libc to use libsel4. The current libc (musl) contains support for many system calls not provided by seL4, one example is thread creation and there are other features, such as capabilities which musl will not likely ever support.

Therefore not having libsel4 depend upon libc can significantly reduce the amount of code needed for some uses of seL4. See this thread (http://sel4.systems/pipermail/devel/2015-June/000391.html) for some additional discussion.

MOD_PYTHON error on http://sel4.systems

sel4.systems is not reachable. Probably module lxml is not installed properly.

ProcessId:      3936
Interpreter:    'sel4.systems.keg.ertos.in.nicta.com.au'

ServerName:     'sel4.systems.keg.ertos.in.nicta.com.au'
DocumentRoot:   '/var/www/seL4/content'

URI:            '/home.pml'
Location:       '/home.pml'
Directory:      None
Filename:       '/var/www/seL4/content/home.pml'
PathInfo:       None

Phase:          'PythonHandler'
Handler:        'ertos'

Traceback (most recent call last):

  File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1537, in HandlerDispatch
    default=default_handler, arg=req, silent=hlist.silent)

  File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1202, in _process_target
    module = import_module(module_name, path=path)

  File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 304, in import_module
    return __import__(module_name, {}, {}, ['*'])

  File "/var/www/seL4/code/ertos.py", line 5, in <module>
    from lxml import etree

ImportError: No module named lxml

64-bit Intel support

I noticed that the KE95 summer projects, 12/2010 – 2/2011 was about porting seL4 to 64-bit Intel.

http://ertos.nicta.com/education/summer.pml

I'm filing this issue to get some documentation/feedback on what happened and possibly feasability or plans for this.

x86: boot hangs due to unstable serial-console output

On our test machine, nightly tests are unstable since we connected a custom USB-HID test device that acts rather dynamically with periodic connect-disconnect cycles. The symptom is that the kernel boot just hangs during PCI scan. I traced this down to console_putchar() in src/plat/pc99/machine/io.c which produces the hang by not returning, and for me the following code looked suspicious

while (!(in8(port + 5) & 0x60));

The implementation checks if the THRE 0x20 or TEMT 0x40 flag was set in the UART. If I remove TEMT from the check all tests work as expected. Also, most other UART drivers I know of just check for THRE as the flag is defined as the UART is ready to accept a new character for transmission (from http://archive.pcjs.org/pubs/pc/datasheets/8250A-UART.pdf).

Makefile PATH append doesn't tolerate spaces in paths

The Makefile tries to add the tools directory to the path, but doesn't properly quote in the case that the original PATH has spaces in it. Fixed by quoting the variable assignment as follows:

diff --git a/Makefile b/Makefile
index 2ab6292..737edfa 100644
--- a/Makefile
+++ b/Makefile
@@ -158,7 +158,7 @@ default: all
 ### Tool setup
 ############################################################

-PATH := ${SOURCE_ROOT}/tools:${PATH}
+PATH := "${SOURCE_ROOT}/tools:${PATH}"
 export PATH

 PARSER = c-parser

typo?

seL4/Makefile

Line 295 in c5184b8

DEFINE += -DCONFIG_PRINTING

x86: add support for position independent syscall bindings

Required if one wants to use the bindings with shared libraries as done on Genode/seL4.

syscall_stub_gen.py ... --word-size 32 ... invocation fails

python sel4/libsel4/tools/syscall_stub_gen.py --buffer -a ia32 --word-size 32 -o ...

Traceback (most recent call last):
  File ".../libsel4/tools/syscall_stub_gen.py", line 821, in <module>
    sys.exit(main())
  File ".../libsel4/tools/syscall_stub_gen.py", line 817, in main
    generate_stub_file(args.arch, wordsize, args.files, args.output, args.buffer)
  File ".../libsel4/tools/syscall_stub_gen.py", line 725, in generate_stub_file
    result.append("assert_size_correct(%s, %d);" % (x.name, x.native_size_bits / 8))
TypeError: unsupported operand type(s) for /: 'str' and 'int'

x86 UEFI support by using Multiboot2 with GRUB2

seL4_NBSend should provide indication that something was sent.

There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place.

compile and link error for imx6 when benchmark interface is enabled

ARCH=arm PLAT=imx6 CPU=cortex-a9 ARMV=armv7-a DEBUG=1 make

--- a/configs/imx6/autoconf.h
+++ b/configs/imx6/autoconf.h
@@ -41,6 +41,7 @@
 #define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1
 #define CONFIG_LIB_SEL4_UTILS 1
 #define CONFIG_LIB_SEL4_VSPACE 1
+#define CONFIG_PRINTING 1
 #define CONFIG_LIB_PLATSUPPORT 1
 #define CONFIG_LIB_SEL4_ALLOCMAN 1
 #define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1
@@ -71,14 +72,14 @@
 #define CONFIG_HAVE_LIB_SEL4_SIMPLE 1
 #define CONFIG_ARCH_ARM 1
 #define CONFIG_HAVE_LIB_ELF 1
-#define CONFIG_PLAT_SABRE 1
+#define CONFIG_PLAT_WANDQ 1
 #define CONFIG_HAVE_LIB_PLATSUPPORT 1
 #define CONFIG_NUM_DOMAINS 16
 #define CONFIG_HAVE_LIB_UTILS 1
 #define CONFIG_USER_OPTIMISATION_O2 1
 #define CONFIG_LIB_CPIO 1
 #define CONFIG_RETYPE_FAN_OUT_LIMIT 256
-#define CONFIG_ROOT_CNODE_SIZE_BITS 12
+#define CONFIG_ROOT_CNODE_SIZE_BITS 14
 #define CONFIG_NUM_PRIORITIES 256
 #define CONFIG_TESTPRINTER_REGEX ".*"
 #define CONFIG_APP_SEL4TEST 1
@@ -93,3 +94,5 @@
 #define CONFIG_BUILDSYS_USE_CCACHE 1
 #define CONFIG_MAX_NUM_NODES 1
 #define CONFIG_KERNEL_STACK_BITS 12
+#define CONFIG_ENABLE_BENCHMARKS 1
+#define CONFIG_BENCHMARK_TRACK_UTILISATION 1

leads to:

 [CC] kernel_final.s
In file included from ./include/plat/imx6/plat/machine/hardware.h:19:0,
                 from ./include/arch/arm/arch/32/mode/machine.h:19,
                 from ./include/machine.h:17,
                 from ./include/api/syscall.h:14,
                 from src/api/faults.c:16:
./include/arch/arm/arch/benchmark_overflowHandler.h: In function ‘handleOverflowIRQ’:
./include/arch/arm/arch/benchmark_overflowHandler.h:31:9: error: implicit declaration of function ‘armv_handleOverflowIRQ’ [-Werror=implicit-function-declaration]
         armv_handleOverflowIRQ();
         ^~~~~~~~~~~~~~~~~~~~~~
./include/arch/arm/arch/benchmark_overflowHandler.h:31:9: error: nested extern declaration of ‘armv_handleOverflowIRQ’ [-Werror=nested-externs]
cc1: all warnings being treated as errors
Makefile:626: recipe for target 'kernel_final.s' failed
make: *** [kernel_final.s] Error 1

Guarding benchmark_overflowHandler.h with a #ifdef leads to following link error:

 [LD] kernel.elf
kernel.o: In function `benchmark_arch_utilisation_reset':
sel4.git/./include/arch/arm/armv/armv7-a/armv/benchmark.h:20: undefined reference to `ccnt_num_overflows'
sel4.git/./include/arch/arm/armv/armv7-a/armv/benchmark.h:20: undefined reference to `ccnt_num_overflows'
collect2: error: ld returned 1 exit status
Makefile:643: recipe for target 'kernel.elf' failed

Spectre variant 1 mitigation

This is a feature request for mitigating against Spectre variant 1 attacks.

master branch does not compile with fastpath disabled and hypervisor enabled on ARM

Compiling the seL4 kernel on ARM with hypervisor support and fastpath disabled produces a linker error about the function slowpath missing. The definition of this function is guarded by an #ifdef FASTPATH:

https://github.com/seL4/seL4/blob/master/src/arch/arm/32/hyp_traps.S#L286

If I move it out of the #ifdef block, everything compiles and links.

benchmark: support reading out idle cpu time on remote cpu

NX / XD on x86_64

Am I on the right track here?

Support passing multiboot modules and command line to rootserver

Container on Sel4

Hello

I installed sel4 on ubuntu o.s. Now I want to install container engine(Docker/kubernetes) on the top of Sel4 microkernel.
Can anyone please help me with the steps.

Thanks.

Drilling down on that mystery async abort

Further to #33, I decided to do a bit of digging to see if I could figure out where that async abort was coming from.

Let's start with the some details:

• element14 i.MX6Q hardware
• U-Boot 2016.03-20505-g7e2d42d (latest Boundary Devices version, but the same happens with u-boot master)
• Current sel4test master, kernel b25b826 and elfloader seL4/seL4_tools@79251ae

And to recap, here's the async abort on return to user space (c.f. sel4test-driver's virt_entry) I'm seeing with an unmodified debug build:

=> fatload mmc 1:1 $loadaddr sel4test-driver-image-arm-imx6 && bootelf $loadaddr
reading sel4test-driver-image-arm-imx6
3065572 bytes read in 165 ms (17.7 MiB/s)
## Starting application at 0x20000100 ...

ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10
  paddr=[20000100..202f041f]
ELF-loading image 'kernel'
  paddr=[10000000..10037fff]
  vaddr=[e0000000..e0037fff]
  virt_entry=e0000000
ELF-loading image 'sel4test-driver'
  paddr=[10038000..103fafff]
  vaddr=[10000..3d2fff]
  virt_entry=1de7c
Enabling MMU and paging
Jumping to kernel-image entry point...

DIDRv: 3, armv 70, coproc baseline only? no.
CPU is in secure mode. Enabling debugging in secure user mode.
Bootstrapping kernel
Caught cap fault in send phase at address 0x0
while trying to handle:
vm fault on data at address 0x7b63f3a2 with status 0x1c06
in thread 0xffdfad00 "rootserver" at address 0x1de7c

Okay, so let's turn on async aborts everywhere and see what blows up. Step 1: Add cpsie a to the kernel's _start and see what happens:

Bootstrapping kernel

KERNEL DATA ABORT!
Faulting instruction: 0xe0000338
FAR: 0xeb25bbaa DFSR: 0x1c06
halting...

Nice! Working backwards just to make sure the abort didn't exist earlier in the boot chain, I also initialised CPSR and turned on async abort interrupts in elfloader's _start. Same error. Nice!

What's the faulting instruction?

e0000300 <initL2Cache>:
e0000300:       e30330ff        movw    r3, #12543      ; 0x30ff
e0000304:       e3a00000        mov     r0, #0
e0000308:       e34f3ff0        movt    r3, #65520      ; 0xfff0
e000030c:       e52de004        push    {lr}            ; (str lr, [sp, #-4]!)
e0000310:       e1a02003        mov     r2, r3
e0000314:       e3001121        movw    r1, #289        ; 0x121
e0000318:       e3430c07        movt    r0, #15367      ; 0x3c07
e000031c:       e3a0e203        mov     lr, #805306368  ; 0x30000000
e0000320:       e30fcfff        movw    ip, #65535      ; 0xffff
e0000324:       e5830005        str     r0, [r3, #5]
e0000328:       e5831009        str     r1, [r3, #9]
e000032c:       e583100d        str     r1, [r3, #13]
e0000330:       e583ee61        str     lr, [r3, #3681] ; 0xe61
e0000334:       e583c67d        str     ip, [r3, #1661] ; 0x67d
e0000338:       e592367d        ldr     r3, [r2, #1661] ; 0x67d      /* !!! */
e000033c:       e6ff3073        uxth    r3, r3
e0000340:       e3530000        cmp     r3, #0
e0000344:       1afffffb        bne     e0000338 <initL2Cache+0x38>
...

Fine, I'll be a jerk about it and disable the L2 cache. On the off chance it doesn't blow up elsewhere, we'll have narrowed things down at least.

Lo and behold!

Bootstrapping kernel

... 8< ... lots of test output ... 8< ...

218/222 tests passed.
*** FAILURES DETECTED ***

Looks like the imx6 platform doesn't have its own initL2Cache function, so I'll have to start digging into src/arch/arm/machine/l2c_310.c. (So far I'm a wee bit flummoxed by the difference between what's in kernel_final.c versus kernel_final.s.)

Given it's an async/imprecise abort, it's not necessarily that instruction that caused the problem, but at least we know something's going awry with the L2 cache. I might see what happens if I tell u-boot not to initialise or use it…

Missing header in tk1 hardware.h

When compiling seL4 for the TK1 with profiling turned on, I get the following error:

/home/ajgacek/phase3-workspace/camkes/kernel/include/plat/tk1/plat/machine/hardware.h:157:9: error: implicit declaration of function 'handleOverflowIRQ' [-Werror=implicit-function-declaration]
         handleOverflowIRQ();

I think that hardware.h file is missing

#include <arch/benchmark_overflowHandler.h>

Compiler error: seL4_Fault_VGICMaintenance_IDX undeclared

I get a compiler error when I try to compile seL4 as a hypervisor. The error message is:

 [CC] src/sel4_bootinfo.o
In file included from /home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/faults.h:16:0,
                 from /home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/sel4.h:25,
                 from /home/ajgacek/phase3-workspace/next-phase3/libs/libsel4/src/sel4_bootinfo.c:11:
/home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/sel4_arch/faults.h: In function 'seL4_getArchFault':
/home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/sel4_arch/faults.h:50:58: error: 'seL4_Fault_VGICMaintenance_IDX' undeclared (first use in this function)
         return seL4_Fault_VGICMaintenance_new(seL4_GetMR(seL4_Fault_VGICMaintenance_IDX));
                                                          ^
/home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/sel4_arch/faults.h:50:58: note: each undeclared identifier is reported only once for each function it appears in
/home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/sel4_arch/faults.h:52:52: error: 'seL4_Fault_VCPUFault_HSR' undeclared (first use in this function)
         return seL4_Fault_VCPUFault_new(seL4_GetMR(seL4_Fault_VCPUFault_HSR));
                                                    ^
/home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/common/common.mk:254: recipe for target 'src/sel4_bootinfo.o' failed
make[1]: *** [src/sel4_bootinfo.o] Error 1
tools/common/project.mk:306: recipe for target 'libsel4' failed
make: *** [libsel4] Error 2

The error seems to stem from commit b827ad3. See also https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/faults.h#L50.

Idle thread runs with async aborts enabled

The idle thread uses the hard-coded CPSR value PMODE_IDLE, which does not mask FIQs or async aborts. If an async abort is pending, the kernel will fault as soon as the system becomes idle.

I see this fault happening on i.MX6Q, presumably triggered by a bad device register access in either the loader or the kernel's serial or timer drivers. Depending on the platform it may also be possible to deliberately trigger it from a user thread that has device registers mapped.

This was fixed before by commit a5f61c7, but it looks like the fix was lost in a merge with the hyp support branch. Also, the CPSR_IDLETHREAD value added by that commit has not been updated for hyp; it should use PMODE_IDLE instead of PMODE_SYSTEM.

Bug in invocation_header_gen.py on ia32?

In file tool/invocation_header_gen.py, around line 80:

enum sel4_arch_invocation_label {
    {{for label, condition in invocations}}
    ...
    {{label}} = nInvocationLabels,
    ...
    {{endfor}}
    nSeL4ArchInvocationLabels
}

On ia32, becasue seL4_arch_invocations is an empty list, this will cause nSeL4ArchInvocationLabels to be declared as 0, rather than nInvocationLabels as intented.

kernel/boot.c nitpick

in allocate_bi_frame():

    /* create the bootinfo frame object */
    pptr = alloc_region(BI_FRAME_SIZE_BITS); <--allocated BI_FRAME_SIZE_BITS
    if (!pptr) {
        printf("Kernel init failed: could not allocate bootinfo frame\n");
        return 0;
    }
    clearMemory((void*)pptr, PAGE_BITS); <-- clear PAGE_BITS

It allocates one size, but clears another. Per chance they are the same so the whole thing didn't blow up.

Update roadmap

The roadmap is out of date — for example, it lists tasks as “to-do” with expected completion dates in the past. This is a feature request that the roadmap be updated to reflect the current situation.

Serial output on x86 version 3.1.0

I compiled the sel4 3.1.0 kernel [0]

make ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 DEBUG=y

and started afterwards it by

qemu-system-i386 -kernel kernel.elf -serial stdio

but get no output at all.

Doing the same with sel4 2.1.0 [1] and 3.0.1 leads to some kernel messages.

Also on native x86 hardware I get on 2.1.0 and 3.0.1 output, but nothing for the
3.1.0 kernel. Also tried with recent git master [2].

Additionally I git bisected between 3.0.1 and 3.1.0 and beginning with commit 541289a there is no output anymore.

[0] git 8150e91
[1] git 0115ad1
[2] git 13709e5

error: Cannot fetch picotcp.git (GitError: picotcp.git update-ref: fatal: 7f12f2949f44b1de04e9d89407642a9efee878c6^0: not a valid SHA1 )

Hi,
When running repo sync command this error will occured.
Can anyone help me?

lex.py broken with recent changes

This line https://github.com/seL4/seL4/blob/master/tools/lex.py#L46 causes this error:

# make
[KERNEL]
 [MKDIR] arch/object
 [PBF_GEN] arch/object/structures.pbf
 [PBF_GEN] plat/32/plat_mode/machine/hardware.pbf
 [PBF_GEN] 32/mode/api/shared_types.pbf
 [BF_GEN] arch/object/structures_gen.h
Traceback (most recent call last):
  File "/home/podhrad/Workspace/sel4/test_default/kernel/tools/bitfield_gen.py", line 29, in <module>
    import lex
  File "/home/podhrad/Workspace/sel4/test_default/kernel/tools/lex.py", line 46, in <module>
    from past.builtins import cmp
ImportError: No module named past.builtins
/home/podhrad/Workspace/sel4/test_default/kernel/Makefile:699: recipe for target 'arch/object/structures_gen.h' failed
make[1]: *** [arch/object/structures_gen.h] Error 1
tools/common/project.mk:258: recipe for target 'kernel_elf' failed
make: *** [kernel_elf] Error 2

After commenting out line 46 compilation works as before.

Thread code nitpick

src/kernel/thread.c:125:13: error: logical not is only applied to the left hand side of this comparison [-Werror,-Wlogical-not-parentheses]
    if ((!!(!seL4_Fault_get_seL4_FaultType(sender->tcbFault) != seL4_Fault_NullFault))) {

I think there's a mess with ! usage here.

x86: support to read out serial i/o ports from BIOS data area

On Genode/x86 we use for all of our 7 supported x86 micokernels the BIOS data area to read out the serial configuration. This eliminates for us the need to manually finding out the I/O ports, which is especially handy on native machines you don't have next to you. Also the support of external users becomes comfortable since most the time the serial output 'just' works. We combine this mechanism with a small chained bootloader like bender [0, 1] that scans for PCI serial cards or/and Intel AMT SerialOverLine, writes it to the BIOS data area and then starts the actual microkernel.

What is your opinion about adding this BDA feature to seL4 in general ?

alex-ab/genode@4c1fe8b depicts the required changes, we currently apply manually to our Genode/seL4 version. (I decided for now to add extra cmdline options, which however are not strictly necessary for us.)

[0] genodelabs/genode#768
[1] genodelabs/genode#1625

Page fault on x86 kernel initialization with 2.1.0

We have experimental support for seL4 as platform for Genode and updated to 2.1.0 recently. Since then we've got strange page faults in src/arch/x86/kernel/apic.c.

========== KERNEL EXCEPTION ==========
Vector:  0xe
ErrCode: 0x0
IP:      0x100335
SP:      0xe0100de4
FLAGS:   0x96
CR0:     0x8000003b
CR2:     0x100335 (page-fault address)
CR3:     0x13a000 (page-directory physical address)
CR4:     0x290

Stack Dump:
*0xe0100de4 == 0xe0103097
...

From my investigation, this is caused by the call to pit_init() which is marked PHYS_CODE, but the calling function apic_measure_freq() is marked BOOT_CODE since 64aed53. Do we miss some detail when building seL4 for Genode?

"No user images loaded! abort() called."

Hi,
I want to boot seL4 test on imx6q-sabrelite and I do as https://docs.sel4.systems/Testing.html. Now there is a problem for me like that:

Do you have any ideas?
Thank you !

Compile error: array

vspace.c: In function init_boot_pd
vspace.c:58:23error: array subscript is above array bound ....

Tried using the flag, and can recreate this on multiple machines

Feature request: epoll-like event polling system

This is a feature request for an epoll-like polling system that allows one thread to wait on a message to be sent to any of N different endpoints/notifications, using at most O(log N) time per receive. Currently, this can be emulated with threads, but threads are relatively expensive, while my hope is that this would not be.

reserved identifier violation

I would like to point out that identifiers like "__API_H" and "__MACHINE_H" do not fit to the expected naming convention of the C language standard.
Would you like to adjust your selection for unique names?

Banked registers are not available with this architecture

I am compiling seL4 for the ARM, Exynos5410 (Odroid-XU, ARMv7a, Coretx A15) with hypervisor support and it fails with the following messages:

 [AS] kernel.o
kernel_final.s: Assembler messages:
kernel_final.s:522: Error: Banked registers are not available with this architecture. -- `msr sp_usr,lr'
kernel_final.s:524: Error: Banked registers are not available with this architecture. -- `msr elr_hyp,lr'
kernel_final.s:526: Error: Banked registers are not available with this architecture. -- `msr spsr_hyp,lr'
kernel_final.s:528: Error: selected processor does not support ARM mode `eret'
kernel_final.s:66215: Error: Banked registers are not available with this architecture. -- `msr sp_usr,lr'
kernel_final.s:66217: Error: Banked registers are not available with this architecture. -- `msr elr_hyp,lr'
kernel_final.s:66219: Error: Banked registers are not available with this architecture. -- `msr spsr_hyp,lr'
kernel_final.s:66221: Error: selected processor does not support ARM mode `eret'
kernel_final.s:67378: Error: Banked registers are not available with this architecture. -- `msr sp_usr,lr'
kernel_final.s:67380: Error: Banked registers are not available with this architecture. -- `msr elr_hyp,lr'
kernel_final.s:67382: Error: Banked registers are not available with this architecture. -- `msr spsr_hyp,lr'
kernel_final.s:67384: Error: selected processor does not support ARM mode `eret'
make[1]: *** [kernel.o] Error 1
make: *** [kernel_elf] Error 2

Can seL4 work on hikey platform?

Does it work at a32 mode? And which compiler fit for it? I would be very appreciate if someone could give me some detailed information.

Installation

Hii
Can anyone please help me how to install sel4 on top of ubuntu?
Like the instructions for installation

Thanks

Cannot run x64 image with Qemu

After reading the Qemu tutorial on seL4 wiki, I can run 32-bit version smoothly with following scripts

make clean
make optiplex9020_defconfig
make silentoldconfig
make
cd images
qemu-system-x86_64  -m 512  -kernel kernel-ia32-pc99 -initrd capdl-loader-experimental-image-ia32-pc99 --enable-kvm  -smp 2 -cpu Nehalem,+vmx -nographic

However, I cannot run 64-bit version with error fsgsbase instructions not supported by the processor reported using almost the same scripts except x86_64 parameters.

......
make x64_optiplex9020_defconfig # x64
......
sudo qemu-system-x86_64  -m 512  -kernel kernel-x86_64-pc99 -initrd capdl-loader-experimental-image-x86_64-pc99 --enable-kvm  -smp 2 -cpu Nehalem,+vmx -nographic #x86_64

My CPU is i7 6700 (Skylake) and FSGSBASE is enabled (checked by lscpu | grep fsgsbase).
Can anyone help me, please?

Shebang in Python files should use python2.7

When trying to build seL4 on distros where Python 3 is the default python (such as Arch), the build fails when running python files as they are are python2 code, instead of python3.

The shebang should be:

#!/usr/bin/env python2.7

CPU grinding on TEST_FPU0001

When testing x86_64 debug builds under hardware virtualisation (KVM rather than QEMU's TCG), the suite succeeds up to TEST_FPU0001, then grinds the CPU at 100%. This happens with the default FXSAVE, XSAVEOPT, a non-simulation build, etc.

Any thoughts as to what might be causing it, how I should approach debugging it, etc.?

Starting test 19: TEST_FPU0000
  TEST_FPU0000
Running test FPU0000 (Ensure that simple FPU operations work)
Test FPU0000 passed
Starting test 20: TEST_FPU0001
  TEST_FPU0001
Running test FPU0001 (Ensure multiple threads can use FPU simultaneously)

(I filed this here because it makes more sense to me that this would be an issue with the kernel than the test suite, but I could very well be wrong!)

x86 asm no rule to make.

make: *** No rule to make target src/arch/x86/machine_asm.S', needed bysrc/arch/x86/machine_asm.s'.

Can the seL4 be compiled in thumb mode?

Can the seL4 be compiled in thumb mode?

Real performance comparisons

I imagine this isn't the right place for this, but i can't find a better one.

I see the performance comparisons at http://l4hq.org/docs/performance.php are run on all different processors. In its current form, the performance numbers here are completely useless. It would be very informative to have real performance benchmarks where the exact same processor is used for every OS in comparison. Otherwise, what am I supposed to do with those number?

Protect cross-userspace Spectre attacks (both variant 1 and 2)

Userspace processes need to be protected against Spectre attacks by other such processes. While the seL4 security claim does not extend to covert channels, timing attacks are a significant threat when untrusted code and trusted code are running on the same system.

Domains, while awesome for high-integrity software development where all trusted code is known a priori, do not suffice for this use case, because they are too strict: the number of domains, and the fraction of the CPU allocated to each, must be set at compile time (at least if I am reading the documentation correctly). As such, e.g. a version of QubesOS on seL4 would not be able to use them.

This issue also applies regarding cross-VM, VM→user, and user→VM attacks.

arm926ej_s is not officially supported

At present, Kconfig contains the entries about arm926ej_s and IntegratorCP:

        config ARM926EJ_S
            bool "ARM926EJ-S"
            depends on ARCH_ARM
            select ARCH_ARM_V5
            help
                Support for ARM926EJ_S

However, there is no architecture support for armv5/arm926ej_s. Would it be better if the related configuration entries are removed?

asid_map may not get initialized when CONFIG_VTX is not set

Compilation error generated by clang:
~/seL4test/kernel/src/arch/x86/64/kernel/vspace.c:786:9: error: variable 'asid_map' is used uninitialized whenever 'if' condition is false [-Werror,-Wsometimes-uninitialized]
if (cap_get_capType(vspaceCapSlot->cap) == cap_pml4_cap) {
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~/seL4test/kernel/src/arch/x86/64/kernel/vspace.c:798:59: note: uninitialized use occurs here
poolPtr->array[asid & ((1ul << (asidLowBits))-1ul)] = asid_map;
^~~~~~~~
~/seL4test/kernel/src/arch/x86/64/kernel/vspace.c:786:5: note: remove the 'if' if its condition is always true
if (cap_get_capType(vspaceCapSlot->cap) == cap_pml4_cap) {
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~/seL4test/kernel/src/arch/x86/64/kernel/vspace.c:785:5: note: variable 'asid_map' is declared here
asid_map_t asid_map;
^

Problematic code from ~/seL4test/kernel/src/arch/x86/64/kernel/vspace.c:
exception_t
performASIDPoolInvocation(asid_t asid, asid_pool_t *poolPtr, cte_t *vspaceCapSlot)
{
asid_map_t asid_map;
if (cap_get_capType(vspaceCapSlot->cap) == cap_pml4_cap) {
cap_pml4_cap_ptr_set_capPML4MappedASID(&vspaceCapSlot->cap, asid);
cap_pml4_cap_ptr_set_capPML4IsMapped(&vspaceCapSlot->cap, 1);
asid_map = asid_map_asid_map_vspace_new(cap_pml4_cap_get_capPML4BasePtr(vspaceCapSlot->cap));
} else {
#ifdef CONFIG_VTX
assert(cap_get_capType(vspaceCapSlot->cap) == cap_ept_pml4_cap);
cap_ept_pml4_cap_ptr_set_capPML4MappedASID(&vspaceCapSlot->cap, asid);
cap_ept_pml4_cap_ptr_set_capPML4IsMapped(&vspaceCapSlot->cap, 1);
asid_map = asid_map_asid_map_ept_new(cap_ept_pml4_cap_get_capPML4BasePtr(vspaceCapSlot->cap));
#endif
}
poolPtr->array[asid & MASK(asidLowBits)] = asid_map;
return EXCEPTION_NONE;
}

Manual: VM Fault section

Hello,
it would be great if the section on VM faults could be extended, I can say nothing regarding ARM but for IA32 the following changes would be great:
Change the ARMish term 'FSR' to the more x86ish 'Page-Fault Error Code'.
When describing the contents of IPCBuffer[3] state that it is a exact copy of the Page-Fault Error Code which the CPU produces on a page fault. A reference to the following would be great (https://www-ssl.intel.com/content/dam/www/public/us/en/documents/manuals/64-ia-32-architectures-software-developer-system-programming-manual-325384.pdf, p. 135-137). This part of the intel manual describes this value in full detail.

Dead links in README.md

Nothing major -- links 2, 3 reference dead pages on the sel4.systems website, and link 5 is actually a redirect.

For your convenience here's a patch to correct the links.

Patch: https://github.com/watbe/seL4/commit/74276ce9ccd7489a06bc8cfd90aa0fc4a3d429cc.patch