September 2018 - Devel - lists.sel4.systems

x86 seL4 kernel bug - kernel page faults on seL4_VMEnter
by Alexander Boettcher 26 Sep '18

26 Sep '18

Hello, during some experimental work on Genode/seL4 and VM extensions, I encountered the issue to trigger a kernel fault. The symptom seems, that if a thread invokes seL4_VMEnter, but the actual thread is not meant/supposed to run a VM, the kernel will (ever?/may?) page fault with a nullpointer access - which effectively renders the whole Genode system unusable. A partial log is attached based on Genode on x86_64 with seL4 kernel version 9.0.1. The fault address points to [0], where the variable _expected_vmcs_ is null and the kernel de-references it. I put a message before this line and print the value of the variable (as visible in the log below). The seL4 10.0.0 code looks similar, so I presume the same issue there . (if the code is not verified - which according to the roadmap is not the case [1] ?) Cheers, Alex B. [0] https://github.com/seL4/seL4/blob/0dd40b6c43a290173ea7782b97afbbbddfa23b36/… [1] https://sel4.systems/Info/Roadmap/home.pml -- Alexander Boettcher Genode Labs https://www.genode-labs.com - https://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth diff --git a/src/arch/x86/object/vcpu.c b/src/arch/x86/object/vcpu.c index cf74fa4..68a1dca 100644 --- a/src/arch/x86/object/vcpu.c +++ b/src/arch/x86/object/vcpu.c @@ -1540,6 +1540,7 @@ restoreVMCS(void) } #ifndef CONFIG_KERNEL_SKIM_WINDOW + userError("opps expected_vmcs=%p", expected_vmcs); if (getCurrentCR3().words[0] != expected_vmcs->last_host_cr3) { expected_vmcs->last_host_cr3 = getCurrentCR3().words[0]; vmwrite(VMX_HOST_CR3, getCurrentCR3().words[0]); Boot config: parsing cmdline '/boot/sel4 disable_iommu' Boot config: console_port = 0x1808 Boot config: debug_port = 0x1808 Boot config: disable_iommu = true Detected 1 boot module(s): module #0: start=0xfd58000 end=0xffff330 size=0x2a7330 name='/boot/image.elf' Parsing GRUB physical memory map Physical Memory Region from 0 size 89400 type 1 Physical Memory Region from 89400 size 16c00 type 2 Physical Memory Region from d2000 size 2000 type 2 Physical Memory Region from dc000 size 24000 type 2 Physical Memory Region from 100000 size bb17c000 type 1 Adding physical memory region 0x100000-0xbb27c000 Physical Memory Region from bb27c000 size 6000 type 2 Physical Memory Region from bb282000 size dd000 type 1 Adding physical memory region 0xbb282000-0xbb35f000 Physical Memory Region from bb35f000 size 12000 type 2 Physical Memory Region from bb371000 size 81000 type 4 Physical Memory Region from bb3f2000 size 1d000 type 2 Physical Memory Region from bb40f000 size 60000 type 1 Adding physical memory region 0xbb40f000-0xbb46f000 Physical Memory Region from bb46f000 size 1f9000 type 2 Physical Memory Region from bb668000 size 80000 type 4 Physical Memory Region from bb6e8000 size 27000 type 2 Physical Memory Region from bb70f000 size 8000 type 1 Adding physical memory region 0xbb70f000-0xbb717000 Physical Memory Region from bb717000 size 8000 type 2 Physical Memory Region from bb71f000 size 4c000 type 1 Adding physical memory region 0xbb71f000-0xbb76b000 Physical Memory Region from bb76b000 size c000 type 4 Physical Memory Region from bb777000 size 3000 type 3 Physical Memory Region from bb77a000 size 7000 type 4 Physical Memory Region from bb781000 size 1000 type 3 Physical Memory Region from bb782000 size 9000 type 4 Physical Memory Region from bb78b000 size 1000 type 3 Physical Memory Region from bb78c000 size 13000 type 4 Physical Memory Region from bb79f000 size 60000 type 3 Physical Memory Region from bb7ff000 size 1000 type 1 Adding physical memory region 0xbb7ff000-0xbb800000 Physical Memory Region from bb800000 size 800000 type 2 Physical Memory Region from bc000000 size 4000000 type 2 Physical Memory Region from e0000000 size 10000000 type 2 Physical Memory Region from feaff000 size 1000 type 2 Physical Memory Region from fec00000 size 10000 type 2 Physical Memory Region from fed00000 size 400 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from fed20000 size 70000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from ff000000 size 1000000 type 2 Physical Memory Region from 100000000 size 38000000 type 1 Adding physical memory region 0x100000000-0x138000000 Multiboot gave us no video information ACPI: RSDP paddr=0xf68e0 ACPI: RSDP vaddr=0xf68e0 ACPI: RSDT paddr=0xbb7f07a2 ACPI: RSDT vaddr=0xbb7f07a2 ***WARNING*** SKIM window not enabled, this machine is probably vulernable to Meltdown (https://www.meltdownattack.com) consider enabling Kernel loaded to: start=0x200000 end=0xaa5000 size=0x8a5000 entry=0x201209 ACPI: RSDT paddr=0xbb7f07a2 ACPI: RSDT vaddr=0xbb7f07a2 ACPI: FADT paddr=0xbb7f0a00 ACPI: FADT vaddr=0xbb7f0a00 ACPI: FADT flags=0xc2ad ACPI: MADT paddr=0xbb7feb45 ACPI: MADT vaddr=0xbb7feb45 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x1 ACPI: MADT_APIC apic_id=0x4 ACPI: MADT_APIC apic_id=0x5 ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: 4 CPU(s) detected ELF-loading userland images from boot modules: size=0x110f000 v_entry=0x2000018 v_start=0x2000000 v_end=0x310f000 p_start=0x10000000 p_end=0x1110f000 Moving loaded userland images to final location: from=0x10000000 to=0xaa5000 size=0x110f000 Starting node #0 with APIC ID 0 Mapping kernel window is done Starting node #1 with APIC ID 1 Starting node #2 with APIC ID 4 Starting node #3 with APIC ID 5 Booting all finished, dropped to user space virtual address layout of core: overall [0000000000002000,00000000c0000000) core image [0000000002000000,000000000310f000) ipc buffer [000000000310f000,0000000003110000) boot_info [0000000003110000,0000000003112000) stack area [0000000040000000,0000000050000000) boot module 'timer' (113344 bytes) boot module 'test-vmm_sel4' (9912 bytes) boot module 'config' (609 bytes) boot module 'ld.lib.so' (937616 bytes) boot module 'init' (352672 bytes) Genode sculpt_vc-2-ge2fd5e5 2909 MiB RAM and 261141 caps assigned to init ... <<seL4(CPU 0) [restoreVMCS/1543 T0xffffff80ba295400 "child of: 'child of: 'rootserver''" @10000c9]: opps _expected_vmcs_=(nil)>> ========== KERNEL EXCEPTION ========== Vector: 0xe ErrCode: 0x0 IP: 0xffffffff80835236 SP: 0xffffffff8087ef18 FLAGS: 0x10086 CR0: 0x8001003b CR2: 0x3298 (page-fault address) CR3: 0xba043000 (page-directory physical address) CR4: 0x6620 Stack Dump: *0xffffffff8087ef18 == 0x10000c9 *0xffffffff8087ef20 == 0xffffffff80a93000 *0xffffffff8087ef28 == 0xffffffff80890040 *0xffffffff8087ef30 == 0x40 *0xffffffff8087ef38 == 0xffffff80ba295400 *0xffffffff8087ef40 == 0xffffffff8087efb8 *0xffffffff8087ef48 == 0xffffffffffffffe7 *0xffffffff8087ef50 == 0xffffffff80a93000 *0xffffffff8087ef58 == 0xffffffff80a93000 *0xffffffff8087ef60 == 0x0 *0xffffffff8087ef68 == 0x0 *0xffffffff8087ef70 == 0xffffffff80890040 *0xffffffff8087ef78 == 0xffffffffffffffff *0xffffffff8087ef80 == 0xffffffff808357fe *0xffffffff8087ef88 == 0xffffffff80a93000 *0xffffffff8087ef90 == 0xffffffff80838c93 *0xffffffff8087ef98 == 0x1001d4 *0xffffffff8087efa0 == 0x0 *0xffffffff8087efa8 == 0xffffffffffffffe7 *0xffffffff8087efb0 == 0xffffffff80839982 Halting... halting... Kernel entry via Interrupt, irq 157

