Devel September 2018

devel@sel4.systems

26 participants
21 discussions

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

Network lwip for imx6
by wong xuguo 11 Dec '18

11 Dec '18

Hi, I am a student fron Nanjing university, a fresh man of microkernel, specially, know very little about the seL4. Recently I accept a chellange about porting the lwip to sel4, on arch of imx6, does any one could give me a clue? I found the source of camkes does have this code, could I do something to port, to make the lwip work? What my aim is make a tcp echo server. Thank you for all of you help. Best regards from Xuguo Wang

4 4

Non CAmkES VM on x86
by Chris Guikema 08 Nov '18

08 Nov '18

DornerWorks is looking at working with the CAmkES-VM. In previous work with ARM, we've only used a non-camkes VMM, since the hypervisor pieces were more important (and 64-bit ARM CAmkES hadn't been developed). Out of curiosity, has Data61 ever worked with a non-CAmkES VM on x86 similar to how the old ARM VMM worked? If so, is that something that could be released? Thanks, Chris Guikema

2 1

Passing Network Resource to Linux VM in TK1-SOM
by Daniel Wang 07 Nov '18

07 Nov '18

Hi all, I got a question, how can I pass the network communication to Linux virtual machine? Following the work of seL4-ARM-VMM with TK1-SOM board, i run seL4 as the microvisor that hosts the buildroot Linux as a user-land process, I was able to mount the MMC storage in the virtual machine, but I cannot get the NIC works. I’m wondering has anyone tried it that can give me some hint? Best Regards -Daniel Wang

2 2

run docker on sel4
by Jia He 06 Nov '18

06 Nov '18

Hi all I am new comer to sel4 community. I knew a little bit virtualisation infrastructe(kvm/qemu), but I know little about sel4/docker. I am investigating the proper implemenatation for running docker on sel4 on arm64. There might several ways I can figure out.Any suggestions are welcome :-) 1. run linux on sel4 vmm (camkes_vm) and run docker on linux. This might be the easiest way. It might have worked well on X86 2. porting l4linux to sel4. Don't know whether it is feasible? 3. run docker as sel4 service without linux. On this way, golang and its library should be ported to sel4. Some missed syscalls which are needed by docker should be implemenated. Is there any other ways or anything else to make the implatation more feasible? --- Cheers, Justin

3 2

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

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

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel September 2018