- Devel - lists.sel4.systems

Future plans w.r.t. Cortex-R
by piotr＠skrzypek.eu 10 Jul '18

10 Jul '18

Dear seL4 Maintainers, Could you please share what are your future support plans w.r.t. ARM Cortex-R family - the 'reliable' and 'real-time' side of ARM portfolio? Cortex-R implementations include interesting safety features i.a. lockstep processing. It feels like a good match for seL4 safety-oriented philosophy. However, Cortex-R processors have MPU instead of MMU, which seems to be ruling them out for now. Are there any plans to have an seL4 'MPU' branch in order to support these kind of processors? Thank you in advance, Piotr Skrzypek

3 4

Questions on U-boot Verified Boot with CAmkES-ARM-VM
by Daniel Wang 10 Jul '18

10 Jul '18

Hi all, I’m trying to test secure boot with the CAmkES-arm-vm. I found that U-boot has its implementation of secure boot called verified boot, but it seems only support FIT image format. I’m wondering is there a way to convert the final ELF image to an FIT image? I’m studying the details of different booting image format. I’m not sure how it would work with seL4 camkes demo specifically, since there are so many binary files and cpio archives packed in the final ELF image. Would love to hear your opinions. Thank you very much! Best Regards -Daniel Wang

2 1

sel4 qemu x86 runtime error
by Thad Seeberger 10 Jul '18

10 Jul '18