2 2

create a new thread in sel4
by Dongxu Ji 25 Sep '18

25 Sep '18

Hello, My platform is imx6q sabrelite and I have run sel4-test successfully. Now I'm trying to create a new thread in the initial thread according to sel4 tutorial2. But it didn't run. The code is shown below: struct driver_env env; allocman_t *allocman; /* function to run in the new thread */ void thread_2(void) { printf("thread_2: hallo wereld\n"); while (1); } int main(void) { int error; reservation_t virtual_reservation; seL4_BootInfo *info = platsupport_get_bootinfo(); seL4_DebugNameThread(seL4_CapInitThreadTCB, "sel4test-driver"); /* initialise libsel4simple */ simple_default_init_bootinfo(&env.simple, info); /* create an allocator */ allocman = bootstrap_use_current_simple(&env.simple, ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool); /* create a vka */ allocman_make_vka(&env.vka, allocman); /* create a vspace */ error = sel4utils_bootstrap_vspace_with_bootinfo_leaky(&env.vspace, &data, simple_get_pd(&env.simple), &env.vka, platsupport_get_bootinfo()); /* fill the allocator with virtual memory */ void *vaddr; virtual_reservation = vspace_reserve_range(&env.vspace, ALLOCATOR_VIRTUAL_POOL_SIZE, seL4_AllRights, 1, &vaddr); if (virtual_reservation.res == 0) { ZF_LOGF("Failed to provide virtual memory for allocator"); } bootstrap_configure_virtual_pool(allocman, vaddr, ALLOCATOR_VIRTUAL_POOL_SIZE, simple_get_pd(&env.simple)); /* Allocate slots for, and obtain the caps for, the hardware we will be * using, in the same function. */ sel4platsupport_init_default_serial_caps(&env.vka, &env.vspace, &env.simple, &env.serial_objects); vka_t serial_vka = env.vka; serial_vka.utspace_alloc_at = arch_get_serial_utspace_alloc_at(&env); /* Construct a simple wrapper for returning the I/O ports. */ simple_t serial_simple = env.simple; /* enable serial driver */ platsupport_serial_setup_simple(&env.vspace, &serial_simple, &serial_vka); simple_print(&env.simple); /* get our cspace root cnode */ seL4_CPtr cspace_cap; cspace_cap = simple_get_cnode(&env.simple); /* get our vspace root page diretory */ seL4_CPtr pd_cap; pd_cap = simple_get_pd(&env.simple); /* create a new TCB */ vka_object_t tcb_object = {0}; error = vka_alloc_tcb(&env.vka, &tcb_object); /* initialise the new TCB */ error = seL4_TCB_Configure(tcb_object.cptr, seL4_CapNull, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, 0, 0); /* give the new thread a name */ name_thread(tcb_object.cptr, "hello-2: thread_2"); UNUSED seL4_UserContext regs = {0}; /* set instruction pointer where the thread shoud start running */ sel4utils_set_instruction_pointer(&regs, (seL4_Word)thread_2); error=sel4utils_get_instruction_pointer(regs); /* check that stack is aligned correctly */ const int stack_alignment_requirement = sizeof(seL4_Word) * 2; uintptr_t thread_2_stack_top = (uintptr_t)thread_2_stack + sizeof(thread_2_stack); /* set stack pointer for the new thread */ sel4utils_set_stack_pointer(&regs, thread_2_stack_top); error=sel4utils_get_sp(regs); /* actually write the TCB registers. */ error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, &regs); /* start the new thread running */ error = seL4_TCB_Resume(tcb_object.cptr); /* we are done, say hello */ printf("main: hello world \n"); return 0; } And I can get some output: cspace_cap is 2 pd_cap is 3 tcb_object.cptr is 5f7 tcb_object.ut is 10000208 tcb_object.type is 1 tcb_object.size_bits is a regs.pc is 9640 regs.sp is 3f24f0 Any advice about the issue? Thank you, Dongxu Ji

