- Devel - lists.sel4.systems

Reminder seL4 developer hangout
by Birgit Brecknell 03 Apr '23

03 Apr '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Apr 5, 7am (UTC), Topics: (open) * Sydney: Wed, Apr 5, 5pm * Central Europe: Wed, Apr 5, 9am * US Pacific Time: Wed, Apr 5, 12pm (midnight) 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

seL4 summit: deadline extension to 24th of April
by June Andronick (seL4 Foundation) 31 Mar '23

31 Mar '23

The deadline to submit a presentation to the seL4 summit 2023 is extended by 2 weeks. You now have until the 24th of April 2023 to propose a talk, by uploading an abstract of one page or less to: https://sel4.systems/Foundation/Summit/2023/submit The reason for the extension is that we want to let you know the definite dates for the summit before the deadline :) Current tentative (and very likely) dates are 19-20-21 September 2023, to be confirmed very soon. Looking forward to receiving your proposals. We want to hear about your cool seL4 work! And spread the word! If you want to hear about specific seL4 work, ping people around you or let us know at summit(a)sel4.systems <mailto:summit@sel4.systems> June

1 0

Issue for setting up the seL4 IPC tutorial
by zhliao＠iastate.edu 26 Mar '23

26 Mar '23

Hi all, I got the following issue when I followed the IPC tutorial to set up an environment. I can build and run the "Hello world" and "Capabilities" tutorials, so I think I have fulfilled the prerequisites for running the IPC tutorial. However, when I built the ipc tutorial using the command "./init --tut ipc --solution" or "./init --tut ipc", and ran the "ninja" command, the following error messages were given: [54/208] Generating capDL-tool/parse-capDL FAILED: capDL-tool/parse-capDL cd /home/zhliao/sel4_tutorials_manifest/ipc_build/capDL-tool && printf capDL-tool/parse-capDL:\ > /home/zhliao/sel4_tutorials_manifest/ipc_build/capDL-tool/parse-capDL.d && find -L /home/zhliao/sel4_tutorials_manifest/projects/capdl/capDL-tool/ -type f -printf %p\ >> /home/zhliao/sel4_tutorials_manifest/ipc_build/capDL-tool/parse-capDL.d && cp -a /home/zhliao/sel4_tutorials_manifest/projects/capdl/capDL-tool/* . && /usr/bin/cmake -E env make stack build --fast Downloading lts-19.12 build plan ... RedownloadInvalidResponse Request { host = "raw.githubusercontent.com" port = 443 secure = True requestHeaders = [] path = "/fpco/lts-haskell/master//lts-19.12.yaml" queryString = "" method = "GET" proxy = Nothing rawBody = False redirectCount = 10 responseTimeout = ResponseTimeoutDefault requestVersion = HTTP/1.1 } "/home/zhliao/.stack/build-plan/lts-19.12.yaml" (Response {responseStatus = Status {statusCode = 404, statusMessage = "Not Found"}, responseVersion = HTTP/1.1, responseHeaders = [("Connection","keep-alive"),("Content-Length","14"),("Content-Security-Policy","default-src 'none'; style-src 'unsafe-inline'; sandbox"),("Strict-Transport-Security","max-age=31536000"),("X-Content-Type-Options","nosniff"),("X-Frame-Options","deny"),("X-XSS-Protection","1; mode=block"),("Content-Type","text/plain; charset=utf-8"),("X-GitHub-Request-Id","35BE:17FF:128736E:17D5D97:641FC551"),("Accept-Ranges","bytes"),("Date","Sun, 26 Mar 2023 04:08:49 GMT"),("Via","1.1 varnish"),("X-Served-By","cache-lga21983-LGA"),("X-Cache","MISS"),("X-Cache-Hits","0"),("X-Timer","S1679803730.680346,VS0,VE66"),("Vary","Authorization,Accept-Encoding,Origin"),("Access-Control-Allow-Origin","*"),("X-Fastly-Request-ID","87538dc12b06e4fb615de6c1a4159b9af113e3a6"),("Expires","Sun, 26 Mar 2023 04:13:49 GMT"),("Source-Age","0")], responseBody = (), responseCookieJar = CJ {expose = []}, responseClose' = ResponseClose}) make: *** [Makefile:51: parse-capDL] Error 1 [62/208] Invoking muslc build system ninja: build stopped: subcommand failed. I am wondering if you got the similar issues or have any idea for this problem? Thanks, Zhonghao

1 0

KataOS modifications to seL4
by Isaac Beckett 22 Mar '23

22 Mar '23

> Message: 1 > Date: Tue, 21 Mar 2023 10:52:40 -0500 > From: June Tate-Gans (ジューン) <jtgans(a)google.com> > Subject: [seL4] Bitfield generator EBNF grammar > To: devel <devel(a)sel4.systems> > Message-ID: > <CAOPTAH0q0UABvFhffnmJ6ygDuPmpf8fMjxBawmYbhCjjJT8MTA(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > Hey guys, > > I've been attempting to put together some rust bindings for the seL4 fault > handling mechanisms, and I'm afraid the bitfield generator is driving me a > bit up a wall at this point. I'd like to find a concise grammar for the > language so I can better understand how bitfield_gen.py works, but there > doesn't seem to be any explicit BNF for it anywhere. > > Is there a paper I should be reading or a reference guide somewhere that > would help? > > Thanks! > > -- > June Tate-Gans > Software Engineer > Techlead, Kata OS / AmbiML, Google Hello June, I have a question about something I read on the announcement post for KataOS: > The current GitHub release includes most of the KataOS core pieces, including the frameworks we use for Rust (such as the sel4-sys crate, which provides seL4 syscall APIs), an alternate rootserver written in Rust (needed for dynamic system-wide memory management), and the kernel modifications to seL4 that can reclaim the memory used by the rootserver. And we've collaborated with Antmicro to enable GDB debugging and simulation for our target hardware with Renode. Are these changes being formally verified? I understand it involves a not insignificant amount of labor to do so, but I worry about bugs being introduced that undermine the security properties of seL4 if care isn’t taken here. Thanks, Isaac Beckett PS: I decided to post this to the mailing list because I thought it may be of interest to some folks here.

2 2

Reminder seL4 developer hangout
by Birgit Brecknell 19 Mar '23

19 Mar '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Mar 21, 9pm (UTC), Topics: (open) * Sydney: Wed, Mar 22, 8am * Central Europe: Tue, Mar 21, 10pm * US Pacific Time: Tue, Mar 21, 2pm Calendar link: 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

shoehorn & fudge factor
by Sam Leffler 13 Mar '23

13 Mar '23

I have a target platform with only 4M of memory. When the system image is generated and the shoehorn helper script is used to find a place in memory to load the build artifacts it tacks on an extra 4M of memory use (aka fudge_factor). The comment in the code <https://github.com/AmbiML/sparrow-seL4_tools/blame/master/cmake-tool/helper…> says this is to accommodate sel4test_driver. Needless to say this breaks on my 4M target platform. So I made the fudge-factor settable from the cmd line with a default of 0 and changed the sel4test build glue to set 4M when building elfloader. Works fine for my target platform. But this change breaks building a bootable image for rpi3 (AARCH64=1 bcm28367)--shoehorn places elfloader s.t. it overlaps the image; e.g. ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 > paddr=[335000..51a0ff] > No DTB passed in from boot loader. > Looking for DTB in CPIO archive...found at 378778. > Loaded DTB from 378778. > paddr=[237000..23afff] > ELF-loading image 'kernel' to 0 > paddr=[0..236fff] > vaddr=[ffffff8000000000..ffffff8000236fff] > virt_entry=ffffff8000000000 > ELF-loading image 'capdl-loader' to 23b000 > paddr=[23b000..33bfff] > vaddr=[400000..500fff] > virt_entry=4009a8 > ERROR: image load address overlaps with ELF-loader! > ERROR: Physical address range invalid > ERROR: Could not load user image ELF Debug output of shoehorn for this case: shoehorn: debug: found CPIO identifying sequence b'070701' at offset 0x40 > in > /usr/local/google/home/sleffler/shodan/out/cantrip/aarch64-unknown-elf/release/elfloader/archive.o > shoehorn: debug: encountered CPIO entry name: kernel.elf > shoehorn: debug: encountered CPIO entry name: kernel.dtb > shoehorn: debug: encountered CPIO entry name: capdl-loader > shoehorn: debug: setting marker to 0x0 (region 0 start) > shoehorn: debug: setting marker to 0x237000 (kernel_end) > shoehorn: debug: setting marker to 0x23b000 (dtb_end) > shoehorn: debug: setting marker to 0x335000 (end of rootserver) So two questions: 1. Where is the 4M under-count of sel4test_driver? (the code indicates this might be explained in JIRA SELFOUR-2335 but I couldn't locate it) 2. Should zero'ing fudge_factor work? If yes, where should I look to remedy the above? I looked upstream for changes that might address this issue but didn't see anything. I suspect I can invert my logic and default fudge_factor to some value and then override as needed (e.g. 0 for my sparrow platform & 4M for sel4test builds). -Sam

3 5

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