- Devel - lists.sel4.systems

memory zero'ing
by Sam Leffler 12 Mar '23

12 Mar '23

I'm chasing an issue that looks like retype'd memory has nonsense data. If I read the kernel code correctly it looks like the object returned by an seL4_UntypeRetype syscall should be zero'd (looks to happen when an untyped memory object is reset here <https://github.com/seL4/seL4/blob/master/src/object/untyped.c#L254>). Is that correct? I don't see anything called out in the manual. -Sam

6 9

Reminder seL4 developer hangout
by Birgit Brecknell 05 Mar '23

05 Mar '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Mar 8, 6am (UTC), Topics: (open) * Sydney: Wed, Mar 8, 5pm * Central Europe: Wed, Mar 8, 7am * US Pacific Time: Tue, Mar 7, 10pm Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

UnknownSyscall Exception Handler for non-seL4 syscall API
by lukas-graber＠protonmail.com 27 Feb '23

27 Feb '23

Hello, I am working on a syscall handler in user-space and want to implement a trap-and-emulate like mechanism. Firstly, some background information and motivation. I see that the seL4 system call API uses negative syscall numbers. This allows me theoretically to use positive syscall numbers to implement an additional syscall API. The seL4 kernel triggers an UnknownSyscall Exception whenever it encounters different syscalls and leads it to the fault handler endpoint in user space of the corresponding CAmkES component. I work with CAmkES and was able to create a fault handler similar to the one implemented in GDBMem with the help of templates. I am generally able to catch the exception in a thread in the same component and get the corresponding arguments. What I don't seem to manage is redirecting the program flow of the control thread so that we return to right after the faulting syscall instruction (should be faultIP + 2). It generally just retriggers the same exception or a different one (the VMFault exception). To better understand what I did, I quickly provide the code: - My C code: Triggers the system call number 60 with 6 arguments: ```bash int run(void) { while(1){ register int rax __asm__ ("rax") = 60; register int rdi __asm__("rdi") = 1; register int rsi __asm__("rsi") = 2; register int rdx __asm__("rdx") = 3; register int r10 __asm__("r10") = 4; register int r8 __asm__("r8") = 5; register int r9 __asm__("r9") = 6; __asm__ __volatile__ ( "syscall" : "+r" (rax) : "r" (rdi), "r" (rsi), "r" (rdx), "r" (r10), "r" (r8), "r" (r9) : "rcx", "r11", "memory"); printf("After the syscall instruction!\n"); } } ``` - My CAmkES code: We connect two threads of the component CompA, the faultIn thread is related to the From Template, the faultOut thread is related to the To template. ```bash connector camkesFaultHandlerThread { from Procedure; to Procedure; } procedure CAmkES_FaultHandlerThread { void bla(); } component CompA { control; uses CAmkES_FaultHandlerThread faultIn; provides CAmkES_FaultHandlerThread faultOut; } assembly { composition { component CompA compA; connection camkesFaultHandlerThread fault0 (from compA.faultIn, to compA.faultOut); } } ``` - The to Template: gets triggered with every fault, should handle the system call and then redirect program flow ```bash /*- set fault_ep = alloc("fault", seL4_EndpointObject, read=True, write=True, grantreply=True) -*/ /*- set info = c_symbol('info') -*/ int /*? me.interface.name ?*/__run(void) { seL4_Word fault_type; seL4_Word length; seL4_Word delegate_tcb; seL4_UserContext regs; seL4_MessageInfo_t info; while (1) { info = seL4_Recv(/*? fault_ep ?*/, &delegate_tcb); seL4_Fault_t fault = seL4_getFault(info); fault_type = seL4_MessageInfo_get_label(info); if(fault_type == seL4_Fault_UnknownSyscall){ printf("faulting PC: %zx\n",seL4_Fault_UnknownSyscall_get_FaultIP(fault)); //handle the syscall ... length = seL4_MessageInfo_get_length(info); seL4_TCB_ReadRegisters(delegate_tcb, false, 0, sizeof(seL4_UserContext) / sizeof(seL4_Word), &regs); // Which registers should I set for the faultIn thread?, right now simply jump over the syscall instruction regs.rip += 2; // Write registers back seL4_TCB_WriteRegisters(delegate_tcb, false, 0, sizeof(seL4_UserContext) / sizeof(seL4_Word), &regs); // Resume the caller seL4_MessageInfo_t info = seL4_MessageInfo_new(0, 0, 0, length); seL4_Reply(info); } else if(fault_type = seL4_Fault_VMFault){ // Why do we get in here after replying to UnknownSyscallException? } } } ``` I simply want to handle the UnknownSyscall Exception (in the faultOut thread) and then return to the instruction right after the original syscall in the control thread. But no matter how I change the IP, it just retriggers the exception or causes a VM Fault Exception. I see that there is a NextIP virtual register field in kernel/include/arch/x86/arch/64/mode/machine/registerset.h. Can I somehow set this one from userspace with setRegister? Has anyone ever tried something similar? Help would be very much appreciated. Thank you very much! Kind Regards, Lukas