Compile now no problem however I'm getting error when running. I believe its an invalid opcode exception. I think my build not matching the qemu but I've tried diff machines and they do the same. I also get this warning during build, not sure if this relevant: Warning: Installation path /home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool not found on the PATH environment variable. make: Leaving directory `/home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool' Qemu commanr, lines with ????? suspect: qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 (process:98550): GLib-WARNING **: gmem.c:483: custom memory allocation vtable not supported Boot config: parsing cmdline 'images/kernel-ia32-pc99 ' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false ???? Warning: Your kernel was not compiled for the current microarchitecture. Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 1fefe000 type 1 Adding physical memory region 0x100000-0x1f800000 Physical Memory Region from 1fffe000 size 2000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Multiboot gave us no video information Kernel loaded to: start=0x100000 end=0x160000 size=0x60000 entry=0x10005e ACPI: RSDP paddr=0xf7180 ACPI: RSDP vaddr=0xdfcf7180 ACPI: RSDT paddr=0x1ffffbc1 ACPI: RSDT vaddr=0xdffffbc1 ACPI: FADT paddr=0x1ffff1c0 ACPI: FADT vaddr=0xdffff1c0 ACPI: FADT flags=0x80a5 ACPI: 0 IOMMUs detected ACPI: MADT paddr=0x1ffffb11 ACPI: MADT vaddr=0xdffffb11 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected Detected 1 IOAPICs, but configured to use PIC instead Detected 1 boot module(s): module #0: start=0x161000 end=0x25aed0 size=0xf9ed0 name='images/capdl-loader-experimental-image-ia32-pc99' ELF-loading userland images from boot modules: size=0x189000 v_entry=0x804f544 v_start=0x8048000 v_end=0x81d1000 p_start=0x25b000 p_end=0x3e4000 Moving loaded userland images to final location: from=0x25b000 to=0x160000 size=0x189000 Starting node #0 with APIC ID 0 Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: ?????? user exception 0x6 code 0x0 in thread 0xff3f5d00 "rootserver" at address 0x805130e With stack: 0x80cfda0: 0x0 0x80cfda4: 0x0 0x80cfda8: 0x0 0x80cfdac: 0x0 0x80cfdb0: 0x0 0x80cfdb4: 0x0 0x80cfdb8: 0x0 0x80cfdbc: 0x0 0x80cfdc0: 0x0 0x80cfdc4: 0x0 0x80cfdc8: 0x0 0x80cfdcc: 0x0 0x80cfdd0: 0x0 0x80cfdd4: 0x0 0x80cfdd8: 0x0 0x80cfddc: 0x0 QEMU: Terminated Have a great day.

2 1

ARM Vchan Error
by Daniel Wang 10 Jul '18

10 Jul '18

Hi all, I’m trying to make Vchan work on camkes-arm-vm in the process I encountered a couple problems. Hope you can give me some advice. I knew that Vchan is out dated and never finished on ARM. But it seems the only option for now (please correct me if I’m wrong). Here is what I did so far: 1. modified tk1_vmlinux.c by adding the virtual device and fault handler and installed it to guest linux with vm_add_device(vm, &vchan_dev); --------------------------------------------------- vchan_device_fault_handler(struct device* d UNUSED, vm_t* vm, fault_t* fault){ //uint32_t data = fault_get_data(fault); uint32_t data = fault_get_ctx(fault)->r1; vchan_entry_point(vm, data); // fflush(stdout); advance_fault(fault); return 0; } struct device vchan_dev = { .devid = DEV_CUSTOM, .name = "vchan-driver", .pstart = 0x2040000, .size = 0x1000, .handle_page_fault = &vchan_device_fault_handler, .priv = NULL, }; --------------------------------------------------- 2. compiled linux-tegra using buildroot (by the way the current linux-tegra is 4.9.0 which is not supported by buildroot-2016, the earliest version works for me is buildroot-2017-2), added a vmm-manager kernel driver similar to the one in camkes-x86-vm. But I changed the call_into_hypervisor() to the following: --------------------------------------------------- int call_into_hypervisor(int cmd, void *data, size_t sz, vmcall_args_t *vmcall) { int res = 0; int err; unsigned phys_ptr = virt_to_phys(vmcall); vmcall->data = data; vmcall->cmd = cmd; vmcall->phys_data = virt_to_phys(data); vmcall->size = sz; down(&hyp_sem); /* Set up arguments for the ARM hyp call */ asm volatile ("mov r0, %0; mov r1, %1" : : "r" (VMM_MANAGER_TOKEN), "r" (phys_ptr): "%r0", "%r1"); asm volatile (".arch_extension virt\n\t” "hvc #0"); asm volatile ("mov %0, r0" : "=r" (res) : : ); err = vargs->err; up(&hyp_sem); return err; } --------------------------------------------------- The kernel built and run correctly. But when I try to install the kernel driver. It crashed with following information. --------------------------------------------------- # modprobe driver.ko [81.826621] driver: loading out-of-tree module taints kernel Bad sys call from [Linux]: scone 0 at PC: 0xbf000214 Assertion failed” !err (/camkes-arm-vm/libs/libsel4arm-vmm/src/vm.c: vm_event: 407) ————————————————————————— I’m not sure if this error is triggered by the modified call_into_hypervisor() or by event_thread_run()->eventfd_signal(). Any help would be appreciated! Thanks in advance. Best Regards -Daniel Wang

2 1

reading thread registers
by Michael Neises 10 Jul '18

10 Jul '18

Hello, I know there exists a function seL4_TCB_ReadRegisters, which can read the registers of a certain thread, given a/the capability to the thread. Ultimately, I'm interested in reading memory at runtime to determine whether the data I expect is present. So I'm wondering, is there in seL4 an init process, whose registers contain all the working memory of the system? And furthermore, how can I access a capability to a given thread in order to pass it into the ReadRegisters function mentioned above? Cheers, Michael

2 1

Memory Region overlap error
by Jeremy Fields 09 Jul '18

09 Jul '18

Hello- I'm trying to boot Genode/seL4 on hardware. I've tried a few different combinations of versions, and GRUB configurations, without success. I keep getting the same error despite these different combinations There was a thread that touched on this, but I couldn't find any resolution http://sel4.systems/pipermail/devel/2017-December/001776.html @##################################### Bender: Hello World. framebuffer at [b8000+b8fa0) 80x25@16 warning - unknown framebuffer type framebuffer at [b8000+b8fa0) 80x25@16 warning - unknown framebuffer type Boot config: parsing cmdline 'sel4 disable_iommu' Boot config: console_port = 0x3f8 ▒Boot config: debug_port = 0x3f8 Boot config: disable_iommu = true module #0: start=0xf8f0000 end=0xffff228 size=0x70f228 name='image.elf' Physical Memory Region from 0 size 9ac00 type 1 Physical Memory Region from 9ac00 size 5400 type 2 Physical Memory Region from e0000 size 20000 type 2 Physical Memory Region from 100000 size 18dbb000 type 1 Adding physical memory region 0x100000-0x18ebb000 Physical Memory Region from 18ebb000 size 12d000 type 4 Physical Memory Region from 18fe8000 size 1000 type 1 Adding physical memory region 0x18fe8000-0x18fe9000 Physical Memory Region from 18fe9000 size 17000 type 4 Physical Memory Region from 19000000 size 4ffd000 type 1 Adding physical memory region 0x19000000-0x1dffd000 Physical Memory Region from 1dffd000 size 3000 type 3 Physical Memory Region from 1e000000 size 8e784000 type 1 Adding physical memory region 0x1e000000-0x1f800000 Physical Memory Region from ac784000 size 94000 type 2 Physical Memory Region from ac818000 size fe8000 type 1 Physical Memory Region from b0000000 size 4000000 type 2 Physical Memory Region from fed20000 size 20000 type 2 Physical Memory Region from fed50000 size 40000 type 2 Physical Memory Region from ffa00000 size 40000 type 2 Physical Memory Region from 1000000000 size 350000000 type 1 Physical memory region not addressable Adding physical memory region 0x0-0x1f800000 seL4 failed assertion '!p_region_overlaps(reg)' at /home/critical/Downloads/genode-18.05/contrib/sel4-c59276cc6e3aa138a1e56af8c8a56ce64cf327b8/src/kernel/sel4/src/ arch/x86/kernel/boot.c:123 in function add_allocated_p_region halting... Kernel entry via Interrupt, irq 0 @##################################### Any thoughts? Anything I can try? Any information I can provide to help diagnose? -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

3 3

We're hiring OS engineers
by Gernot.Heiser＠data61.csiro.au 06 Jul '18

06 Jul '18

Would you like to work on seL4 inside the TS team? Here’s your chance: https://jobs.csiro.au/job/Sydney%2C-NSW-Operating-System-Engineer/488529400/ https://jobs.csiro.au/job/Sydney%2C-NSW-Operating-Systems-Senior-Engineer/4… Gernot

1 0

Re: [seL4] IOMUX on iMX6 conflict with libethdrivers
by Kofidoku.Atuah＠data61.csiro.au 06 Jul '18

06 Jul '18

Hey Fabrizio?, I'm sorry we took so long to get back to you: The underlying problem here is that we haven't yet finished defining and implementing a driver framework for our userspace code, so in order to satisfy dependencies, we began stuffing them into the io_ops struct. So since lots of devices depend on an initialized mux driver, what you see here is the result of that, unfortunately -- the good news is that we're currently defining a driver framework internally (https://docs.sel4.systems/seL4DriverAPI/ChildEnumeration.html is one of the draft pages of documentation -- but none of this is finalized) over the course of this year. What I'd recommend is that you use the helper function, mux_sys_valid() in mux.h (https://github.com/seL4/util_libs/blob/master/libplatsupport/arch_include/a…) inside of the ethernet driver, and map the whole 16K range inside of the IO-Ops initializer -- essentially what's going on there is that there's a dependency on the mux driver that's satisfied by the IO-Ops object. Thanks very much for your patience,? and this sort of thing should be cleaned up soon. Yours truly, -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 3

Re: [seL4] seL4 CNode and capability question
by 송대영 05 Jul '18

05 Jul '18

*I have a question about capability. 1. I know that CNode can consist of hierarchy of CNodes like 1-level, 2-level, 3-level.Can I create new CNode object like them? 2. If I can create hierarchy of CNode, I want to create hierarchy of CNode in order to retype new object to new CNode object.I tried it like below source code but it doesn't work with message "Untyped Retype: Invalid destination address".Would you give some advices?--------------------- source code // ** create CNode & mapping seL4_CPtr new_CNode_cap = info->empty.start + 5; error = untyped_retype_root(untyped, seL4_CapTableObject, seL4_SlotBits, cspace_cap, new_CNode_cap); ZF_LOGF_IFERR(error, "Failed to retype our chosen untyped into an CNode object.\n"); printf("================== seL4_DebugCapIdentify ======================\n"); printf("seL4_DebugCapIdentify seL4_CPtr CNode_cap : %u \n", seL4_DebugCapIdentify(new_CNode_cap)); // ** create new Endpoint object and mapping to new CNode seL4_CPtr new_CNode_cap_Endpoint; new_CNode_cap_Endpoint = info->empty.start + 6; error = seL4_Untyped_Retype(untyped /* untyped cap */, seL4_EndpointObject /* type */, seL4_SlotBits /* size */, new_CNode_cap /* root cnode cap */, new_CNode_cap_Endpoint /* destination cspace */, 32 /* depth */, new_CNode_cap_Endpoint /* offset */, 1 /* num objects */); if(error == 0) printf("error : %d \n", error);3. Can I check CNode level? It means like CNode level number.*

1 0

IPC
by tj5527 04 Jul '18

04 Jul '18

Searching on the sel4 repository, I find there is a manual talking about IPC (https://github.com/seL4/seL4/blob/9dba8e67ccb54e207bbec22e25f21c65e5c6a45f/…) In addition to this material, where - particularly source code - would be a good start point to look into IPC design and implementation? Thanks

2 1