2 2

seL4 and rump kernel synchronization primitives limitations
by Jason Wenger 20 Sep '18

20 Sep '18

I think I've uncovered an interesting problem involving IPC between rump kernels and seL4, and I'm curious if anyone has any thoughts on mitigating it. My use case is that I want a CAmkES component to be able to notify the rump component to send a network packet. However, as far as I can see: CAmkES connector, mutex, and semaphore threads that run in a rump component • can wait on their seL4 synchronization primitives • ... but they can't call rump function calls because they're not rump threads. You can try to call, becuase you're running in the same address space as the rump kernel, but if you call a rumpkernel function, the CAmkES thread crashes when it reaches curlwp() becuase the calling thread is unknown to the NetBSD kernel. Therefore you can't call sendto() inside, for example, a notification callback or an seL4RPCCall handler, unless you can work out a way to signal to the NetBSD kernel that you're calling into the kernel from a foreign thread. Is this somehow possible through use of rump_schedule() and rump_unschedule()? ... and the other possible path I can see also has problems: rumpkernel created userspace threads (pthreads) • can wait on seL4 synchronization primitives • ... but if they do wait, they also unschedule the* entire rest of the rump kernel and userspace* because every single rump thread (both kernel and user) all run in one seL4 thread. Therefore you can't do while(true) { semaphore_wait(); sendto(...); } without unscheduling the entire rump component when you hit the wait(). For this to work, there would need to be a way to have multiple seL4 threads for rump kernel execution so that one could block while the others continue. That *is* done for interrupt and timer handling, but there's no way I can see to set it up from a rump userspace program. The only other possible path appears to be busy-wait polling which is obviously very inefficient. Any thoughts? --Jason C. Wenger