2 2

Slowpath IPC mechanism
by mincheol＠vt.edu 22 Feb '23

22 Feb '23

Hi, I am wondering how the slowpath IPC mechanism works. Does it use shared memory to transfer the IPC message?

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 20 Feb '23

20 Feb '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Feb 21, 9pm (UTC), Topics: (open) * Sydney: Wed, Feb 22, 8am * Central Europe: Tue, Feb 21, 10pm * US Pacific Time: Tue, Feb 21, 1pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

2 1

Re: U-boot for Raspberry PI
by Michal Podhradsky 08 Feb '23

08 Feb '23

Hello, thank you for prompt replies! I used the default U-boot, however now I am stuck in the next phase of booting - specifically loading and booting the sel4 test image. Following the instructions in the docs ( https://docs.sel4.systems/Hardware/Rpi4.html) I do: *U-Boot> fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2711** Reading file would overwrite reserved memory **Failed to load 'sel4test-driver-image-arm-bcm2711* Which is odd. Perhaps the memory map on Rpi has changed recently? Picking another memory location gets me further (although it is unclear that it is a correct location): *U-Boot> fatload mmc 0 0x00008000 sel4test-driver-image-arm-bcm27115164988 bytes read in 235 ms (21 MiB/s)U-Boot> bootefi 0x00008000* Now, the image gets loaded but the boot fails with an seL4 assertion fail: *U-Boot> bootefi 0x00008000Card did not respond to voltage select! : -110No EFI system partitionBooting /sel4test-driver-image-arm-bcm2711ELF-loader started on CPU: ARM Ltd. Cortex-A72 r0p3 paddr=[6603000..ffffffffffffffff] dtb=6af2000Looking for DTB in CPIO archive...found at 674d958.Loaded DTB from 674d958. paddr=[123f000..1245fff]ELF-loading image 'kernel' to 1000000 paddr=[1000000..123efff] vaddr=[ffffff8001000000..ffffff800123efff] virt_entry=ffffff8001000000ELF-loading image 'sel4test-driver' to 1246000 paddr=[1246000..164bfff] vaddr=[400000..805fff] virt_entry=40ef20Enabling MMU and pagingJumping to kernel-image entry point...Bootstrapping kernelavailable phys memory regions: 3 [1000000..3b400000] [40000000..fc000000] [100000000..200000000]reserved virt address space regions: 3 [ffffff8001000000..ffffff800123f000] [ffffff800123f000..ffffff800124556b] [ffffff8001246000..ffffff800164c000]Booting all finished, dropped to user spaceseL4 failed assertion 'isSchedulable(candidate)' at /tmp/kernel/src/kernel/thread.c:371 in function schedulehalting...Kernel entry via Interrupt, irq 0* Any suggestions what am I missing? Regards Michal On Thu, Jan 19, 2023 at 5:53 PM Sudvarg, Marion <msudvarg(a)wustl.edu> wrote: > I have a version of U-boot that works. I would have to go back through > piles of notes to see what I did to make it work, but I can share the file > with you if it's helpful. > > I also had to change config.txt to set the GPU and coprocessor frequency > to a fixed value; I had issues with boot (which is handled by the GPU) and > UART without that. > > Happy to help with the process if you like. > > Marion Sudvarg > Washington University in St. Louis > > -----Original Message----- > From: mpodhradsky(a)galois.com <mpodhradsky(a)galois.com> > Sent: Thursday, January 19, 2023 7:02 PM > To: devel(a)sel4.systems > Subject: [seL4] U-boot for Raspberry PI > > Hello! > > The instructions for building seL4 for Raspberry Pi 3 and 4 mention ask > for a custom compiled U-boot. The note mentions that an automatic revert of > the specified commit no longer works. Is this patched U-boot still > necessary, or will a vanilla version work? If the customization is still > needed, do you have a modified version available? It is not clear how to > modify the recent U-boot, since it has changed significantly. > > Regards > Michal > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to > devel-leave(a)sel4.systems >

4 5

Reminder seL4 developer hangout
by Birgit Brecknell 05 Feb '23

05 Feb '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Feb 8, 6am (UTC), Topics: (open) * Sydney: Wed, Feb 8, 5pm * Central Europe: Wed, Feb 8, 7am * US Pacific Time: Tue, Feb 7, 10pm Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

kernel builds w/ different memory configurations
by Sam Leffler 26 Jan '23

26 Jan '23

I have a target platform w/ 2 pre-defined memory configs. I've created separate .dts files w/ the different memory sizes and then in src/plat/sparrow/config.cmake do: if(KernelDebugBuild) list(APPEND KernelDTSList "tools/dts/sparrow-debug.dts") else() list(APPEND KernelDTSList "tools/dts/sparrow.dts") Overloading KernelDebugBuild is awkward (it seems contrary to it's purpose) and fragile. How is this handled for existing platforms? -Sam

