- Devel - lists.sel4.systems

US Army SBIR calls for open HW/SW stack
by Gernot.Heiser＠data61.csiro.au 09 Oct '18

09 Oct '18

… and mentions seL4 prominently: https://www.sbir.gov/sbirsearch/detail/1508741

1 0

seL4 IPC fastpath question
by 송대영 08 Oct '18

08 Oct '18

Hello, I have question about seL4 IPC fastpath. I ran sel4bench on sabre lite(arm v7). 1. IPC fastpath can apply in seL4_Call and seL4_Reply_Recv, is it right? seL4_Send, seL4_Recv can't apply IPC fastpath. 2. IPC_fastpath can only send message that message's length is 0, is it right? I found these comments. /* Call slowpath, long IPC (10), same prio client to server, different address space */ /* ReplyRecv slowpath, long IPC (10), same prio server to client, on the slowpath, different address space */ 3. In seL4 IPC mechanism, IPC only use registers not memory?

3 2

Questions on CAMKES-ARM-VM Build and Components
by Daniel Wang 04 Oct '18

04 Oct '18

Hi all, It seems CAmkES-arm-vmm has been immigrated to cmake, How can I build it? I tried to build it by invoking: # ../init-build.sh -DCAMKES_VM_APP=tk1_vm -DPLATFORM=tk1 # ninja But it does not work. Also, thank for the detailed CAmkES X86 documents. I’m wondering does the VM Connector and kernel modules work for ARM architecture, TK1 or TK1-SOM specifically? Best Regards -Daniel Wang

3 6

Does seL4 provide an initrd with a shell?
by Baptiste Lepers 03 Oct '18

03 Oct '18

I have been following the instructions "Fetching, Configuring and Building seL4test" on this page https://docs.sel4.systems/GettingStarted.html. Everything seems to work, but the initrd provided only runs a bunch of tests and then exits. Is there another project that provides a shell or a way for me to launch my own programs? I have tried to follow the instructions on these pages https://docs.sel4.systems/Hardware/Qemu/ and https://docs.sel4.systems/CAmkESVM but the repo init command fails (404). Thanks, Baptiste.

3 4

Problem in Installing Genode OS
by Amit Goyal 02 Oct '18

02 Oct '18

Hi All, I tried to run Genode OS (on x86-64, i5, ubuntu 16.04) via 3 means but could not succeed. Can someone please suggest a possible way out. a) Running iso on virtual box [1] The system complete freezes and the corresponding error is: emR3Debug: rc=VERR_PGM_HANDLER_VIRTUAL_CONFLICT b) Running iso on Qemu [1] The interface appears with following options: Introduction, Web Browser, Seamless Linux, OpenGL, Qt4. but none of the options work on clicking. c) Building the kernel [2] After following all the instructions in [2] and creating the build directory, the last command <<make KERNEL=linux demo>> fails: Error: target 'demo' does not exist Makefile:211: recipe for target 'error_missing_targets' failed make: *** [error_missing_targets] Error 1 [1] https://genode.org/download/live-cds [2] https://genode.org/documentation/developer-resources/getting_started Also, can you please direct us towards any other operating system which is built using the seL4 microkernel. -- Thanks and Regards, Amit Goyal

2 1

Alignment fault without U-Boot Cache Enabled
by Nicholas Pahl 29 Sep '18

29 Sep '18

Hi All, I have noticed an alignment fault in the seL4 elfloader when running seL4 on an AArch64 platform with dcache disabled in U-Boot. The alignment fault is caused by reading the elf files header in the elfloader. The fault can be fixed (hacked) by modifying the length of the elf file name, located before the elf file header, to force a proper alignment. Is the seL4 elfloader intended to be dependent on u-boot enabling the cache?

2 1

How is undefined behavior in x86 ISA handled?
by Wean Irdeh 27 Sep '18

27 Sep '18

Hi all. I was having discussion about how secure handwritten asm code compared to C code in https://board.flatassembler.net/topic.php?p=206126#206117 and someone mentioned that there are undefined behavior in x86 instruction set How is these x86 undefined behavior handled in sel4?

2 1

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