2 1

genode-sel4-arm -- Genode OS with seL4 on ARM hardware
by Adam Wiethuechter 18 Sep '18

18 Sep '18

Webite -- http://genodl4arm.critical.com/ Github -- https://github.com/CriticalTechnologiesInc/genode-sel4-arm Hello everyone, I have something rather exciting to share with you all today that we here at Critical Technologies Inc (CTI) have been working on for sometime now - the marriage of Genode OS and seL4 on native ARM hardware. We currently are supporting the Wandboard Quad (from Wandboard) and the SabreLite (from Boundary Devices). We are hoping to continue development targeting ARMv8a boards of interest; mainly the Raspberry Pi 3B and/or the Xilinx Zynq UltraScale+ ZCU102. This is obviously a work in progress with only the first step but we wished to share our documentation to the community for others to contribute and see what we are doing. I am happy to answer any questions you may have. -- 73's, Adam Wiethuechter, Jr Software Engineer Critical Technologies Inc. <adam.wiethuechter(a)critical.com>

2 1

Building/Running https://github.com/SEL4PROJ/docs with docker
by Axel Heider 17 Sep '18

17 Sep '18

Hi, I'm trying to build and run https://github.com/SEL4PROJ/docs with docker. Following the instrucitons: git clone https://github.com/SEL4PROJ/docs cd docs git submodule init git submodule update docker run --network=host -v $PWD:/host -w /host -it ruby bash -c 'bundle install && bundle exec jekyll serve' things fails with: ... Bundle complete! 8 Gemfile dependencies, 29 gems now installed. Bundled gems are installed into `/usr/local/bundle` Configuration file: /host/_config.yml Source: /host Destination: /host/_site Incremental build: disabled. Enable with --incremental Generating... Liquid Exception: No such file or directory @ rb_sysopen - /host/_repos/sel4/manual/generated_markdown/GeneralSystemCalls.md in ApiDoc.md jekyll 3.6.2 | Error: No such file or directory @ rb_sysopen - /host/_repos/sel4/manual/generated_markdown/GeneralSystemCalls.md Any hint what's failing here? I don't even see a folder "_repo", but I assume the build should create one? Thanks, Axel

2 1

Getting Started
by Dave Richards 13 Sep '18

13 Sep '18

I am in the process of reading the Getting Started documentation and building a development environment on Debian Linux. I thought RefOS would be the best example project to start with. When I execute the command: repo init -u ssh://git@github.com/seL4/refos-manifest -b master I get the response: Please make sure you have the correct access rights and the repository exists. Permission denied (publickey). fatal: Could not read from remote repository. Please make sure you have the correct access rights and the repository exists. fatal: cannot obtain manifest ssh://git@github.com/seL4/refos-manifest Apparently something has changed since the instructions were written. Dave

2 1

Notion of a User in seL4
by Amit Goyal 11 Sep '18

11 Sep '18

