- Devel - lists.sel4.systems

Question about LionsOS
by Isaac Beckett 20 Apr '24

20 Apr '24

Hello! Looking at the LionsOS website and documentation you posted, it seems like Lions is an operating system built using Microkit out of components/drivers that use the sDDF? Do I have the right shape of things in my head? Also, would sDDF drivers for a static OS like Lions (or other OS built in Microkit, since that’s what’s it’s built for) be potentially portable to other operating systems using the seL4 kernel and sDDF? Like, if I design a non-static operating system that uses sDDF drivers, could I use existing code from Lions or would I face issues with code assuming that the system’s components can’t change at runtime? Thanks, Isaac

11 26

seL4 vs QNX and Linux benchmarks
by Andrew Warkentin 20 Apr '24

20 Apr '24

Somebody in the Zoom call the other day (IIRC it was Gernot) said that seL4 IPC is considerably faster than QNX IPC, but it seems that QNX is somehow faster in a simple benchmarking experiment in which a client repeatedly sends messages to a bit-bucket server, using the TSC to determine timing. I'm running both QNX and seL4 under identical VirtualBox configurations with a single core. I'm using a QNX 6.3.1 x86-32 image i have in my collection (x86-64 support was only added in 7.0; this is the most recent image I have with dev tools installed). The seL4 version I'm using is from February 2022 and is built for x86-64 with MCS enabled (the priority of the threads is 255, and both the timeslice and budget are the initial thread default of 5 ms). My benchmark times a loop of 10000 RPCs; for QNX it's just using the regular read() function on /dev/null or a custom server that also acts like /dev/null but forces a copy of the message into a server-provided buffer, and for seL4 I'm directly calling Send()/Recv()/Reply(). I've also tested Linux's /dev/null, and QNX's implementation actually seems somewhat faster than it (for the system /dev/null; the custom server's best case seems only slightly worse than under Linux). Under QNX and Linux I'm running a C implementation of the benchmark and under seL4 I tried both C and Rust implementations (which have very similar performance). The messages on QNX and Linux are 100 bytes, and on seL4 they are 2 words, which should be hitting the fast path. Here are the best and worst cases I got: seL4: 0.114-0.136s QNX, custom null server: 0.006-0.063s QNX, system null server: 0.002-0.022s Linux: 0.004-0.005s Has anyone else benchmarked seL4 IPC against that of QNX and gotten better (or comparable) results for seL4, unlike what I got? Is synchronous IPC just less optimized under seL4 than QNX?

5 12

Release 0.1.0 of LionsOS
by Ivan Velickovic 16 Apr '24

16 Apr '24

Hello all This is a message to let people know that version 0.1.0 of LionsOS has been released. LionsOS is aimed at embedded, IoT and cyberphysical systems and is designed to be formally verifiable, adaptable to a wide class of use cases in the target domain, while at the same time setting the benchmark for performance of microkernel-based operating systems. We expect to achieve all three aims by a highly modular yet ruthlessly performance-oriented design and strict adherence to the time-honoured KISS principle. LionsOS is still in its early stages but we are at the point where we have a non-trivial example system and initial documentation. You can find the website here: https://lionsos.org/ and the source code here: https://github.com/au-ts/lionsos Thanks, Ivan

1 0

One week to go to submit a talk for seL4 summit 2024
by Birgit Brecknell 15 Apr '24

15 Apr '24

One week to go to submit a talk [0] for seL4 summit 2024 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. The seL4 Summit 2024 will be held 15-17 October 2024 at the Holiday Inn Potts Point, Sydney, Australia. The summit will be an in-person event. Registration details to follow soon. We’re looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2024/cfp [1] https://sel4.systems/Foundation/Summit/2024/ [2] https://sel4.systems/Foundation/Summit/2024/submit Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

question about the seL4/camkes-vm-examples
by PX 15 Apr '24

15 Apr '24

Hi,All I am trying to build the seL4 VMM example for the qemu-arm-virt platform from seL4/camkes-vm-exmaples. I can build the vmm image successfully, but I cannot run the image. Here are what I did: 1. I use the "../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt" command. 2. ninja After these two steps, the vmm image, capdl-loader-image-arm-qemu-arm-virt is successfully built. But when I run the generated scripts, ./simulate, to run the VMM on qemu, the vmm fails to boot up. The error message is attached below. I use Ubuntu 20.04 and QEMU emulator version 4.2.1. Do I miss something here? Do I use the correct version of the building environment? Any help would be appreciated! ./simulate ./simulate: QEMU command: qemu-system-arm -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a15 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p1 paddr=[61805000..62c02ebf] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 6192264c. Loaded DTB from 6192264c. paddr=[60042000..60043fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60041fff] vaddr=[e0000000..e0041fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' to 60044000 paddr=[60044000..6140cfff] vaddr=[10000..13d8fff] virt_entry=1880c Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. available phys memory regions: 1 [60000000..c0000000] reserved virt address space regions: 4 [e0000000..e0042000] [e0042000..e0043da9] [e0044000..e140d000] [ff000000..ff200000] Booting all finished, dropped to user space *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 65536 bytes needed, 0 bytes available).>>* run@main.c:1332 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1) install_vm_devices@main.c:704 module name: map_frame_hack install_vm_devices@main.c:704 module name: init_ram Loading Kernel: 'linux' Loading Initrd: 'linux-initrd' Loading Generated DTB -------- *Pagefault from [vm0]: read prefetch fault @ PC: 0x4 IPA: 0x4, FSR: 0x6* *Context:* *r0: 0x0* *r1: 0xffffffff* *r2: 0x4f000000* *r3: 0x0* *r4: 0x0* *r5: 0x0* *r6: 0x0* *r7: 0x0* *r8: 0x0* *r9: 0x0* *r10: 0x0* *r11: 0x0* *r12: 0x0* *pc: 0x4* *r14: 0x0* *sp: 0x0* *cpsr: 0x9b* m-------- main_continued@main.c:1310 Failed to run VM Halting...

3 4

seL4 developer hangout reminder
by Birgit Brecknell 15 Apr '24

15 Apr '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 16 Apr, 22:00 UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 docker build issues on Apple Silicon
by Mark Jones 14 Apr '24

14 Apr '24

Dear All, I’m trying to use the instructions on https://docs.sel4.systems/projects/dockerfiles/ to set up an seL4 docker build environment on an Apple Silicon Mac. I’ve actually tried this on two different machines (with small variations in the versions of macOS Sonoma, Apple Silicon, and Docker between each of the machines), but get the same result on each one. I’m hoping that other folks on this list might know how to fix this. I start by running: git clone https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles.git cd seL4-CAmkES-L4v-dockerfiles make user But the make command fails with the output appended below. Any hints (including other places to post this question) would be much appreciated! Best wishes, Mark ______________ scripts/utils/check_for_old_docker_imgs.sh WARNING: Unable to check if your trustworthysystems docker images are getting a bit old! The date command did not behave as expected. Skipping the check. docker build --force-rm=true \ --build-arg=USER_BASE_IMG=trustworthysystems/camkes \ -f dockerfiles/extras.Dockerfile \ -t extras \ . [+] Building 109.7s (6/6) FINISHED docker:desktop-linux => [internal] load build definition from extras.Dockerfile 0.0s => => transferring dockerfile: 602B 0.0s => [internal] load metadata for docker.io/trustworthysystems/camkes:latest 1.4s => [internal] load .dockerignore 0.0s => => transferring context: 153B 0.0s => [1/2] FROM docker.io/trustworthysystems/camkes:latest@sha256:29206d51ef1d09bb5e1934b11a1946a13d13333ab0ff7c2ff2645ea 96.3s => => resolve docker.io/trustworthysystems/camkes:latest@sha256:29206d51ef1d09bb5e1934b11a1946a13d13333ab0ff7c2ff2645ea2 0.0s => => sha256:e943b5afb84223c55b5dfdbe2f383970021765c345c51b08fa8b9b0d4d69ccd7 9.97kB / 9.97kB 0.3s => => sha256:46cbb6e89f5727950fb43b0c4b18a28073c18ad928ccf16c6e2a9f6d708ccb35 80.82MB / 80.82MB 6.9s => => sha256:29206d51ef1d09bb5e1934b11a1946a13d13333ab0ff7c2ff2645ea2e12c65f2 1.79kB / 1.79kB 0.0s => => sha256:678186f76064904e561bbec5cc0fb200e1c7d0435dbeeaf2433d050631a132ab 6.82kB / 6.82kB 0.0s => => sha256:99046ad9247f8a1cbd1048d9099d026191ad9cda63c08aadeb704b7000a51717 31.36MB / 31.36MB 3.0s => => sha256:4f4fb700ef54461cfa02571ae0db9a0dc1e0cdb5577484a6d75e68dc38e8acc1 32B / 32B 0.8s => => sha256:be52171dda4a5d045a589cf92b25fe60ac5b74dac75bb03997d5a049d47b361e 1.15GB / 1.15GB 53.1s => => extracting sha256:99046ad9247f8a1cbd1048d9099d026191ad9cda63c08aadeb704b7000a51717 1.2s => => sha256:460c68d68ad3efcc4c324e3da3ea9a8d7ebee818d87643e78fa551c90106c218 1.19GB / 1.19GB 65.4s => => extracting sha256:e943b5afb84223c55b5dfdbe2f383970021765c345c51b08fa8b9b0d4d69ccd7 0.0s => => extracting sha256:46cbb6e89f5727950fb43b0c4b18a28073c18ad928ccf16c6e2a9f6d708ccb35 3.0s => => extracting sha256:4f4fb700ef54461cfa02571ae0db9a0dc1e0cdb5577484a6d75e68dc38e8acc1 0.0s => => extracting sha256:be52171dda4a5d045a589cf92b25fe60ac5b74dac75bb03997d5a049d47b361e 20.1s => => extracting sha256:460c68d68ad3efcc4c324e3da3ea9a8d7ebee818d87643e78fa551c90106c218 22.7s => [2/2] RUN apt-get update -q && apt-get install -y --no-install-recommends cowsay sudo 11.8s => exporting to image 0.1s => => exporting layers 0.1s => => writing image sha256:29bf5499ec09fe5c0398c5023deb519373d25d2c8ea0d3d0d964759317511415 0.0s => => naming to docker.io/library/extras 0.0s View build details: docker-desktop://dashboard/build/desktop-linux/desktop-linux/ohi6vc8w1dj06hmvvu5ocypjs What's Next? 1. Sign in to your Docker account → docker login 2. View a summary of image vulnerabilities and recommendations → docker scout quickview docker build --force-rm=true \ --build-arg=EXTRAS_IMG=extras \ --build-arg=UNAME=user \ --build-arg=UID=502 \ --build-arg=GID=20 \ --build-arg=GROUP=staff \ -f dockerfiles/user.Dockerfile \ -t user_img-user . [+] Building 0.7s (2/2) FINISHED docker:desktop-linux => [internal] load build definition from user.Dockerfile 0.0s => => transferring dockerfile: 353B 0.0s => ERROR [internal] load metadata for docker.io/library/extras:latest 0.6s ------ > [internal] load metadata for docker.io/library/extras:latest: ------ user.Dockerfile:9 -------------------- 7 | ARG EXTRAS_IMG=extras 8 | # hadolint ignore=DL3006 9 | >>> FROM $EXTRAS_IMG 10 | 11 | # Get user UID and username -------------------- ERROR: failed to solve: extras: pull access denied, repository does not exist or may require authorization: server message: insufficient_scope: authorization failed View build details: docker-desktop://dashboard/build/desktop-linux/desktop-linux/q25mw2voldchjfgf3ybhy2q0d make: *** [build_user] Error 1

2 2

Release 0.4.0 of the seL4 Device Driver Framework
by Ivan Velickovic 09 Apr '24

09 Apr '24

Hello all This is a message to let people know that version 0.4.0 of the seL4 Device Driver Framework (sDDF) has been released. The sDDF aims to provide a collection of interfaces, libraries and tools for writing device drivers for seL4 that allow accessing devices securely and with low overhead. Some may be familiar with the sDDF from previous seL4 Summit talks. Since the pre-release at the 2023 Summit, we have made significant improvements to the networking sub-system, generally rationalising interfaces and further improving performance, the Ethernet device-class interfaces are now mature. We have also introduced preliminary specs and prototype implementations for serial, I2C, block, audio and graphics device classes. You can find information about the release and the accompanying documentation here: https://github.com/au-ts/sddf/releases/tag/0.4.0 Thanks, Ivan

1 0

Two weeks to go to submit a talk for seL4 summit 2024
by Birgit Brecknell 08 Apr '24

08 Apr '24

Two weeks to go to submit a talk [0] for seL4 summit 2024 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. The seL4 Summit 2024 will be held 15-17 October 2024 at the Holiday Inn Potts Point, Sydney, Australia. The summit will be an in-person event. Registration details to follow soon. We’re looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2024/cfp [1] https://sel4.systems/Foundation/Summit/2024/ [2] https://sel4.systems/Foundation/Summit/2024/submit -- Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems bbrcknl(a)gmail.com

1 0

sel4test CACHEFLUSH0001 failed
by Leonid Meyerovich 29 Mar '24

29 Mar '24

Hello, I run sel4test on the aarch64 platform. My CACHEFLUSH0001 test in sel4test failed /* Clean makes data observable to non-cached page */ *ptr = 0xC0FFEE; *ptrc = 0xDEADBEEF; test_assert(*ptr == 0xC0FFEE); test_assert(*ptrc == 0xDEADBEEF); I have tried to make to 'improve' memory/cache coherence, but the last assertion still failed /* Clean makes data observable to non-cached page */ *ptr = 0xC0FFEE; *ptrc = 0xDEADBEEF; error = seL4_ARM_Page_Clean_Data(framec, 0, PAGE_SIZE_4K); error = seL4_ARM_Page_Invalidate_Data(framec, 0, PAGE_SIZE_4K); __asm volatile("dmb sy" ::: "memory"); test_assert(*ptr == 0xC0FFEE); test_assert(*ptrc == 0xDEADBEEF); Thank you, Leonid

2 2

Re: Only 512mb ram available on capdl-loader-image-arm-qemu-arm-virt image
by Peter Chubb 26 Mar '24

26 Mar '24

>>>>> "Daniele" == Daniele Feliciani <felicianidaniele(a)gmail.com> writes: Daniele> Hello Peter, I have the same Daniele> problem. i tried to change the guest ram value to Daniele> 0x40000000. I added set(QEMU_MEMORY "2048") in config.cmake Daniele> but I get the following errors while running : " Daniele> map_vm_memory_reservation@guest_memory.c:477 Failed to get Daniele> frame for reservation address 0x60000000" and " Daniele> vm_ram_touch@guest_ram.c:165 Failed to touch ram region: Not Daniele> registered RAM region 32 bit ARM insts not decoded" Check the size of the MMIO region. By default it uses 29 bits; for a 2G region you need 31 bits. In the devices.camkes file, in the untyped_mmios section. There's probably an entry, "0x40000000:29", try increasing this to "0x40000000:31" to get a 2^31 region. -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

3 3

Re: Only 512mb ram available on capdl-loader-image-arm-qemu-arm-virt image
by Daniele Feliciani 25 Mar '24

25 Mar '24

It doesn't seem to work. I'm attaching the device.camkes file and the error screenshots. Il giorno lun 25 mar 2024 alle ore 10:43 Peter Chubb < peter.chubb(a)unsw.edu.au> ha scritto: > >>>>> "Daniele" == Daniele Feliciani <felicianidaniele(a)gmail.com> writes: > > Daniele> I changed the value but now i > Daniele> have the following error: > > Danielle> ./simulate: QEMU command: qemu-system-aarch64 -machine > Danielle> virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 > -nographic > Danielle> -m size=2048 -kernel > images/capdl-loader-image-arm-qemu-arm-virt > Danielle> ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 > Danielle> paddr=[61b07000..62ee00b7] > Danielle> No DTB passed in from boot loader. > Danielle> Looking for DTB in CPIO archive...found at 61c07c68. > Danielle> Loaded DTB from 61c07c68. > Danielle> paddr=[60242000..60243fff] > Danielle> ELF-loading image 'kernel' to 60000000 > Danielle> paddr=[60000000..60241fff] > Danielle> vaddr=[8060000000..8060241fff] > Danielle> virt_entry=8060000000 > Danielle> ELF-loading image 'capdl-loader' to 60244000 > Danielle> paddr=[60244000..6170cfff] > Danielle> vaddr=[400000..18c8fff] > Danielle> virt_entry=408d88 > Danielle> Enabling hypervisor MMU and paging > Danielle> Jumping to kernel-image entry point... > Danielle> > Danielle> Bootstrapping kernel > Danielle> Warning: Could not infer GIC interrupt target ID, assuming 0. > Danielle> available phys memory regions: 1 > Danielle> [60000000..c0000000] > ^^^^^^^^^ this is the physical memory region you have to play > with. Make the region given to the VM start at 0x60000000 > instead of 040000000 > > -- > Dr Peter Chubb https://trustworthy.systems/ > Trustworthy Systems Group CSE, UNSW > Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm. >

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 25 Mar '24

25 Mar '24

Hi all A friendly reminder that the seL4 developer hangout is on next week: * Wed Apr 3, 7am UTC For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Only 512mb ram available on capdl-loader-image-arm-qemu-arm-virt image
by skydivebcn＠gmail.com 25 Mar '24

25 Mar '24

Hi! I'm running a an aarch64 Linux guest with qemu with "qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -m size=2048 (...) -kernel capdl-loader-image-arm-qemu-arm-virt". I have noticed that no matter how I set the "-m size" parameter that only 512MB are available to the Linux guest. Removing the "highmem=off" crashes the system. Ok, what is the fastest, easiest way to get a workaround to this (if possible)? and have much more RAM available to Linux guest? Best,

2 1

next seL4 TSC meeting on Fri 22 Mar
by Gerwin Klein 20 Mar '24

20 Mar '24

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Fri, 22 Mar, 6pm - Central Europe: Fri, 22 Mar, 8am - US West Coast (LA/SF): Fri, 22 Mar, 0:00h See also the seL4 calendar feed available from here: https://sel4.systems/contact/home.pml The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/83417411537 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - action items from last meeting - RFC-17: IPI API - RFC-16: PMU (for discussion/feedback, not enough detail yet to vote) - RFC-15: Morello (for discussion/feedback, not enough detail yet to vote) - RFC-14: MCS budget limit thresholds — status? - should we remove deprecated sel4lib functions to enable verification? - steps for next seL4 release - discussion if there is time: - use GitHub discussions instead of discourse? (i.e. retire discourse?) - use GitHub for RFC process? (i.e. retire/archive JIRA?) If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 18 Mar '24

18 Mar '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Tue Mar 19, 9pm UTC For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Re: DIFFICULTY RUNNING SEL4TEST ON RASPBERRY PI 4 REV 1.5 4GB
by Peter Chubb 15 Mar '24

15 Mar '24

>>>>> "Mario" == Mario CUSANO <mario.cusano(a)rina.org> writes: Mario> I hope this email finds you well. I am reaching out to seek Mario> assistance regarding running sel4test on a Raspberry Pi 4 Mario> Rev1.5 4GB. seL4 is only supported at the moment on the Raspberry Pi 4B with a BCM2711. Each build of seL4 is specific to a particular SoC. The Rev 1.5 has a different SoC. I don't know if anyone has done the work to port seL4 to the Rev 1.5 Pi4, which (I think) uses a BCM2835. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

2 1

How would you approach supporting a new processor architecture?
by Isaac Beckett 09 Mar '24

09 Mar '24

Hello! I’m writing to ask how someone would approach porting seL4 to a new CPU architecture. For example, ppc64le/IBM Power, since those systems can be run with limited or no black box firmware blobs, they could offer stronger security under seL4 since you can audit or replace the platform firmware in many cases. There’s even an OEM manufacturing Power9 systems with this in mind. That said, I know supporting a new architecture is not trivial. New platform code would have to be written and verified, and existing userspace code for Arm and x86-64 may have to be adjusted. How does one approach something like this? Is it feasible for someone less familiar with seL4’s internals to get something quick and dirty running as a proof of concept?

2 2

question about booting camkes Arm VMM on TX1 from SD card
by PX 09 Mar '24

09 Mar '24

Hi, all, I tried to boot the camkes arm vmm on TX1 from a SD Card, but failed. I just follow the instructions at https://github.com/seL4/camkes-vm-examples/blob/master/README.md, and do nothing new. I build the vmm image using the "../init-build.sh -DAARCH64=YES -DCAMKES_VM_APP=minimal DPLATFORM=tx1", I got the image, capdl-loader-image-arm-tx1, and copied it to a SD card. I believe this image is a binary image. On the TX1 board, I try to load it using the u-boot command: 1.mmc dev 1 2.fatload mmc 1 0x80000000 capdl-loader-image-arm-tx1 3.go 0x80000000 However, I cannot boot the guest VM. seL4 failed assertion "cap_get_capType(destSlot->cap)==cap_null_cap" Did I miss something here? Did I set the wrong load address for Tx1? Thanks,

1 0

RISC-V Page Tables for SV39
by Jeff 09 Mar '24

09 Mar '24

Hello, I am trying to understand how the seL4_RISCV_PageTable_Map function works when working with SV39, where we have 3 page tables. The RISCV implementation doesn't have the advantage of the separate levels, so for all the page tables, we can only use the same function. However, based on the description, there are a few questions that I have: *Description:* Starting from the VSpace, map the page table object at any unpopulated level for the provided virtual address. If all paging structures and mappings are present for this virtual address, return an seL4_DeleteFirst error. It says it maps the page table object at *any unpopulated *level for the provided virtual address. What does that necessarily mean? When you attempt to map the pages, how do you differentiate between the different levels? Is it just based on the vaddr or do you have to point the vspace to one of the lower level pages? Or does vspace have to be the root page table? Thanks, Jeff

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 04 Mar '24

04 Mar '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Mar 6, 7am UTC For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

RISC-V Simulation Support
by Jeffery Lim 26 Feb '24

26 Feb '24

Hello, What does the Simulation column mean in the RISC-V table in https://docs.sel4.systems/Hardware/? Does it mean that spike is the only supported platform to run qemu simulations? All the other platforms can only be run on hardware? Thanks, Jeff

2 1

interested in participating in a survey on seL4 website and docsite structure next week?
by June Andronick (seL4 Foundation) 19 Feb '24

19 Feb '24

Hi, We are working on improvements to the seL4 website (https://sel4.systems/) and docsite (https://docs.sel4.systems/) Next week, we will conducting a survey (over a week) to gather feedback on the website and docsite structures. If you’re interested in participating, please email me at june(a)sel4.systems Thanks June

5 5

Reminder seL4 developer hangout
by Birgit Brecknell 19 Feb '24

19 Feb '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * UTC: Tue, 20 Feb, 9pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

new RFCs
by Gerwin Klein 13 Feb '24

13 Feb '24

I would like to draw your attention to two new RFCs that have been proposed for discussion and later decision by the technical steering committee: RFC-17: seL4 multikernel IPI (Inter-Processor Interrupt) API https://sel4.atlassian.net/browse/RFC-17 RFC-16: Add new capability for the PMU (Performance Management Unit) https://sel4.atlassian.net/browse/RFC-16 Please comment and give feedback if you have any. The slightly older RFC-15 and RFC-14 that may benefit from further discussion (type RFC-15 or RFC-14 into the search field at the top of the page on https://sel4.atlassian.net/) Cheers, Gerwin

1 0

SeL4 Question: Implementation of encrypted file types
by info＠wolffgames.com 12 Feb '24

12 Feb '24

Greetings SeL4 Development, My name is Marc Wolff, currently located in Portland, Oregon, USA. I'm CEO of Leyline Nexus, an R&D team primarily for game development, but also some other things. I have an implementation question for the SeL4 microkernel, and I was hoping you could point me in the right direction. Unfortunately I'm not a computer scientist and my knowledge is both self-taught and currently very limited. Right now we're focused on tabletop games, but our next development target is video games and hardware development. I see based on what I can understand from the whitesheet that SeL4 can hypervise, but I'm wondering about an idea to fully secure it on the hardware side, essentially solving one its primarily vulnerabilities. The basic idea starts with a modified risc-based CPU architecture on an FPGA (since x86 is compromised) for testing. This includes a microcode-embedded SeL4 mk with an added feature for encrypting a NEW SYSTEM of FILE TYPES. Here, all files types become a system-specific encrypted file type which presents a virtual (more common) file type externally for readability, e.g. ".doc" or ".exe". I suppose this would be at -0 privilage, since it happens in microcode and the processs would not be accessible through ASM instructions, except through dedicated query ports and flag registers. The result is that the system comes up with its own hidden and encrypted name, for example, for the .exe file type. I guess it could do this for any arbitrary file name, so long as its source code could be validated by the hyperviser (possibly modified?; it would have to do this both at runtime when executing code and when compiling). When compiling files, if the microkernel discovers exploits in the code (invalid requests, etc.), then it can simply compile it as the standard file type that could run on other systems (.exe) but not on this system - since this system only reads its own encrypted file types. If there's an existing standard output for invalid programs in SeL4 then this could modify that or be added to it for certain cases. I suppose this would entirely depend on the quality of encryption, save for reverse-engineering through decapping or something, but it seems like a potential solution for fully separating virtual memory from runtime execution. I definitely DO NOT know what I'm talking about, but from my perspective this seemed like a great way to implement copyright protection on game hardware SOC's. Maybe on the FPGA you could even do a sub-GPU within a microkernel core that was dedicated to encrypting? Maybe someone has already thought of all this before? If yes, we'd be very interested to know - as it could save us a lot of time and headaches... Best regards, Marc Marc Wolff Email: info(a)wolffgames.com Phone: 530.210.4811

3 4

root task executable memory changed
by Leonid Meyerovich 08 Feb '24

08 Feb '24

Hello, I have a seL4 project that creates a number of processes with multiple threads. An application works fine. Every process periodically calculates the checksum of the executable segment and the system (Monitor process) keeps track that these values should be the same over the time. Some time when I change (add) some code in amu process I have an error that Monitor process prints CHECKSUM ERROR -------- Someone modified executable memory process=Startup 0x400000 8868997 last->10daf436f961b809 this->95ebd3119aee7736!!!! It always complains about the root (Startup) task. Checksum value changes every time the Startup process calculates it. The code that calculate executable segment are: typedef struct { unsigned char e_ident[EI_NIDENT]; /* Magic number and other info */ Elf64_Half e_type; /* Object file type */ Elf64_Half e_machine; /* Architecture */ Elf64_Word e_version; /* Object file version */ Elf64_Addr e_entry; /* Entry point virtual address */ Elf64_Off e_phoff; /* Program header table file offset */ Elf64_Off e_shoff; /* Section header table file offset */ Elf64_Word e_flags; /* Processor-specific flags */ Elf64_Half e_ehsize; /* ELF header size in bytes */ Elf64_Half e_phentsize; /* Program header table entry size */ Elf64_Half e_phnum; /* Program header table entry count */ Elf64_Half e_shentsize; /* Section header table entry size */ Elf64_Half e_shnum; /* Section header table entry count */ Elf64_Half e_shstrndx; /* Section header string table index */ } Elf64_Ehdr; extern char __executable_start[]; // function returns executable segment start address and size int initStartupElfSegsParams(Elf64_Ehdr *pELFHeader, uintptr_t *startAddr, uintptr_t *size) { seL4_Word phoff = pELFHeader->e_phoff; Elf_Phdr *currentPH = (Elf_Phdr *)((void *)pELFHeader + phoff); for (int i=0; i<pELFHeader->e_phnum; i++) { ZF_LOGD("ELF: p_type=%x p_flags=%x p_vaddr=%p p_memsz=%lu", currentPH[i].p_type, currentPH[i].p_flags, (void *)currentPH[i].p_vaddr, currentPH[i].p_memsz); if ( ((currentPH[i].p_type & 1) == 1) && ((currentPH[i].p_flags & 1) == 1)) // p_flags & 1 == 1 - executable { *startAddr = (uintptr_t)currentPH[i].p_vaddr; *size = (uintptr_t)currentPH[i].p_memsz / sizeof(uint64_t); return 0; } } return -1; }; initStartupElfSegsParams((Elf64_Ehdr *)__executable_start, &proc_validate_params[STARTUP_INDEX].p_addr, &proc_validate_params[STARTUP_INDEX].p_size); Any help will be appreciated. Thanks

2 6

Reminder seL4 developer hangout
by Birgit Brecknell 05 Feb '24

05 Feb '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Feb 7, 6pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

fault processing
by Leonid Meyerovich 27 Jan '24

27 Jan '24

I am working on fault processing. When I am a fault I am calling void sel4utils_print_fault_message(seL4_MessageInfo_t tag, const char *thread_name) from sel4libsutils library I have tested it for "page fault" condition and it works fine - I am getting seL4_Fault_VMFault fault type But in certain case I have got seL4_Fault_VCPUFault type, which is not implemented sel4libsutils library I try to process this fault similar to seL4_Fault_VMFault to get all neccessary registers, but the kernel does not have functions like seL4_Fault_VCPUFault_get_IP. What is the message format for VCPU fault? Thanks

2 3

seL4 fault processing
by Leonid Meyerovich 25 Jan '24

25 Jan '24

My root task (root thread created by kernel) checks for fault from the other threads, which are created in root thread with badged fault_ep seL4_Word badge; seL4_MessageInfo_t messageInfo = seL4_NBRecv(init_objects.fault_cap, &badge); if (seL4_MessageInfo_get_label(messageInfo) != seL4_Fault_NullFault ) { process_fault(messageInfo, badge); } Normally I don't have any faults, but every time I have seL4_MessageInfo_get_label(messageInfo) == 4, which is not in seL4_Fault_tag enumeration type enum seL4_Fault_tag { seL4_Fault_NullFault = 0, seL4_Fault_CapFault = 1, seL4_Fault_UnknownSyscall = 2, seL4_Fault_UserException = 3, seL4_Fault_VMFault = 5, seL4_Fault_VGICMaintenance = 6, seL4_Fault_VCPUFault = 7, seL4_Fault_VPPIEvent = 8 }; Could somebody explain? Thanks,

4 5

seL4 root task executable memory region
by Leonid Meyerovich 25 Jan '24

25 Jan '24

I assume that the code segment of the root task starts from __executable_start address. Does it point to ELF header? Or code starts directly from this address? Thank you,

1 0

seL4 fault handling
by Leonid Meyerovich 24 Jan '24

24 Jan '24

Hello, Where can I find a comprehensive description of fault message registers for every of the following faults enum seL4_Fault_tag { seL4_Fault_NullFault = 0, seL4_Fault_CapFault = 1, seL4_Fault_UnknownSyscall = 2, seL4_Fault_UserException = 3, seL4_Fault_VMFault = 5, seL4_Fault_VGICMaintenance = 6, seL4_Fault_VCPUFault = 7, seL4_Fault_VPPIEvent = 8 }; Thanks, LM

3 3

Reminder seL4 developer hangout
by Birgit Brecknell 22 Jan '24

22 Jan '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jan 24, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Reminder seL4 developer hangout
by Gerwin Klein 09 Jan '24

09 Jan '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jan 10, 6pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

CAmkES VMM custom OS
by Hugo V.C. 18 Dec '23

18 Dec '23

Hi all, I'm wondering if someone could forward me to the path I must follow to achieve booting a Hermit unikernel (https://github.com/hermit-os/hermit-rs) via CAmkES VMM. I know CAmkES VMM are "virtualised Linux guests on seL4 for ARM and x86 platforms" but I think that being able to boot a Rust based unikernel opens the door to a fascinating World... (no more dependency on "fat/buggy" Linux kernel). Any help where I need to start? Does it require to modify CAmkES VMM to add such functionality? Best,

2 2

get interrupts in x86
by os.team.1992＠gmail.com 14 Dec '23

14 Dec '23

Hi I am trying to run linux OS on camkes seL4 hypervisor. The hardware I use is x86-64. But I do not receive the interrupts from the devices that I have passthrough, and Linux is managing the interrupts in the form of pooling. This problem exists at the kernel level. Where the IO/APIC settings should be applied to the system but are not applied correctly. Is this problem solved in internal versions? For example, physical interrupt 10 is defined for network hardware. Vector 58 is defined for this interval. The IO/APIC information used for this device is also specified. However, interrupts are not received correctly. (In fact, because the level trigger is set, interrupts are sent quickly, this is not true and causes a destructive effect on the performance of the guest OS)

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 11 Dec '23

11 Dec '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Dec 13, 6pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Question on TCB without SC in receiveSignal
by chenpingyuan＠xiaomi.com 05 Dec '23

05 Dec '23

Hello guys, I got confused on the implementation of receiveSignal in sel4 with MCS. When the notification status is NtfnState_Active, the kernel will try to donate the notification's schedule context to the thread by calling maybeDonateSchedContext. My confusion point is that: If the thread doesn't have a valid schedule context, the thread will not be able to execute, then how can this thread call receiveSignal to receive the signal? void receiveSignal(tcb_t *thread, cap_t cap, bool_t isBlocking) { notification_t *ntfnPtr; ntfnPtr = NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)); switch (notification_ptr_get_state(ntfnPtr)) { .... case NtfnState_Active: setRegister( thread, badgeRegister, notification_ptr_get_ntfnMsgIdentifier(ntfnPtr)); notification_ptr_set_state(ntfnPtr, NtfnState_Idle); #ifdef CONFIG_KERNEL_MCS maybeDonateSchedContext(thread, ntfnPtr); // If the SC has been donated to the current thread (in a reply_recv, send_recv scenario) then // we may need to perform refill_unblock_check if the SC is becoming activated. if (thread->tcbSchedContext != NODE_STATE(ksCurSC) && sc_sporadic(thread->tcbSchedContext)) { refill_unblock_check(thread->tcbSchedContext); } #endif break; } }

2 9

seL4 summit 2024: survey about location
by Birgit Brecknell 29 Nov '23

29 Nov '23

Dear seL4 friends, With the great success of the seL4 summit 2023 behind us, we are now looking at the seL4 summit 2024! This should happen around Sep/Oct 2024. We have started investigating options for the location, and we would like your feedback. We would greatly appreciate it if you could fill in this very short survey to tell us your opinion between Abu Dhabi and Sydney: https://forms.gle/LQKSHVrqLGNqV2Ld8 Please do so by Nov 22nd 2023. Feel free to forward to anyone you believe may want to attend the summit next year. Many thanks! June & Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

2 3

How to avoid priority inversion in seL4
by chenpingyuan＠xiaomi.com 29 Nov '23

29 Nov '23

Hello experts, I'm reading the code of seL4 kernel, but I got confused how seL4 could help to avoid priority inversion. seL4 itself doesn't change the priority of TCB at the kernel level, does it mean that seL4 leaves the user level to handle priority inversion? Regards Neil.

2 2

A few questions regarding seL4
by Benjamin J. Kelly 29 Nov '23

29 Nov '23

To Whom It May Concern, My name is Ben Kelly. Myself and my partner James Briscoe - CC'd on this email - are in the beginning stages of starting a company that will host websites and web services for clients requiring high security on hardware that we control from the firmware up. We haven't decided which OS we want to use yet. Our initial goal is a customizable OS that contains only the minimum services to host a web server and nothing else. We will be evaluating the seL4 Microkernel. We're also intrigued by the possibilities of enhanced application performance and security that can be had from a unikernel approach. Is there anything that would forbid using the seL4 MicroKernel acting as a 'hypervisor/scheduler' for highly isolated and performant unikernel applications? If not, seL4 and Unikernel technology could potentially deliver the maximum amount of performance and security possible for hardware running seL4-compatible CPUs. In the following video Boyd Multerer, https://youtu.be/YG5BaoB24eA?si=TcxHq51Q5HLC0m1_ was asked the question if seL4 would "make sense on servers." Boyd replied that "I think it would but it's not something that we are targeting ... yet." He also said that "Yeah, I do think seL4 would be perfect at the bottom of the server once the multi-core thing gets figured out. But we don't need to solve that right away." Do you think seL4 is mature enough for our purpose? If we were to invest our time doing a deep dive into understanding seL4 do you know of any companies that are willing to pay for our acquired knowledge? Very Respectfully, Benjamin J. Kelly President Windsor Lake Computing LLC http://windsorlake.llc/ Sent with [Proton Mail](https://proton.me/) secure email.

3 5

Reminder seL4 developer hangout
by Birgit Brecknell 27 Nov '23

27 Nov '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Nov 29, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

How to run seL4 on FVP?
by Hesham Almatary 23 Nov '23

23 Nov '23

Hello, I can build sel4test for FVP, how do I run it there? I couldn't find any documentation on that, would be great if someone could drop a command line and any required dependencies. Regards, Hesham

3 4

Use C-parser on seL4 based application
by r2ji＠uwaterloo.ca 20 Nov '23

20 Nov '23

Hi, I have been trying to reuse the seL4 verification framework to verify a toy example I built on seL4, and I am currently stuck on the c-parser step. I am trying to use c-parser to parse the example I built, then conduct refinement verification. The toy example is a normal c project, which includes `sel4.h`. From this thread: https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/3QYNFY… I learned that I am supposed to do $ ./isabelle/bin/isabelle jedit -d . -l CParser toy.thy And the toy.thy file is supposed to begin with `install_C_file("toy.c")`. However, since toy.c includes sel4.h, I am not sure how to preprocess it before I put it into toy.thy. I know the standalone c-parser can have a -I flag to include in all the dependency directories, but it cannot open an interactive window. (From my understanding, the standalone c-parser seems to be only a checking tool) I also know that when sel4 is parsed into HOL, it is preprocessed into a single c file `kernel_all.c_pp`, which is later parsed. I am not sure if the preprocessor tool can be reused for other applications as well. My question is summarized as: 1. Is there a way to add an include directory in interactive CParser? 2. If not, can I reuse the preprocessing approach for sel4 to preprocess my application to a singleton file that can be parsed by c-parser? Any help will be appreciated! Thanks, Ru

2 2

Conclusions regarding speculation
by Demi Marie Obenour 18 Nov '23

18 Nov '23

I talked with a Xen developer and came to these conclusions: - Speculative taint tracking provides complete protection against speculative attacks. This is sufficient to prevent leakage of cryptographic key material, even in fully dynamic systems. Furthermore, it is compatible with fast context switches between protection domains. - Full time partitioning eliminates all timing channels, but it is possible only in fully static systems, which severely limits its applicability. - Time protection without time partitioning does _not_ fully prevent Spectre v1 attacks, and still imposes a large penalty on protection domain switches. Additionally, I am almost certain that: - On properly designed hardware, both time protection and speculative taint tracking can be enabled and disabled by systems software. - Time protection and speculative taint tracking are not mutually exclusive. A cloud provider might use time partitioning to partition different customers from each other, while guest OSs use speculative taint tracking to protect different processes from each other. In short, time protection is excellent, but it is not a sufficient mechanism for general-purpose computing. Speculative taint tracking is a different mechanism that is applicable to many more workloads, and which provides complete protection against speculative attacks. Both mechanisms can be used together depending on system security policy. -- Sincerely, Demi Marie Obenour (she/her/hers)

6 18

CfP: Microkernel and Component-based OS Devroom at FOSDEM 2024
by Martin Decky 16 Nov '23

16 Nov '23

Microkernel and Component-based OS Devroom at FOSDEM 2024 CALL FOR PARTICIPATION On-line version of this CfP: http://fosdem.microkernel.info/ The developers and users of several free and open source microkernel-based, unikernel-based and component-based operating systems will meet as part of FOSDEM 2024 [1] and will share a developer room. The devroom is currently looking for content in the form of talks and other activities related to microkernel-based, unikernel-based, component-based operating systems and similar areas. Possible topics of the devroom include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * languages, tools and toolchains used * enabling support for hardware (architectures, device drivers) and programming languages * development processes, debugging * maintenance, testing and release engineering * safety, security and robustness * trends and challenges * research and open questions * community and governance * use cases, experiences and status updates * best practices and lessons learned * demos The devroom has been scheduled to Saturday February 3rd 2024 in the afternoon (Central European Time). This is a call for your participation. We kindly ask you to submit your proposals no later than on December 10th 2023 (End of Day, Anywhere on Earth). Please use the pretalx [2] web site to submit your proposals. Note that this is a new submission system and the user accounts from the previous submission system (pentabarf) have not been transferred. Make sure to select the Microkernel and Component-based OS as the track when submitting your proposal and include at least the following information: * title of your proposal * short abstract (one or two paragraphs) * duration (at least 15 minutes and no longer than 40 minutes) * your full name * your short bio You can specify your preferred time slot of your proposal and any other relevant information. The communication language of the devroom is English. Please note that the devroom has been allocated only a half of a day this year. Therefore the final decision on the duration of the talks will be made by the devroom organizers based on the number of accepted proposals. The official devroom schedule (along with the accepted talks) will be announced on December 15th 2023 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will be published on the FOSDEM web site, too. About the Devroom Since the first Microkernel OS Devroom at FOSDEM 2012 [4], this devroom has been a part of each following FOSDEM (with slight variations of the name). The focus gradually widened to include component-based, unikernel-based and other operating systems. By now, it has become a somewhat institutionalized tradition for the open source operating systems community, a kind of "extended family meeting" and it is one of the places where microkernel and unikernel enthusiasts meet regularly. To this date, over two dozen projects have participated in one way or another. Many of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. As every previous year, the devroom will offer the "stage" both to established community members and to newcomers. We like to select the talks in an inclusive manner, while staying true to the main technical topics (system-level software, broadly speaking) and creating a balanced and unbiased schedule. We would like to keep the quality bar of the devroom same as in the previous years. Presenting at FOSDEM implies that the recordings of the talks will be published under Creative Commons license by FOSDEM. By submitting a proposal, the speaker agrees to have the talk made available publicly indefinitely. For organizational purposes, we also need contact information of the speakers of accepted talks. Microkernel Dinner It has also become a habit that the devroom participants dine together somewhere in Brussels. The year 2024 will not be any different, so there is going to be a dinner on Saturday night. We will inform you about the exact arrangements later. About FOSDEM FOSDEM [5] is a two-day conference organized by volunteers to promote the widespread use of free and open source software. FOSDEM is widely recognized as one of the largest and best such events worldwide. FOSDEM covers a wide spectrum of free and open source software and hardware projects and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and proposals. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. In recent years, FOSDEM has been hosting more than 8000 developers annually at the ULB Solbosch Campus in Brussels, Belgium. The participation in FOSDEM is totally free, although the organizers gratefully accept donations and sponsorship. No registration is necessary. Attendees are expected to follow the [6]FOSDEM's code of conduct. Important Dates Recap * 2023-12-10: Deadline for proposal submission * 2023-12-15: Schedule published and speakers notified of acceptance * 2024-02-03: Devroom taking place Contact For any comments, questions and suggestions, please do not hesitate to use the devroom's mailing list [3] to contact the devroom organizers. The primary organizers of the devroom in 2024 are: * Martin Decky * Razvan Deaconescu References [1] https://fosdem.org/2024/ [2] https://pretalx.fosdem.org/fosdem-2024/cfp [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://archive.fosdem.org/2012/schedule/track/microkernel_os_devroom.html [5] https://fosdem.org/ [6] https://fosdem.org/2024/practical/conduct/

1 0

Re: Conclusions regarding speculation
by G. Branden Robinson 15 Nov '23

15 Nov '23

[re-send 2/2] ----- Forwarded message from "G. Branden Robinson" <g.branden.robinson(a)gmail.com> ----- Date: Mon, 13 Nov 2023 04:03:16 -0600 From: "G. Branden Robinson" <g.branden.robinson(a)gmail.com> To: devel(a)sel4.systems Subject: Re: [seL4] Re: Conclusions regarding speculation Hi Demi, At 2023-11-13T03:39:00-0500, Demi Marie Obenour wrote: > > The difference is QubesOS do not rely on a verified hypervisor while > > the hypothetical system I'm talking about it will have seL4 booting, > > which is a verified piece of code. > > I would love that, but seL4 currently is missing at least five > critical security features on x86: > > 1. Interrupt remapping in the IOMMU. This is the sort of thing that gets solved by putting together a small team of engineers, some very thick manuals from the manufacturer, a contact inside the vendor to address points "accidentally" omitted or erroneously documented, and a not insignificant amount of money. A Simple Matter of Programming, in other words. > 2. Protection against speculative execution attacks the moment the > embargo breaks. > 3. The ability to either choose the appropriate mitigations itself, > or to let userspace choose them. > 4. Properly implemented speculative execution mitigations. These 3 seem to be what you and Gernot are arguing about and I feel unqualified to get into the middle of that. > 5. Microcode update support. This is like (1) except it will never happen with verifiability and reliability because that would either expose, or enable the replacement of, the "secret sauce", by which the profit margin on the chip is protected. And that is why we need fully open cores subject to third-party correctness verification. I've never even seen an argument that you can combine these properties with binary blobs or trade secrets. And as long as that is true we're sure to keep getting trashed by spec ex attacks or the next great innovation in system compromise. > Without all five of these, seL4 is _less_ secure than Xen, which > defeats the entire purpose of using it. As per the discussion in > https://github.com/seL4/seL4/issues/1108 this will not be fixed any > time soon. I may not be completely understanding your argument, but it sounds like you're saying that with Xen/QubesOS you essentially achieve compartmentalization by partitioning one process (in the Unix sense) per processor (in the cores plus shared caches sense). Once you do this, doesn't it start to look a lot like OpenVMS? This would initially be a good way to drive the KVM-switch-in-a-laptop into the market but I think it would run into scaling problems pretty quickly. > That’s why I asked about desktop-class hardware I can actually buy: > the only non-x86 desktop-class hardware I know of are Macs with Apple > silicon and POWER9 machines from Raptor, ...insanely expensive (5 figures USD) last I looked... And Apple won't give up secret sauce of any kind before the extinction of our species. They still curse John Sculley's name. > and seL4 supports neither. > Apple silicon has lots of nonstandard IOMMUs that seL4 would need to > support, and POWER is not supported at all. For the time being, we are simply screwed. We are the cows from which economic rents are milked; this pleases the Street. The only rescue from our plight is Joseph Schumpeter's "creative destruction", opinions of which seem to vary in a consistent way depending on one's temporal distance from an IPO. > (Fun fact: you probably have some formally verified cryptographic code > installed on your system _right now_, since NSS uses fiat-crypto for > some of its cryptographic primitives last I checked.) ! Share a link next time. :) > To be clear: I don’t fault seL4 for focusing on embedded right now. > The reward/effort ratio is vastly more favorable there. That, and I think the larger players in the industry perceive potential risks to the status quo. The promise of lower expenses down the road due to fewer security incidents is a really hard thing to quantify, and much decision making is tied to what can be said in the next quarterly 10-C filing with the SEC. Yes, Heartbleed can give you heartburn big time. But sufficiently large and reliable income streams salve any scald. Quality of implementation is simply not the sort of thing anybody on the financial side of any firm cares about unless it's as dramatic as an airplane falling out of the sky. (I would have said "or life support equipment not being fit for purpose", but that appears not to be the case.[1][2]) > Servers are significantly harder and I suspect desktops and laptops > are the worst-case scenario, because _everything_ is dynamic and > subject to the whim of a human who can and will break any simplifying > assumptions one has made. And this is even before one starts talking > about GPUs and other accelerators, which are a huge attack surface and > yet can be the difference between a system being usable and unusable > for the tasks people expect of it. There is a reason Qubes OS is > going to be supporting GPU acceleration at some point. > > That’s why I am so pessimistic about time protection on desktop: all > of the stuff I have read about it assumes at least some static > partitioning, and in the desktop world, static _anything_ simply > doesn’t exist. I think it's bad, but maybe not quite as bad as you do. I'm going to risk coming off as naïve for a moment. Or saying a bunch of stuff you (or everyone on this list) already knows. Getting back to CS 101 fundamentals, what does a computing system do? A. It computes things (runs instructions). B. It remembers things (has storage). C. It communicates with the world (performs I/O operations). Time division multiplexing is our solution to (A) and (C) when we have more things we want to compute and communicate than we have machine resources for. This is well-studied and reasonably well controlled. We tried cooperative multitasking; it didn't work out because we couldn't solve the halting problem (but mainly because programmers are not infallible). Fine. Limited bandwidth and measurable latencies are so pervasive that we _assume_ unreliability of all I/O (but largely hide it inside network stacks or bus protocols). That leaves (B). So the dynamic system problem boils down to the multiplexing of memory. And I venture that is mainly a problem because when DEC added virtual memory to the PDP-11 and the Berkeley CSRG rewrote the Unix kernel to use it (thus "vmunix"), we all fell into a trap. That trap has a name. Memory overcommit. Your userland application can't overcommit CPU cycles. You'll get preëmpted. You can't overcommit I/O, either; something will throttle you. So we've spent a few decades being fantastically reckless with memory, especially in C and C++. (And, worst of all, JavaScript, according to my htop(1).) Running out of memory was never supposed to be problem in real life; rare enough that, if you were a slouch, you used the return value of malloc/calloc/realloc without thinking, and if you weren't, you just fatal-errored out, proclaiming defeat. I expect that the next generation will start breaking the wretched habit of assuming unbounded memory availability. Here's why. We (desktop users) drastically under-use all these parallel cores in our systems. If we were to partition memory consumption at the application level for large problems, we could more easily apply divide-and-conquer strategies to them. This is not a new insight. "MapReduce" was a buzzword 20+ years ago. As often happens, stuff that got figured out at the "enterprise" level last generation trickles down to the desktop for this one. This time maybe we can do better than J2EE. So, as I see it, the solution to the "insanely dynamic system" problem is to stop being insane. Accept a bound on memory consumption. Stop overcommitting memory, which already causes frustrating problems.[3] Use something like Massif[4] to profile your heap usage. Ask for as much as you will need at process launch, or refactor your memory-hog functions to work within one or more smaller arenas. See what happens. Yes, some stuff that never used to crash will start crashing because its authors didn't bother writing with highly parallel systems in mind, or assumed that memory was infinite. We also used to watch things crash because people treated pointers and ints as equivalent. I'm old enough to remember the DEC Alpha teaching a lot of hard lessons in this area (and also with respect to unaligned memory accesses). We learned. Now, we will slowly learn to stop asking for more than we need, and how to carve up the memory arenas we use. We also may continue our slow migration away from worse-is-better behemoths like C/C++ and Unix kernels. Am I wrong? Could be. Point me to reading material. I try not to talk too much on this list. Tonight I reckon I blew through my quota for the year, and I still had something I wanted to post from the summit... :-| Regards, Branden [1] https://www.fiercebiotech.com/medtech/getinge-life-support-systems-temporar… [2] Take note of the dates mentioned in article [1] and compare it with the five-year share price history of the manufacturer. https://www.google.com/search?q=getinge+share+price If you'd bought in when the first recall started in "late 2020" and held ever since, you would not have lost money. And in fact you could have cashed out with 100+% profit in the second half of 2021. [3] https://lwn.net/Articles/668126/ [4] https://valgrind.org/docs/manual/ms-manual.html ----- End forwarded message -----

1 0

Re: Conclusions regarding speculation
by G. Branden Robinson 15 Nov '23

15 Nov '23

[sending a revised verison of this and one other message; Peter was able to confirm that the earlier ones got lost somewhere between exim and mailman--maybe my GPG signature attachment caused problems, so leaving that off] ----- Forwarded message from "G. Branden Robinson" <g.branden.robinson(a)gmail.com> ----- Date: Mon, 13 Nov 2023 02:51:36 -0600 From: "G. Branden Robinson" <g.branden.robinson(a)gmail.com> To: devel(a)sel4.systems Subject: Re: [seL4] Re: Conclusions regarding speculation At 2023-11-13T08:55:47+0100, Hugo V.C. wrote: > > One might as well just buy multiple laptops and be able to use them > > at the same time. > > *** You can not easily travel with multiple laptops and it is not a > comfortable solution, nor you can sell this idea to anyone. > Instead you can travel with a single laptop with 3 different computing > platforms inside, basically, the user will never know, it will be > transparent. When I was at TS we had a demo system that manifested this sort of partitioning, but I think it furthermore used a windowing system. The project was no longer under development while I was working there--probably it wasn't being actively funded--but the proof of concept seems to have been delivered. It may have had only two tiers, "red" and "black", with the former a data sink only (apart from what your eyeballs could see) and the latter a source and sink. Pretty sure someone else on the list can correct me and say more. (I want to say it was called MDDC? "Multi-Domain Display Controller"?] My other thought is that we're basically talking about putting a KVM ("keyboard/video/mouse", not "kernel virtual machine" :) ) switch inside a chassis with cores, storage, and peripheral ports. That doesn't seem like it should be too hard.[0] The physical dimensions of KVMs seem to be dominated by the sizes of the connectors attached to them. Not an issue inside a chassis. Economically there is a reason to expect this to come to pass as well; with the death of Moore's Law, I submit that we buy multicore CPU packages not because we use them efficiently--I don't, except when running "make -j", and that's a tiny fraction of my interaction time--it is because CPU vendors desire to keep the price point of the minimum configured processor model for consumer machines around USD 100. I guess some kind of commodity market dynamics are thought to set in somewhere below that point, and such dynamics are threatening to the U.S. consumer-facing semiconductor duopoly. (Vertical integration is a classic defense against having to participate in this sort of competition, and is consistent with Apple's in-housing of CPU design and manufacture.) As innovations go, this could be a benign one, and a real improvement if we seize the opportunity on the OS side. (We still need a capability-based OS and, as Hugo points out, a formally verified network stack.) Here's an amusing proof of concept with a mightily retro hardware/software stack. But if a hobbyist can do this in his garage... "Meet the ZedRipper – a 16-core, 83 MHz Z80 powerhouse as portable as it is impractical." http://www.chrisfenton.com/the-zedripper-part-1/ Aside: Just over the past couple of weeks, glibc and other libc implementers have held an open conversation with the Linux man-pages maintainer such that they're seriously trying to get the best available information to C programmers about how to perform the seemingly simple operation of copying strings, and why the silver bullets that have been touted to date, aren't.[1] For decades our industry has labored under the harmful myth that the standard C library, even as it existed in ANSI C89, was perfectly good enough for this, and if you screwed up it was because you're a bad programmer, not because C's infamously weak type system and silly selection of return values in its library[2] laid down a minefield for you to traverse. Rust has caught fire despite all the money Google has thrown at Go,[3] and a few people (not just me, I promise) even remember and point out how Ada got a lot of stuff right 40 years ago that the "close-to-the-metal"/portable-assembly school of hacking keeps getting pwn3d by.[4] gnulib is adding CHERI support as we speak.[5] I don't personally prefer CHERI to using a better language than C/C++ (and ISA than x86) from the ground up, but it is a serious and honest attempt to face the problems with C that code cowboys have waved aside for decades. Could our industry be--at long, long last--tiring of crap security? May it be. By all means put a KVM switch in an 8-package/64-hart RISC-V 64 laptop. I promise not to block the vent. Regards, Branden [0] This is how you know I'm not a hardware guy. [1] https://lore.kernel.org/linux-man/ZU4SDh-Se5gjPny5@debian/T/#mfb5a3fdeb3548… [2] https://www.symas.com/post/the-sad-state-of-c-strings [3] An oft-heard rebuttal to this observation is that Google wasn't/isn't really trying to target the same applications as Rust. That sounds like post hoc sour grapes. It's Google. They put Thompson and Pike on this. They were shooting for the moon. [4] https://lwn.net/Articles/919016/ [5] https://git.savannah.gnu.org/cgit/gnulib.git/log/ ----- End forwarded message -----

1 0

[RFC] Support CHERI/Morello in seL4
by Hesham Almatary 13 Nov '23

13 Nov '23

Hello, I have started working on porting seL4 to CHERI/Morello. Part of that, and as a first step, I submitted an RFC [1] as we aim to ideally upstream this work to make it reusable by others and allow collaborations. Any feedback or comments will be appreciated, happy to discuss further. For those who don't know me, I have worked on seL4 at the TS group from 2016-2018, during which I added FPU and SMP support to the Armv7 32-bit port, and added the RISC-V port. I then did my PhD on "CHERI compartmentalisation for embedded systems." [1] https://sel4.atlassian.net/browse/RFC-15 Regards, Hesham

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 13 Nov '23

13 Nov '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Nov 15, 5pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Where are the interrupts disabled in the kernel mode?
by chenpingyuan＠xiaomi.com 09 Nov '23

09 Nov '23

Hi experts, The sel4 whitepaper says "seL4, like most members of the L4 microkernel family, executes with interrupts disabled while in kernel mode.". But I didn't find the code which disabled interrupts when entering kernel mode, for example, when a syscall is triggered. Can anybody help to point out? Thanks.

2 4

Reminder seL4 developer hangout
by Birgit Brecknell 30 Oct '23

30 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Nov 1, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Camkes-vm-linux tutorial
by felicianidaniele＠gmail.com 26 Oct '23

26 Oct '23

Hi, I modified the vm_tutorial.camkes file to obtain two VMs. It works but I would like to see the two virtual machines on two different consoles. Is it possible? Thanks Daniele

1 0

vm-minimal on raspberry pi4
by felicianidaniele＠gmail.com 19 Oct '23

19 Oct '23

Hi everyone, I would like to run vm-minimal and vm-multi (camkes-vm-manifest repo) on raspberry pi 4 4gb RAM. Can someone help me? Thanks Daniele

1 0

Running Sel4 on Rasberry pi 4 4 gb RAM
by felicianidaniele＠gmail.com 18 Oct '23

18 Oct '23

Hello, i'm trying to upload seL4 ( seL4test-driver-image-bcm2711 image) on raspberry pi 4 but i'm encountering two different errors: 1. If I follow the website procedure and upload the sel4test image into the address 0x10000000 the error is : “Reading file would overwrite reserved memory” 2. If I try to upload the image into 0x1000000 I read the following error: “sel4 failed assertion ‘isSchedulable(candidate)’ at /kernel/thread.c can someone help me? Thanks Daniele

2 2

Help with navigating the l4v repository
by Typaldos, Athanasios 18 Oct '23

18 Oct '23

Hello, I am from Lin Zhong’s group at Yale University and I am currently looking at the seL4 specifications and proofs. I am interested in finding the invariants at the abstract level regarding the capability management (CNode and CSpace). I would need some help with navigating the repository, because I am relatively new to interactive theorem proving in general. - I think what I am looking for is in the `l4v/proof/invariant-abstract` directory inside the `{CNode, CSpace}*_AI.thy` files. Is this correct ? - How can I distinguish between helper lemmas and the invariants that you state for example in your paper: SeL4: formal verification of an OS kernel<https://dl.acm.org/doi/10.1145/1629575.1629596> ? - Is there any textual artifact that lists the invariants in prose that could help me ? - Can you clarify me the relationship between the specifications in `l4v/spec/abstract` and the proofs in `l4v/proof/invariant-abstract` ? According to my understanding, the abstract specification defines the system in the abstract level, whereas the proofs use these definitions from the specifications to prove properties and invariants about them. So, the invariants are the statements that the proofs prove. Am I on the right track ? Thank you for your help, Thanasis Typaldos

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 16 Oct '23

16 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Oct 18, 5pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Incorrect dtb in the Microkit tutorial
by Luke Hart 09 Oct '23

09 Oct '23

Hello, It seems that the linux.dtb file supplied with the tutorial code is not correct and does not allocate enough memory for the initrd. The symptoms this issue caused when attempting to run part4 was that the libresolv.so.2 could not be opened and the vmm panic'ed. The linux.dtb supplied in the 'solution' folder in the git repository has 'initrd-end' set to a larger value and this version does work. Thanks, Luke

2 1

Re: The seL4 Microkit tutorial is now available
by Isaac Beckett 05 Oct '23

05 Oct '23

> Date: Wed, 4 Oct 2023 06:36:02 +0000 > From: Ivan Velickovic <i.velickovic(a)unsw.edu.au> > Subject: [seL4] The seL4 Microkit tutorial is now available > To: devel <devel(a)sel4.systems> > > Hello everyone, > > For those who are new to seL4 or want to learn about the seL4 Microkit, the Microkit tutorial is now available to everyone on the Trustworthy Systems website: https://trustworthy.systems/projects/microkit/tutorial/welcome.html. This is the same tutorial that ran at this year’s seL4 Summit. > > The tutorial code and infrastructure is also open-source, available here https://github.com/au-ts/microkit_tutorial. Feel free to provide feedback or ask questions there. > > Thanks, > Ivan Hello, I was going to ask what Microkit was and how it differs from seL4 Core Platform, but I see it’s just a new name. That’s good to know. I’ll definitely be checking out that tutorial Also, where can I find information on comparison between CAMmkES and Microkit/seL4cp? I only have a vague idea of the difference between the two. Thanks, Isaac

2 1

The seL4 Microkit tutorial is now available
by Ivan Velickovic 04 Oct '23

04 Oct '23

Hello everyone, For those who are new to seL4 or want to learn about the seL4 Microkit, the Microkit tutorial is now available to everyone on the Trustworthy Systems website: https://trustworthy.systems/projects/microkit/tutorial/welcome.html. This is the same tutorial that ran at this year’s seL4 Summit. The tutorial code and infrastructure is also open-source, available here https://github.com/au-ts/microkit_tutorial. Feel free to provide feedback or ask questions there. Thanks, Ivan

1 0

Re: [oss-security] Xen Security Advisory 439 v1 (CVE-2023-20588) - x86/AMD: Divide speculative information leak
by Solar Designer 04 Oct '23

04 Oct '23

On Tue, Sep 26, 2023 at 09:59:19PM -0400, Demi Marie Obenour wrote: > These detailed security advisories are one of the things I love about > Xen. It's hard to trust a hypervisor (KVM) that will not issue them, > for then one has no way to know if a particular problem got fixed. I concur. I'd appreciate security advisories from the KVM project. > I'm CCing KVM here to make sure they have a fix. From their Git commit > history, I am almost certain that seL4 does not. I'm CCing the seL4 > developers to alert them of this and suggest that the x86 port be > removed or at least have a big warning. I strongly oppose removal of a port/support for a certain architecture just because some implementations of it are/were problematic. Adding a warning is fine. Alexander P.S. Demi Marie, please note that oss-security list content guidelines explicitly discourage CC'ing other lists(*), and Xen advisories are already stretching this. In this reply, I am still CC'ing many of what you had CC'ed as I am following up on your specific points relevant to those lists, but in general let's be more careful about this. (*) Because we may then get off-topic follow-ups from there, especially if CC'ing project user lists or high-volume lists like LKML. In this specific case, we're lucky so far.

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 02 Oct '23

02 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Oct 4, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Add GICv3 emulation support for vmm on arm platform
by colorglass4＠outlook.com 27 Sep '23

27 Sep '23

Hi, I am trying to run a guest Linux using seL4's vmm library on the rk3568 platform, which uses gicv3 as its irq controller. But there is only gicv2 emulation officially supported in the vm library. I did find that there are 2 "gicv3" branch of the repository, but they are all outdated and have not being maintained for a long time. Is there any plan to formally add the gicv3 support to vmm library? Thanks.

2 3

Sel4 VMM on zcu102
by An,Jianjun 26 Sep '23

26 Sep '23

Hi I have run sel4 on the development board of zcu102. I found on the official website that the camkes-vm project does not support the platform zcu102. Could you please give me some guidance to make the functions of this vmm run and run a linux on the guest. Thanks

2 4

Bug on sel4 rootserver?
by chenpingyuan＠xiaomi.com 12 Sep '23

12 Sep '23

Hello guys, I'm trying to run sel4 using qemu under macosx, but it looks crash happened(Same steps were done on Ubuntu, but nothing bad happened.). More info: I'm following the doc here with docker as the build environment: https://docs.sel4.systems/GettingStarted.html Any tips are appreciated. Logs: chenpingyuan@in-container:/host/sel4_arm64/build_aarch64$ ./simulate ./simulate: QEMU command: qemu-system-aarch64 -machine virt -cpu cortex-a53 -nographic -m size=2G -kernel images/sel4test-driver-image-arm-qemu-arm-virt Not in hyp mode, cannot reset CNTVOFF_EL2 ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[40a27000..40eed0b7] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 40b61eb8. Loaded DTB from 40b61eb8. paddr=[4023d000..4023efff] ELF-loading image 'kernel' to 40000000 paddr=[40000000..4023cfff] vaddr=[ffffff8040000000..ffffff804023cfff] virt_entry=ffffff8040000000 ELF-loading image 'sel4test-driver' to 4023f000 paddr=[4023f000..40634fff] vaddr=[400000..7f5fff] virt_entry=40e568 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. available phys memory regions: 1 [40000000..80000000] reserved virt address space regions: 3 [ffffff8040000000..ffffff804023d000] [ffffff804023d000..ffffff804023ed11] [ffffff804023f000..ffffff8040635000] Booting all finished, dropped to user space Caught cap fault in send phase at address 0 while trying to handle: unknown syscall 0x476dcc in thread 0xffffff807ffca400 "rootserver" at address 0x460964 With stack: 0x6e3ca0: 0x466a53 0x6e3ca8: 0x460b84 0x6e3cb0: 0x457474 0x6e3cb8: 0x0 0x6e3cc0: 0x6e3f30 0x6e3cc8: 0x0 0x6e3cd0: 0x0 0x6e3cd8: 0x4433f0 0x6e3ce0: 0x0 0x6e3ce8: 0x0 0x6e3cf0: 0x0 0x6e3cf8: 0x0 0x6e3d00: 0x0 0x6e3d08: 0x0 0x6e3d10: 0x0 0x6e3d18: 0x0

2 2

2 weeks left before the seL4 summit; there's still time to register
by June Andronick (seL4 Foundation) 06 Sep '23

06 Sep '23

The seL4 summit 2023 will start in 2 weeks in Minneapolis! There is still time to register if you haven’t done it yet. Summit: https://sel4.systems/Foundation/Summit/2023/ Register: https://events.linuxfoundation.org/sel4-summit/register/ Program: https://sel4summit2023.sched.com/ See you there!

1 0

next seL4 TSC meeting on Tue 12 Sep (Mon 11 Sep in US)
by Gerwin Klein 04 Sep '23

04 Sep '23

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Tue, 12 Sep, 4pm - Central Europe: Tue, 12 Sep, 8am - US West Coast (LA/SF): Mon, 11 Sep, 11pm See also the seL4 calendar feed available from here: https://sel4.systems/contact/home.pml The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/85916669769 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - action items form last meeting - discuss and vote on RFC-5 (The seL4 Core Platform) - discuss and vote on adding the seL4 Rust support repositories currently at https://github.com/coliasgroup/rust-seL4 to the seL4 GitHub org. - discuss steps for the next seL4 release - if there is time: discuss remaining open RFCs If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 04 Sep '23

04 Sep '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Sep 6, 8am For your time zone, please see the 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 2pm-5pm Fri 9am-5pm

1 0

Standalone experiments
by sean bruno 01 Sep '23

01 Sep '23

I'm investigating some of the different microkernels out there for some graduate exploration. The tutorials were awesome and got me bootstrapped *very* quickly, thank you for the effort on those. I am attempting to build a "hello-world" on my own and seem to be missing a step as base.cmake no longer can see the musllibc that I have in my tree. I'm fairly certain my CMake knowledge here is weak or I just flat out missed a step. My checkout tree looks like the following: $ tree -L 1 ├── build ├── CMakeLists.txt -> tools/cmake-tool/default-CMakeLists.txt ├── init-build.sh -> tools/cmake-tool/init-build.sh ├── kernel ├── projects ├── README.md └── tools $ tree -L 1 projects/ projects/ ├── hello-world ├── musllibc ├── seL4_libs └── util_libs When cmake runs from build, I see the following: ~/build]$ cmake -DCROSS_COMPILER_PREFIX=aarch64-linux-gnu- -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -C ../kernel/configs/AARCH64_verified.cmake ../projects/hello-world/ loading initial cache file ../kernel/configs/AARCH64_verified.cmake -- The C compiler identification is GNU 12.1.1 -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /usr/lib64/ccache/aarch64-linux-gnu-gcc - skipped -- Detecting C compile features -- Detecting C compile features - done -- The CXX compiler identification is GNU 12.1.1 -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /usr/lib64/ccache/aarch64-linux-gnu-g++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/lib64/ccache/aarch64-linux-gnu-gcc -- /home/sbruno/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating from DTB... WARNING:root:Only mapping 4096/16777216 bytes from node /iommu@12000000, region 0. Set kernel_size in YAML to silence. -- CPIO test cpio_reproducible_flag PASSED CMake Error at /home/sbruno/tools/cmake-tool/base.cmake:55 (find_package): By not providing "Findmusllibc.cmake" in CMAKE_MODULE_PATH this project has asked CMake to find a package configuration file provided by "musllibc", but CMake did not find one. Could not find a package configuration file provided by "musllibc" with any of the following names: musllibcConfig.cmake musllibc-config.cmake Add the installation prefix of "musllibc" to CMAKE_PREFIX_PATH or set "musllibc_DIR" to a directory containing one of the above files. If "musllibc" provides a separate development package or SDK, be sure it has been installed. Call Stack (most recent call first): CMakeLists.txt:4 (include) -- Configuring incomplete, errors occurred!

2 1

CPU design, Re: Confidentiality and realtime requirements
by Isaac Beckett 27 Aug '23

27 Aug '23

> Date: Sun, 13 Aug 2023 16:18:08 +0000 > From: Gernot Heiser <gernot(a)unsw.edu.au> > Subject: [seL4] Re: Confidentiality and realtime requirements > To: devel <devel(a)sel4.systems> > >>>> On 12 Aug 2023, at 02:07, Demi Marie Obenour <demiobenour(a)gmail.com> wrote: >>>> >>> If you want to relax this, you’ll need a very careful analysis of your security requirements, and deploy TP where needed and omit where it’s not needed. But you can't prevent µarch timing channels without TP. Everybody knows about D-cache channels these days and how easy they are to exploit, and similar with LLC channels. And if you want to prevent at least those, then full TP has no extra cost. >> >> Does time protection require temporal isolation? > > Nope. Time protection is the mechanism that allows providing temporal isolation. > >>> Developing such a framework is on my agenda (it’s a core part of what I said I’m waiting for a good PhD student to work on). Basically I want to be able to make certain security guarantees where components have overt communication channels. An example is tab isolation in a browser: We want to have a fully functional web browser that allows processing of sensitive information in one tab, but guarantee that it cannot be leaked to a different tab. >> >> Another good example is different apps on a mobile device. Android allows any two applications on the same profile to communicate with mutual consent, and yet also allows one application to keep information secret from another. > > Yes. The smartphone space is really interesting. While built on top of the classical Unix security model (but implementable on a much simpler model) it demonstrates that stricter security policies (compared to desktops) can be made acceptable to users. > >> One critical requirement is that such a framework must allow an efficient implementation, both in terms of performance and power consumption. If it isn’t efficient enough to be deployed, then it won’t do people any good. > > Energy is (to first order) proportional to computation, so just looking at “performance” is good enough. > > And performance has always been our driver – see “security is no excuse for bad performance!” ;-) > > As I argued earlier, the performance cost of time protection is not higher than what you need to eliminate just the most easily exploitable cache channels. > > Gernot This makes me wonder if it’d make sense to design a new CPU and/or instruction set with the goal of eliminating timing and other side channels. Like, we had the Lisp machines with hardware support for Lisp, and now most CPUs are optimized for C and similar languages, and in turn those languages are optimized for those CPUs (x86, Arm, etc.). But I can’t say I know enough about computer science at this time to even tinker with the idea. And also, on the other hand maybe it doesn’t make sense to create hardware and accompanying software that are nearly impossible to non-destructively subvert, given the concerning trend of computer manufacturers and tech companies of restricting what code can run on their products. I don’t want to make something that could be set up to prevent an end user from modifying or running their own code. Isaac

4 9

How to understand seL4?
by Jason Long 24 Aug '23

24 Aug '23

Hello,I want to learn seL4 deeply. So that I can figure it out and develop it. Where should I start? Thank you.

2 1

How to enable SMP on qemu-arm-virt
by chenpingyuan＠xiaomi.com 21 Aug '23

21 Aug '23

Hello cool guys, I'm trying SEL4 using qemu-arm-virt platform with command： ../init-build.sh -DPLATFORM=qemu-arm-virt -DSIMULATION=true I noticed that SMP was not enabled by default, so I added: set(KernelMaxNumNodes "4") into kernel\src\plat\qemu-arm-virt\config.cmake. After running it with command ./simulate , I got the following error log and seL4 refused to continue: HVC is not supported for PSCI! My question is how shall I change the build scripts in order to run seL4 with SMP on qemu-arm-virt platform. Regards

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 21 Aug '23

21 Aug '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Aug 23, 5pm For your time zone, please see the 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 2pm-5pm Fri 9am-5pm

1 0

A desktop OS based on seL4
by Jason Long 19 Aug '23

19 Aug '23

Hello,Is there an operating system that uses seL4 as a kernel and is suitable for home or server users like GNU/Linux or Windows OS? Thank you.

2 2

sel4cp and networking driver
by Sid Agrawal 14 Aug '23

14 Aug '23

Hi, I would like to setup a working example on sel4 with picoTCP and an eth driver. I came across this [1] from one of the seL4CP/sDDF demos and [2] from the camkes examples. However, I do not have access to those particular boards. I have a rspi4 and a Toradex Colibri iMX8X module with the aster carrier board. This Toradex has the same SoC ( iMX8X) as the tqma8xqp-1gb mentioned on the sel4cp website. Do you folks have any thoughts on how much effort it is getting seL4 working on "Toradex Colibri iMX8X" given it is supported on "tqma8xqp-1gb" which has the same SoC? I do not mind buying a specific development board as long as I know that I can use it for a while :) For folks who are working on sel4cp, what kind of dev setup do you have? I am looking for basic conveniences like flashing the image via USB (so I do not have to add/remove an SD card), TFTPboot, and some simple device drivers. I did see the instructions on TFTPbootat [3]. However, does it matter if the image was built via the sel4test of sel4cp? I think not, but I just wanted to double-check. And lastly, a higher-order question about seL4cp. How does sel4cp tie into the example in seL4_Libs [3], which has barebones libc and a VMM? Which is what I have used so far with sel4test. I understand that both sel4cp and camkes are for static systems, but I thought that I could use sel4cp to start some initial processes, such as a driver, a memory server, and some management processes. And later use process_spawn from seL4 libs to start additional PDs. Best, Sid [1] https://github.com/lucypa/sDDF [2] https://github.com/seL4/global-components/tree/master/components/Ethdriver/… [3] https://docs.sel4.systems/Hardware/GeneralARM

4 10

Confidentiality and realtime requirements
by Demi Marie Obenour 14 Aug '23

14 Aug '23

One of the goals of the MCS scheduler is to allow untrusted parts of the system (such as device drivers) to still have low interrupt latency. However, this seems to interact badly with the domain scheduler, as interrupts can arrive when the domain that will serve them is not scheduled. Worse, it appears that interrupts will generally require an IBPB (or equivalent) on both entry and exit, since they may interrupt any code. Is this accurate? If so, it seems that the “flush all μArch state” instruction coming to some RISC-V CPUs is insufficient, and full speculative taint tracking is required. More generally, requiring mutually distrusting domains to be explicitly marked seems to be problematic for anything that is not a static system: in a dynamic system (one that can run third-party code), one must typically assume that different address spaces are mutually distrusting, with the result that IPC latency will be severely impacted. Am I missing something, or will a general-purpose OS need full speculative taint tracking in hardware if it is to have fast IPCs between mutually-distrusting code on out-of-order CPUs? -- Sincerely, Demi Marie Obenour (she/her/hers)

3 13

Changing the cspace of a TCB while it is listening on a EP
by Sid Agrawal 08 Aug '23

08 Aug '23

Hi, I have a scenario and would like to understand how the kernel is expected to behave when I change the CSpace of a TCB when it is blocked on an EP. 1. A TCB (say TCB_1) is blocked on seL4_reply() on an endpoint (say EP_1). 2. Now, another PD, which has the capability to TCB_1, changes the CSpace of TCB_1 by using seL4_TCB_SetSpace(). Let's assume that the VSpace is identical. This new CSpace can be different from the old CSpace in 4 ways: A. It doesn't have the endpoint EP_1 B. It has the endpoint EP_1 but at a different CSlot. C. It has the endpoint EP_1 at the same CSlot. But since it is a different CSpace(so CNodes shared), it is a minted copy of the EP_1. Let's call it EP_1-prime. D. It has the endpoint EP_1 at the same CSlot, and it is the same EP as I have shared the CNode containing the EP_1 from the original CSpace. New and old CSpaces share the CNode containing that EP_1 like two trees sharing a sub-tree. I think scenario D should work as if nothing happened, but I do not know what to expect in scenarios A, B, and C. I will try these out soon, but I wanted your input as I did not find a clear answer in the manual. Best, Sid

2 2

Reminder seL4 developer hangout
by Birgit Brecknell 07 Aug '23

07 Aug '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Aug 9, 8am For your time zone, please see the 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 2pm-5pm Fri 9am-5pm

1 0

Ultra96V2 in sel4cp_VMM is cautiously here - initial support
by Nataliya Korovkina 06 Aug '23

06 Aug '23

Highlights, briefly... 1. Project "ultra96v2-sel4cpvmm" The project introduces changes to the three components: seL4, sel4CP, sel4cp_VMM. * Xilinx Linux booting requires SMC calls support in seL4. The project uses the SMC cap impelementation offered by DornerWorks (approved but not merged). * Changes in sel4CP relate to the new capability in seL4. * As for sel4cp_VMM, a policy of VM's SMC calls handling will be different from one VMM-PD to another. The project introduces registration of a custom handler by PD application as well as it provides the default handler - the simplest "pipe" passing calls and responses through. The project published as sets of patches to the components. More the details are in the README.md and Issue #1 - https://github.com/malus-brandywine/ultra96v2_sel4cpvmm/issues/1 of the project: https://github.com/malus-brandywine/ultra96v2_sel4cpvmm 2. Project "petalinux-ultra96v2-sel4cpvmm" The project enables generation of linux image and minimal rootfs to run VM with sel4cp_VMM. More details are in README.md of the project: https://github.com/malus-brandywine/petalinux-ultra96v2-sel4cpvmm Status: Linux VM loads to login prompt

1 0

2 weeks left to get the early-bird registration at the seL4 summit
by Birgit Brecknell 04 Aug '23

04 Aug '23

2 weeks left to get the early-bird registration at the seL4 summit! A friendly reminder that the early bird cut-off date is 18 August 2023. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and Dinner Registrations: https://events.linuxfoundation.org/sel4-summit/register/ seL4 summit 2023: https://sel4.systems/Foundation/Summit/2023/<https://sel4.systems/Foundation/Summit/2023/> --- 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 2pm-5pm Fri 9am-5pm

1 0

CMake error “Variable 'KernelArch' is not set.” Happens when building RISCV based seL4 system.
by sueboxian＠gmail.com 25 Jul '23

25 Jul '23

Hi, I met a CMake error, “Variable KernelArch is not set” when I tried to build a seL4 project based on the open source code of the UNSW course, Advanced Operating System, aka. AOS. The original version uses odroidc2 as the building platform, and I want to build it with the riscv gnu toolchain and simulate it on qemu-riscv-virt. Here is the repository: https://github.com/SEL4PROJ/AOS-manifest The building hierachy is as the basic build system structure, with init-build.sh, setting.cmake and CMakeLists.txt in the top level. And the top level contains kernel, tools, and project folders, in which there are CMakeLists.txt and .cmake files. Since I have no experience on cmake, I tried to compare the manifest xml between AOS project and seL4test project. I found that the major difference between them are in “init-build.sh”, “setting.cmake” and the “CMakeList.txt” in the top level. There are also some unused libraries in AOS project. I tried deleting the “set PLATFORM odroidc2” command in the setting.cmake, and added the DCROSSCOMPILER=riscv-unknown-linux-gnu, DPLATFORM=qemu-riscv-virt in the build command. But they doesn’t work. After checking the “/kernel/configs/seL4Config.cmake”, it says that the error is caused since KernelArch is left as empty string… And I want to ask whether I have set anything improperly.... I will appreciate for any help. Thank you for reading my question!

3 2

Reminder seL4 developer hangout
by Birgit Brecknell 24 Jul '23

24 Jul '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jul 26, 5pm For your time zone, please see the 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 2pm-5pm Fri 9am-5pm

1 0

Soft-float problem happens when building seL4test using riscv64-unknown-linux-gnu-gcc toolchain
by sueboxian＠gmail.com 15 Jul '23

15 Jul '23

Hi, I met a problem when building seL4test project with riscv toolchain, with the float operations compiled as soft-float. Here are my configuration commands:  python3 ~/bin/repo init -u https://github.com/seL4/sel4test-manifest  python3 ~/bin/repo sync  mkdir build-riscv  cd build-riscv  ../init-build.sh -DPLATFORM=qemu-riscv-virt -DCROSS_COMPILER_PREFIX=riscv64-unknown-linux-gnu- -DSIMULATION=TRUE  ninja The terminal reported "can't link double-float modules with soft-float modules" errors when compiling fpu.c, and thus stopped compilation. I have tried rebuilding the glibc version riscv toolchain, with multilib enabled. But it doesn't work. I also checked the terminal, it says that I'm compiling with march=riscv64imac_zicsr_zifencei -mabi=lp64, which as the best of my knowledge, means compiling the float as soft-float. I want to know whether I lossed something. I would appreciate for any help. Thanks in advance.

3 6

Reminder seL4 developer hangout
by Birgit Brecknell 10 Jul '23

10 Jul '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jul 12, 8am For your time zone, please see the 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 2pm-5pm Fri 9am-5pm

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 23 Jun '23

23 Jun '23

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

1 0

Bitfield generator EBNF grammar
by June Tate-Gans (ジューン) 07 Jun '23

07 Jun '23

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

3 5

question about sel4 kernel preemptionPoint
by yadong.li 05 Jun '23

05 Jun '23

Hi: I have one question about sel4 kernel preemptionPoint on smp platform such as ARMv8. Take an example, when kernel takes long time to clear memory when UntypedRetype kernel object on core1, it will check preemptionPoint, when pending IRQ exists on core1, it will handle this irq, and return to userspace let other syscall or cores such as core2 have chance to run, but irq pending only check current cpu(PerCPU), no all cores of smp system, if core1 execute long seL4_Untyped_Retype syscall, core2 has a pending irq, the pending irq will not be checked in current core1, it will block until the execution of long syscall is completed if we take no account of archtimer irq, This phenomenon looks inconsistent at the system level between signal core and mutil core I want to know the current design intent about preemptionPoint of archtimer interrupt and other peripheral interrupts on SMP platform, only take current core interrupt as soon as possible or give other core and high priority task a chance to entry kernel and take big kernel lock? Thanks for your help

2 1

seL4 Rust crates doc links broken
by Hugo V.C. 01 Jun '23

01 Jun '23

Hi all, was looking around the Rust crates to check what is available to play around with seL4 from Rust and just found that most interesting ones (sel4_sys, sel4-start, ...) have documentation pointing doc.robigalia.org which is a broken link. Looks like the only communication way to Robigalia is #robigalia IRC channel... (I don't use IRC since 90s, not used to it anymore...) so I'm publishing this info here as I bet those amazing developers are in this list too and can read this message: please 🙏 fix the link at crates.io. Beside this, I will never get tired of remember the importance of taking care of the "general public" (that is, common developers not familiarized with seL4, common companies that are not security nor technical gurus, etc... that is, the average potential user of seL4 in the future) so it has an "easy/friendly" approach to seL4 as an early adopter. For that reason, checking that (healthy) Rust environment is there available for everyone will be a good starting point. seL4 topic is complex enough with documentation, so without it becomes simply not usable (for humans... 😅). Hoping Robigalia amazing guys can read this here, thank you for your work on Rust, as this is the best interface to seL4 development for people living on this planet. Best,

1 0

porting to a new platform
by steve.burke.56＠gmail.com 01 Jun '23

01 Jun '23

I'm trying to port an old sel4 code base to the latest so I decided to take the sel4test manifest & work through through the following page (https://docs.sel4.systems/projects/sel4/porting.html) The old code base does not add the new platform the same way since the new code seems to have some new CMake macros that do most of the heavy lifting. Is there a test project that does this with an arbitrary platform that I can use as a reference? My platform defines don't seem to be coming through correctly. Is working through the porting page the best way to do and does it seem current? Thanks.

3 2

Reminder seL4 developer hangout
by Birgit Brecknell 29 May '23

29 May '23

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

Ring 3 iopl is going away, seL4 is ok
by William ML Leslie 21 May '23

21 May '23

Hello, I just noticed in the new x86-S rfc that Intel published that there will be no further support for io port access for processes in ring 3. Thankfully, this doesn't look like it will impact seL4, which provides capabilities to special objects representing port ranges on x86, which are then implemented in the kernel. Just in case anyone was wondering if there will be any impact, since this is the one thing that stuck out to me. Here's Intel's RFC: https://www.intel.com/content/www/us/en/developer/articles/technical/envisi… I think I might steal your IO port API for newer versions of Coyotos, which /is/ impacted by the change. TBF, I think seL4 has a better IRQ handling interface than the one we currently have too. I guess it's only fair it goes both ways! -- William ML Leslie

3 3

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

Reminder seL4 developer hangout
by Birgit Brecknell 15 May '23

15 May '23

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

Reminder seL4 developer hangout
by Birgit Brecknell 01 May '23

01 May '23

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

1 0

One week to go to submit a talk for seL4 summit 2023!
by Birgit Brecknell 17 Apr '23

17 Apr '23

One week to go to submit a talk for seL4 summit 2023 [0]! If you'd like to submit a talk, please upload an abstract of one page or less to the submission portal [1]. The seL4 Summit 2023 will be held 19 - 21 September 2023 at the Elliot Park Hotel, Minneapolis, USA. The summit will be hosted by the Linux Foundation, and will be an in-person event. Registration details to follow soon. We're looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2023/cfp [1] https://sel4.systems/Foundation/Summit/2023/submit --- 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

Reminder seL4 developer hangout
by Birgit Brecknell 17 Apr '23

17 Apr '23

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

Release of the CAmkES to seL4CP Transition Guide
by Jingyao Zhou 14 Apr '23

14 Apr '23

Hi all, The initial version of the CAmkES to seL4CP Transition Guide has been released. The guide aims to provide information and advice for those who are migrating applications built using CAmkES to the seL4 Core Platform. The main focus of this guide is on device driver development and virtual machine (monitor) development. The PDF version of this guide can be found on the Trustworthy Systems web page: https://stage.trustworthy.systems/projects/TS/sel4cp/2304-11-camkes-to-sel4… <https://stage.trustworthy.systems/projects/TS/sel4cp/2304-11-camkes-to-sel4…> The source of this guide can be found in the Trustworthy Systems GitHub repository: https://github.com/au-ts/camkes_to_sel4cp_guide <https://github.com/au-ts/camkes_to_sel4cp_guide> Please don’t hesitate to provide feedback! Regards, Jade.

2 4

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