2 2

help with Nvidia Jetson Xavier port
by Axel Heider 26 Jan '23

26 Jan '23

Hi, we are working on porting seL4 to the Nvidia Jetson Xavier. The kernel is booting, but then there are random crashes in user mode where the cores seem to stop completely within a minute, no crash output is visible. Our test applications are just doing some integer number crunching to create load, there are no drivers involved (besides a bit of UART output). It looks like this also happened to others, a similar problem was described in this post: https://forums.developer.nvidia.com/t/illegal-instruction-with-i-cache-disa… Did anybody get seL4 userland running stable there? Axel

1 0

Inquiry to Verified Components
by Seoyeon Hwang 26 Jan '23

26 Jan '23

Hello, From this document https://apps.dtic.mil/sti/pdfs/AD1027690.pdf <https://urldefense.com/v3/__https://apps.dtic.mil/sti/pdfs/AD1027690.pdf__;…>, we figured out that system call APIs are verified (except for their composition with sel4 kernel proofs). However, we are not sure whether other process/thread-spawning APIs are also verified. We use the APIs (listed below) in our project, hoping to develop a formally verified root-of-trust architecture atop seL4. Could you let us know if they are all verified, and if so, could you also point out the resources we can cite in our paper? Thanks, Seoyeon APIs used in our projects are: Initial Process-related APIs platsupport_get_bootinfo simple_default_init_bootinfo bootstrap_use_current_simple allocman_make_vka simple_get_cnode simple_get_pd Thread Spawning APIs vka_alloc_tcb vka_alloc_frame seL4_ARCH_Page_Map vka_alloc_page_table seL4_ARCH_PageTable_Map vka_alloc_endpoint vka_mint_object seL4_TCB_Configure seL4_TCB_SetPriority sel4utils_set_instruction_pointer sel4utils_set_stack_pointer seL4_TCB_WriteRegisters sel4runtime_write_tls_image sel4runtime_set_tls_variable seL4_TCB_SetTLSBase seL4_TCB_Resume Process Spawning APIs sel4utils_bootstrap_vspace_with_bootinfo_leaky vspace_reserve_range bootstrap_configure_virtual_pool process_config_default_simple sel4utils_configure_process_custom vka_cspace_make_path sel4utils_mint_cap_to_process sel4utils_create_word_args sel4utils_spawn_process_v IPC/System call APIs seL4_MessageInfo_new seL4_MessageInfo_get_length seL4_SetMR seL4_GetMR seL4_Call seL4_Recv seL4_Reply seL4_Wait seL4_Yield

7 10