Hi All, As far as I understand, in seL4, the notion of a subject is similar to a thread (process). Each process has a different cspace and thus has different capabilities. Correct me, if I am wrong. Currently, we can make different components say server and client which run on the same seL4 kernel. They can interact with each other by creating endpoint and adding capability for that endpoint, in others cspace. Now, I want to extend it and run client and server on different host machines which run seL4. The threads (client and server) thus generated will be different users as per the standard linux convention. a) How does the communication happen in such a scenario in seL4? The problem which I see is how the capabilities for endpoint on one machine will be minted into other machine's process cspace. b) I also want to understand the notion of a user in seL4. -- Thanks and Regards, Amit Goyal

2 1

seL4 - getting the execution time of different threads
by Mr. Peace 10 Sep '18

10 Sep '18

Hello together, I was wondering how you do get the execution time in seL4 if you are using multiple threads. In the initial thread I can use the timer as it is shown in the tutorial about timers since I do have the bootinfo, vka, allocman and so on. But how do I use the timer to measure the execution time of the other threads without stopping their execution to "pull" the time from the initial thread? Is it possible to share the timer or create new ones in the other threads? Or is there another way to measure the execution time? Some background information: The threads have different VSpace's and CSpace's. Used tutorials: seL4-tutorial 4, seL4-tutorial timer. The other threads do not have a bootinfo in their environment. Kind regards, Chris

4 5

Strange behavior when writing to memory mapped to a custom device in the VMM.
by Dan DaCosta 09 Sep '18

09 Sep '18

To Whom It May Concern: I am observing seL4+VM+ARM behavior on the TK1-SOM that I find very puzzling. Consider the following code: #define idx(i) (i%16) for(i = 0; i < buf->capacity() && buf->capacity() > 16; i++, pArray++){ mem[idx(i)] = *pArray; } where 'pArray' is the array representation of 'buf' and 'mem' is a memory mapped page set that corresponds to a page set of memory that is managed by a fault handler in the VMM (something I have installed myself using a 'DEV_CUSTOM' device). This code runs as I would expect. However, the follow code results in an assertion failure in the VMM: #define idx(i) (i%16) for(i = 0; i < 16; i++, pArray++){ mem[idx(i)] = *pArray; } The error report follows: 32 bit ARM insts not decoded -------- Pagefault from [Linux]: write fault @ PC: 0xbd7499a8 IPA: 0xe0001000, FSR: 0x2000046 Context: r0: 0xb6d2a050 r1: 0x0 r2: 0xb6ac76b8 r3: 0x4c r4: 0xb6d2a050 r5: 0xb6d2a8ec r6: 0x1 r7: 0xb6d2a050 r8: 0x7fb73000 r9: 0xad13cfff r10: 0xabe31310 r11: 0x19 r12: 0xb6d285d8 pc: 0x7f68f9a8 r14: 0x7f68f99c sp: 0xaf1c3c20 cpsr: 0x80000010 -------- Assertion failed: rt >= 0 (../projects/seL4_projects_libs/libsel4arm-vmm/src/fault.c: get_rt: 357) Some added information that may be helpful; if the strange modulo operation I am performing on the index is removed I receive a similar crash for both code snippets. Any thoughts on where I might look to get to the bottom of this problem would be helpful. Thanks! Dan DaCosta

2 1

CAmkES VMM platform support
by Grant Jurgensen 07 Sep '18

07 Sep '18

Hi all, I was hoping someone could clarify for me a couple of points regarding the CAmkES VMMs. First off, I have a program I want to run under a linux VM within CAmkES. However, it is written in a language which can be compiled to x86-64 but not IA-32. The impression I have gotten from the documentation and the examples is that the x86 CAmkES VMM only supports the 32-bit variant. Is that correct? My attempt to build the project targeting x86_64 has been met with errors (qemu complains "Huge page not supported by the processor"). Alternatively, said program can be compiled to ARMv6. In fact, the ultimate goal is for this project to run on an Odroid XU4, but as that platform is not currently supported by the CAmkES ARM VMM, I was hoping to build up the infrastructure as much as possible by testing it on any platform I could. The two platforms that are supported for the ARM VMM do not seem to have support on the qemu end though, so unfortunately I have no way of testing there either. Is it fair to assume that porting the Odroid implementation to the Odroid XU4 would be a non-trivial undertaking, or are they perhaps more similar than I am imagining? Thanks, Grant Jurgensen

2 4