- Devel - lists.sel4.systems

Ethernet passthrough on x86 (QEMU)
by alberto.lange＠ib.edu.ar 29 Apr '25

29 Apr '25

Hi! I wanted to share another problem with you again, I hope it doesn't bother you. I'm trying to set up a small network between two simulations on QEMU of seL4 running a VM before dealing with hardware. I saw the tutorials related to Ethernet passthrough, but I'm not sure if the same approach applies when using QEMU. These are my configs for the minimal app example: vm0_config.ioports = [ {"start":0xc000, "end":0xc03f, "pci_device":0, "name":"Ethernet5"}, ]; vm0_config.pci_devices = [ { "name":"Ethernet5", "bus":0x0, "dev":0x3, "fun":0, "irq":"Ethernet5", "memory":[ {"paddr":0xfeb80000, "size":0x20000, "page_bits":12}, ], }, ]; vm0_config.irqs = [ {"name":"Ethernet5", "source":11, "level_trig":1, "active_low":1, "dest":10} ]; And checking what QEMU presents to seL4 as hardware: Bus 0, device 3, function 0: Ethernet controller: PCI device 8086:100e PCI subsystem 1af4:1100 IRQ 11, pin A BAR0: 32 bit memory at 0xfeb80000 [0xfeb9ffff]. BAR1: I/O at 0xc000 [0xc03f]. BAR6: 32 bit memory at 0xffffffffffffffff [0x0007fffe]. id "" But when I'm looking for the device on the VM: # lspci 00:00.0 Class 0600: 5e14:0042 I would appreciate any comments on this. Thanks in advance. Alberto Lange

1 0

Custom kernel for x86 VM
by alberto.lange＠ib.edu.ar 29 Apr '25

29 Apr '25

Hi! I'm Alberto, and I'm currently working on my Telecommunications Engineering thesis, which focuses on building a secure system using an seL4 virtual machine. Right now, I'm trying to use the minimal app from the camkes-vm-examples repository with a modified Linux kernel (v6.12.9) built using Buildroot. To do this, I've been replacing the kernel and rootfs files in the vm-linux/images directory with my custom ones. However, this has led to multiple errors during execution. I’d really appreciate some guidance on the correct way to integrate a custom kernel into the CAmkES VM framework. Specifically, should I be using the functions provided in the linux-source-helpers.cmake file to update the kernel and rootfs? Thanks in advance!

2 2

seL4 Summit 2025: extended deadline to submit a talk
by Birgit Brecknell 28 Apr '25

28 Apr '25

The deadline to submit a talk [0] for the seL4 Summit 2025 [1] has been extended until 2 May 2025. If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. **Abstracts are due on 2 May 2025.** Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. The seL4 Summit 2025 will be held 3 - 5 September 2025 at the Grandior Hotel Prague, Prague, Czech Republic. The summit will be an in-person event. Registration and location details are available here [4] [0] https://sel4.systems/Foundation/Summit/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment [4] https://events.linuxfoundation.org/sel4-summit/register/ Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 developer hangout reminder
by Birgit Brecknell 28 Apr '25

28 Apr '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 30 Apr, 8:00am 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

hello_rumprun app not worked
by MOHAMAD REZA SHAFIEI 19 Apr '25

19 Apr '25

hi. i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors: simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x402b7f , . . so i found that this method not implemented yet so i return 0 in this method and resolved. for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method. so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug? thanks for your attention. -- This email was Anti Virus checked by Security Gateway.

5 5

Issue when running rumprun_hello app from the CAmkES manifest
by dinukaamarasinghe817＠gmail.com 19 Apr '25

19 Apr '25

Hello all, mostly Kent, When I run the rumprun_hello app that's included in the CAmkES manifest, I encounter the following runtime errors: [...] Booting all finished, dropped to user space simple_get_extended_bootinfo_length@simple.h:608 simple_get_extended_bootinfo_length not implemented vka_cspace_alloc@vka.h:149 Unimplemented vka_alloc_object_at_maybe_dev@object.h:47 Failed to allocate cslot: error -1 init_rumprun@entry.c:306 [Cond failed: res != 0] Failed to allocate notification object This seems related to the simple->extended_bootinfo_len callback not being implemented, which causes downstream failures in object allocation (e.g. notification object). This issue appears specifically when running Rumprun-based apps. Would appreciate any insights or suggestions on how to resolve or properly set up this functionality. Note that i haven't modified any of the code here. Just tried to run the existing 'rumprun_hello' application.

1 0

Re: Register for the seL4 summit 2025
by Vasily A. Sartakov 16 Apr '25

16 Apr '25

Dear all, > Thanks for the info! A quick question for clarification: What is the difference between the Professional and the Hobbyist registration type? (Sorry if this is obvious to someone, but I'm unable to find an explicit explanation anywhere.) I guess, If you pay out of your own pocket, you are an enthusiast. if it is sponsored by your employer, you are a professional. — Dr.-Eng. V. A. Sartakov

3 2

Register for the seL4 summit 2025
by Birgit Brecknell 14 Apr '25

14 Apr '25

The seL4 summit 2025 [0] will be held in Prague, Czech Republic, 3 - 5 September 2025. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and dinner Register here [1] The early bird cut-off date is 3 August 2025. A number of informal social activities will be organised by the seL4 community for Tuesday 2 Sep 2025. Stay tuned for more info! [0] https://sel4.systems/Foundation/Summit/2025/ [1] https://events.linuxfoundation.org/sel4-summit/register/ Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

2 1

DKernelSkimWindow=off
by Sanyou 14 Apr '25

14 Apr '25

Hi, I am testing sel4 on real Sanyou> x86 board now. I found that if we use parameter DKernelSkimWindow=off, we can see nothing on the uart. Can you give me any advice. Regards, Sanyoo

1 0

seL4 Summit 2025: one week to go to submit a talk
by Birgit Brecknell 14 Apr '25

14 Apr '25

One week to go to submit a talk [0] for the seL4 Summit 2025 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. **Abstracts are due on 21 April 2025.** Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. The seL4 Summit 2025 will be held 3 - 5 September 2025 at the Grandior Hotel Prague, Prague, Czech Republic. 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/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 developer hangout reminder
by Birgit Brecknell 14 Apr '25

14 Apr '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 15 Apr, 10:00pm 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Running seL4 on bare-metal x86_64 PC
by saftab.rashid＠gmail.com 11 Apr '25

11 Apr '25

Hi, I am very new to sel4 and I am trying to run it bare-metal on an Intel Xeon x86_64 machine. I am following the instructions here PC99 | seL4 docs. I can run seL4 using the ./simulate script which runs the kernel under QEMU. However, I would like the run seL4 natively on my machine. After the build, I have the following images in the images/ directory. kernel-x86_64-pc99 sel4test-driver-image-x86_64-pc99 I have created a Grub2 menu entry by copying these images under /boot. However, when I boot using the created menu entry I get a black screen and I also see no output on the serial port. My Grub2 menu entry is as follows menuentry “Load seL4 VM” --class os { load_video insmod gzio insmod part_msdos insmod ext2 set root=‘(hd0,msdos2)’ multiboot /boot/kernel-x86_64-pc99 module /boot/sel4test-driver-image-x86_64-pc99 } I have also tried the multiboot2 protocol as I have an UEFI-supported system but it also doesn’t work. After booting into the seL4 VM I get a black screen and there is no output on the serial port. Any Idea what I am doing wrong?

2 2

Interactions between sDDF and libvmm
by Julia Royer 09 Apr '25

09 Apr '25

Hello, I am currently exploring libvmm and sDDF and I have a question regarding how sDDF is intended to be used in practice. From what I understand, sDDF is often seen in conjunction with libvmm in examples and documentation. My question is: Is sDDF meant to be used exclusively with libvmm, or can it also be used independently? If the latter is possible, is it considered a recommended or meaningful use case, or is the project mainly designed around integration with libvmm? Thank you for your help. Best regards, Julia Royer

2 1

seL4 Summit 2025: two weeks to go to submit a talk
by Birgit Brecknell 07 Apr '25

07 Apr '25

Two weeks to go to submit a talk [0] for the seL4 Summit 2025 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. **Abstracts are due on 21 April 2025.** Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. The seL4 Summit 2025 will be held 3 - 5 September 2025 at the Grandior Hotel Prague, Prague, Czech Republic. 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/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Question about extensibility
by 1plus.yijia＠gmail.com 01 Apr '25

01 Apr '25

One the advantages of microkernel is the extensibility of user space components; however, doesn't the static system design eliminate this advantage? Do I miss something? I wonder if it possible to only recompile a component and replace an older one; if yes, if it possible to replace it in runtime.

2 1

seL4 developer hangout reminder
by Birgit Brecknell 31 Mar '25

31 Mar '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 2 Apr, 7:00am 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

User-level proofs and capability revocation
by Anton Burtsev 28 Mar '25

28 Mar '25

Hi all I have a couple of questions on how user-level proofs are constructed in the seL4 ecosystem. Just to start, can someone point me to an example of a user-level proof, just so I can take a look at how specifications are exported to user processes and how everything is stitched together. But also, I'm a bit confused on what kind of assumptions are needed to build verified user-level code in the face of revocable memory. I.e., it seems that one needs to assume (and trust) that the memory of any verified (or even rather mission critical) process is never revoked. Maybe I'm wrong and missing something and you have a way in mind for how to bypass such trust. Or maybe one can argue that such trust is reasonable, which is probably true for a "flat" system in which the mission critical domain is created right from the trusted boot process or some trusted TCB above it. Yet it seems hard to argue that such trust is reasonable when the recursion is deeper, e.g., the boot process launches Linux, and then Linux tries to start some kind of a mission critical process like a microkernel-protected software TEE or something (out of its memory hence it can later revoke it). And one wants to build a proof about this TCB yet such proof needs to deal with memory that can be revoked at any time or assume that revocation is impossible. Just wandering what is the take on this. I apologize if this all is covered somewhere in seL4 docs and I just didn't dig deep enough. Thank you! Anton

7 14

seL4 libraries compatibility with Microkit
by Julia Royer 22 Mar '25

22 Mar '25

Hi, I understand that Microkit simplifies the seL4 API. However, I would like to know if it is still possible to use seL4 libraries when working with Microkit. If so, is there any benefit to doing so? Thank you in advance for your help. Kind regards, Julia Royer

2 2

seL4 developer hangout reminder
by Birgit Brecknell 17 Mar '25

17 Mar '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 18 Mar, 9:00pm 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Reminder: Call For Presentations for the seL4 Summit 2025
by Birgit Brecknell 14 Mar '25

14 Mar '25

Reminder: Call For Presentations [0] for the seL4 Summit 2025 [1] - Share your seL4 work - Share your seL4 experience - Share your seL4 thoughts Check the full Call For Presentations [0]. To propose a talk, upload an abstract of one page or less by **21 April 2025** to the submission portal [2]. Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. [0] https://sel4.systems/Foundation/Summit/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Libvmm on Rasperry Pi 4B
by Julia Royer 12 Mar '25

12 Mar '25

Hello, I am currently working on a project aimed at exploring the capabilities of the seL4 microkernel and Microkit. For this purpose, I have chosen the Raspberry Pi 4B board. I noticed that libvmm is not yet supported for this platform. Do you have an estimate on when Raspberry Pi 4B might be supported? Thank you for your time and support. Kind regards, Julia Royer

2 5

Release 2.0.0 of Microkit
by Ivan Velickovic 09 Mar '25

09 Mar '25

Hello everyone, There is a new release of Microkit, version 2.0.0. This release contains various bug fixes, quality-of-life changes, features, and new board support. This is a major version bump due to a breaking change. Below the release notes, there is a section on how to upgrade from Microkit 1.4.1. You can download the pre-built SDK from GitHub: https://github.com/seL4/microkit/releases/tag/2.0.0 Ivan

5 11

seL4 for general purpose/desktop operating systems?
by Isaac Beckett 09 Mar '25

09 Mar '25

Hello! I saw Microkit 2.0 has just been released, and it’s prompted a question I’ve been thinking about since before Microkit, when CaMKes was the main thing: Both Microkit and Camkes are designed for embedded and/or static systems, where there is no detection/configuration of hardware at runtime, and in Microkit no swapping of components such as drivers. Is there any work ongoing to use seL4 for a general purpose operating system? Like, a situation where you may have e.g. PC style hardware that can have all sorts of reconfiguration between power-off and next boot, or even while booted and running. Of course this introduces a lot of attack surface, but it makes a lot more sense for a general purpose computer, rather than an embedded one. Is there any recent work/prior art on using seL4 outside of the context of deeply embedded systems? Thanks, Isaac

5 10

Deprecating old boards in the CI system
by Peter Chubb 05 Mar '25

05 Mar '25

Hi folks, There are a number of boards we currently support that we can no longer test, as the boards we had have died. Some of these have been out of production for more than five years. I'm intending to write up deprecation RFCs for any that noone is using -- please reply if you still have software you support on any of the SoCs on these boards: Arndale Exynos 5250 -- Introduced 2012, last available in 2018 Odroid X Exynos 4412 -- introduced 2012, last available 2018 Beagleboard Xm DM3730 -- introduced 2014, still available as new-old-stock, but no longer manufactured. Hikey960 Kirin 620 -- Introduced 2017, last available 2020 Inforce IFC6410 Snapdragon -- Introduced 2013; no userspace support at present -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

seL4 developer hangout reminder
by Birgit Brecknell 03 Mar '25

03 Mar '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 5 Mar, 7:00am 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Call For Presentations for the seL4 Summit 2025
by Birgit Brecknell 17 Feb '25

17 Feb '25

Call For Presentations [0] for the seL4 Summit 2025 [1] - Share your seL4 work - Share your seL4 experience - Share your seL4 thoughts Check the full Call For Presentations [0]. To propose a talk, upload an abstract of one page or less by 21 April 2025 to the submission portal [2]. Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. [0] https://sel4.systems/Foundation/Summit/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 developer hangout reminder
by Birgit Brecknell 17 Feb '25

17 Feb '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 18 Feb, 9:00pm 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 developer hangout reminder
by Birgit Brecknell 03 Feb '25

03 Feb '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 5 Feb, 7:00am 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 test on x86
by Yevgeny Lavrov 30 Jan '25

30 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

seL4 developer hangout reminder
by Birgit Brecknell 20 Jan '25

20 Jan '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 21 Jan, 9:00pm 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

reclaiming root server memory frames
by Yanfeng Liu 18 Jan '25

18 Jan '25

Dear experts, I am wondering how seL4 app can reclaim some root server memory frames at later stage of bootstrapping? Regards, yf

1 1

seL4 developer hangout reminder
by Birgit Brecknell 06 Jan '25

06 Jan '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 8 Jan, 7:00am 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

CDT traveling
by Yanfeng Liu 18 Dec '24

18 Dec '24

Dear experts, I am trying to understand the memory usage of a running seL4 demo with help of GDB. I am wondering how I can travel the Capability derivation tree starting from original untyped objects and see how memory are used. I noticed that `mdb_node_t` has `mdbPrev` and `mdbNext` pointer fields but not sure how can they be used to travel the capability derivation tree? Regards, yf

2 10

On Common IPC Patterns in Microkit
by Wanja.Zaeske＠dlr.de 16 Dec '24

16 Dec '24

Hi together, during the proceedings of the last seL4 summit I participated in a discussion about Microkit usability. In particular we were talking about common patterns for IPC in Microkit, potential pitfalls and how the Microkit Tutorial introduces some of them implicitly (by requiring the user to apply them). At some point Kent suggested to put the topic on the mailing list, so here we go 😊. When initially playing through the Microkit Tutorial, I assumed that the budget/period of a protection domain were providing uninterrupted time-slots. I was thus slightly surprised, when I found out that sending a notification to a higher priority PD would immediately preempt my current PD. Now, this on its own is not problematic, Gernot simply commented my mistake with "Yes, priorities are observed". However: When playing the Microkit tutorial, I understood the way to solve Part 2 (Serial Server to Client Communication) to be as follows: * [serial server] write received char to shared buffer. * [serial server] notify client. * [client] read char from shared buffer. This is also the current approach found in the provided solution [1]. This works in some (most!) cases, but it is not reliable. It could be that chars get lost, due to the serial server overwriting the buffer before it was consumed form the client. The specific details if this works depend upon the combination of: * Data size (not-so-critical with one byte, but more data means more time is required to consume the buffer form the client) * Budget/Period of the client (can the client read all data before it is preempted by exhaustion of its budget in the current period) * Hardware Performance (same as above) * Priorities (if the serial server is higher priority and gets triggered by another hardware event before the client can consume the char, it gets lost again) This is problematic: the details of the scheduling are not very explicit in the manual (roughly one half of a page), but the first example of IPC taught via the tutorial relies on a lot of implicit circumstance on how PDs are scheduled to function correctly. Now I have three suggestions to improve upon this. 1. In the tutorial, explicitly mention the possibility of using the same notification channel in the opposite direction for a read-ACK. If another serial interrupt comes, but no ACK was received, just log an error. The point is not, to introduce ring-buffers and a the machinery for robust communication -- that would like explode the scope for a simple tutorial. Rather, the point is to teach people that this IPC mechanism may silently fail (as in chars get dropped). 2. For certain scheduling + IPC scenarios, examples with a graphical representation would be good. Here are two examples: Sending data to a higher priority PD (via notifications + shared memory) [2] and sending data to a lower priority PD (via notification + shared memory + ACK notification) [3]. Please bear with me, my talent to intuitive graphical representation is of limited nature, this for sure could be made better looking. In the end, I'd like to have an engineer short on time quickly look up the current scenario (sharing data bi-/unidir?, other PD is strictly higher prio/lower prio?, silent loss of data tolerable or not?, ...) from a table, take a look at the timing diagram and pick the correct approach for the task at hand. Microkit does not provide very sophisticated IPC APIs, and that is good! It keeps Microkit small, and the API IMHO provides everything needed, for synchronous and asynchronous communication, for large and small data, ... But composing the IPC correctly is not trivial, so anything we can to take sharp edges of the experience without bloating the API should be considered. 3. I think, there is a finite number of relevant IPC scenarios. Maybe one can build a tool to verify them (something something Promela?) and display them graphically (something something PlantUML Timing Diagrams?). This could either be used to fill a chapter in the Microkit Manual ("Common IPC Patterns, their Behavior and Pitfalls"?), or exposed as small (Web?) GUI Tool. Maybe this could become part of a student thesis even? I hope the above might spark some thought on improving accessibility of Microkit. Kind Regards, Wanja [PlantUML diagram] [PlantUML diagram] [1] https://github.com/au-ts/microkit_tutorial/blob/6733b7864217831e4e77616647e… [2] https://www.plantuml.com/plantuml/uml/VL9DYzim4BthLppIGoxP49kwWHvADlHOIYc5F… [3] https://www.plantuml.com/plantuml/uml/XLDDYzim4BthLpnosKisnA4Ecq9BjlHOIkbbp… —————————————————————————— Deutsches Zentrum für Luft- und Raumfahrt (DLR) Institut für Flugsystemtechnik | Sichere Systeme & Systems Engineering | Lilienthalplatz 7 | 38108 Braunschweig Wanja Zaeske Telefon 0531 295-1114 | Fax 0531 295-2931 | wanja.zaeske(a)dlr.de<mailto:wanja.zaeske@dlr.de> DLR.de<http://www.dlr.de/>

6 7

address of L1 CNode Cap
by Yanfeng Liu 12 Dec '24

12 Dec '24

Dear experts, When reading section 3.3.2 of the latest seL4 manual, it says: > Figure 3.3 depicts an example CSpace. In order to illustrate these ideas, we determine the address of each of the 10 capabilities in this CSpace. I guess the total number of 10 is made of 3 caps for CNode types and 7 for non- CNode ones A~G as shown in diagram. However, in the following graph, the address of the L1 CNode Cap is missed. Thus I am curious what the address for that L1 CNode Cap? Regards, yf

2 2

seL4 developer hangout reminder
by Birgit Brecknell 09 Dec '24

09 Dec '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 11 Dec, 7:00am 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

LionsOS musllibc old version? Vulnerable?
by Hugo V.C. 30 Nov '24

30 Nov '24

Hi, reading the dependencies of LionsOS I realized it is using an old version of muslibc : https://github.com/au-ts/musllibc/blob/81842bc43d0b49bbcca03ff5f506c6df8e2b… if this version has not been patched may be vulnerable to a remotely exploitable buffer overflow in the dns resolution: https://git.musl-libc.org/cgit/musl/commit/?id=45ca5d3fcb6f874bf5ba55d0e965… Can someone confirm or reject? Thanks.

3 3

find all seL4 threads
by Yanfeng 25 Nov '24

25 Nov '24

Dear experts, I am wondering when checking a running seL4 target from GDB, how can we find all threads? It seems that `ksReadyQueues[]` only holds a sub set. Regards, yf

3 3

seL4 developer hangout reminder
by Birgit Brecknell 25 Nov '24

25 Nov '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 26 Nov, 9:00pm 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

iMX8MM seL4 12.1.0 running a VM
by Zippy Manaic 22 Nov '24

22 Nov '24

Hi, I have encountered a problem where the device tree is not correctly being parsed resulting in interrupts not being routed to the VM. A node which exhibits this issue is (there are several more in the iMX8MM device tree that also trigger the problem) ``` snvs@30370000 { compatible = "fsl,sec-v4.0-mon\0syscon\0simple-mfd"; reg = <0x30370000 0x10000>; phandle = <0x1b>; snvs-rtc-lp { compatible = "fsl,sec-v4.0-mon-rtc-lp"; regmap = <0x1b>; offset = <0x34>; interrupts = <0x00 0x13 0x04 0x00 0x14 0x04>; clocks = <0x02 0xe4>; clock-names = "snvs-rtc"; }; }; ``` Interrupts 0x13 and 0x14 should be included in the camkes_dtb_irqs[] variable but they are not. Looking at the node as it is parsed in macros.py via the function parse_dtb_node_interrupts {'compatible': ['fsl,sec-v4.0-mon', 'syscon', 'simple-mfd'], 'reg': [808910848, 65536], 'phandle': [27], 'snvs_rtc_lp': [<pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c28f10>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c28f70>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c28fd0>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f070>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f0d0>, <pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f130>], 'snvs_rtc_lp_compatible': ['fsl,sec-v4.0-mon-rtc-lp'], 'snvs_rtc_lp_regmap': [27], 'snvs_rtc_lp_offset': [52], 'snvs_rtc_lp_interrupts': [0, 19, 4, 0, 20, 4], 'snvs_rtc_lp_clocks': [2, 228], 'snvs_rtc_lp_clock_names': ['snvs-rtc'], 'snvs_powerkey': [<pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f1f0>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f250>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f2b0>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f310>, <pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f370>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f3d0>, <pyfdt.pyfdt.FdtProperty object at 0x7483b4c2f430>, <pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f490>], 'snvs_powerkey_compatible': ['fsl,sec-v4.0-pwrkey'], 'snvs_powerkey_regmap': [27], 'snvs_powerkey_interrupts': [0, 4, 4], 'snvs_powerkey_clocks': [2, 228], 'snvs_powerkey_clock_names': ['snvs-pwrkey'], 'snvs_powerkey_linux_keycode': [116], 'snvs_powerkey_wakeup_source': [], 'snvs_powerkey_status': ['okay'], 'this_address_cells': [1], 'this_size_cells': [1], 'this_node_path': '/soc@0/bus@30000000/snvs@30370000'} The function is looking for 'interrupts' but the interrupt declaration in the child node has been renamed to 'snvs_rtc_lp_interrupts'. This explains why the interrupts are omitted from the template generated code. A hacky fix, that does appear to work, is to paste the interrupt declarations into the parent node. I'm sure there's a more elegant way to resolve this but my detailed knowledge in this area is lacking. I am going to have a look at seL4 13.0.0 to see if this has already been fixed with a view to a potential backport but thought I'd check here before starting to dig a new hole to fall into. Many thanks, Zippy

2 3

seL4 summit 2025: survey about location
by Birgit Brecknell 20 Nov '24

20 Nov '24

With the great success of the seL4 summit 2024 [0] behind us, we are now looking at the seL4 summit 2025! This should happen around Sep/Oct 2025, and will be held in Europe. We have started investigating options for the location, and would like your feedback. We would greatly appreciate it if you could fill in this very short survey to tell us your opinions: https://form.jotform.com/243076885259874 *Please do so by 29 Nov 2024.* Feel free to forward to anyone you believe may want to attend the summit next year. [0] https://sel4.systems/Foundation/Summit/2024/ Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Re: Modifying the root user thread's CSpace
by Indan Zupancic 16 Nov '24

16 Nov '24

Hi Ben, (Please don't drop CC.) Glad I could help. Don't be too hard on yourself, hindsight is easy. For defensive programming reasons (which also makes attacks harder), it's good to have a non-zero guard for your caps which doesn't overlap with your virtual address space, at least for the first level. For the last level it depends on how you want overflows to behave: If you want to seamlessly continue into the next CNode, have a zero guard size (good for e.g. dynamic CNode allocation). If you want to detect overflow errors on sets of caps, make sure you have a guard size of at least 1 bit. Having a non-zero guard value has less advantage for later CNode levels. Greetings, Indan On 2024-11-15 16:25, Ben McCart wrote: > Indan, > > Thank you so much! seL4_CNode_Mint instead of seL4_CNode_Copy solved > my problem. The piece I was missing was that I needed to change the > guard on the original seL4_CapInitThreadCNode when copying it into the > first CSlot of the new root CNode. (Doh!) I should have caught that > as you said explicitly in you prior response that each CNode capability > can have different guard bits set. (I just didn't think carefully > enough about that.) > > On 11/15/2024 4:55 AM, Indan Zupancic wrote: >> >> seL4_CNode_Copy can't change the guard, you have to use >> seL4_CNode_Mint() if you need to change it: >> >> assert(bi->initThreadCNodeSizeBits <= 16); >> seL4_CNode_Mint( >> cspace_cap, >> 0, // Destination index in the >> new Cap table. >> 16, // Number of bits for the new >> Cap table. >> seL4_CapInitThreadCNode, >> seL4_CapInitThreadCNode, >> seL4_WordBits, >> seL4_AllRights, >> 16 - bi->initThreadCNodeSizeBits); // Zero pad guard to reach 16 >> bits. >> <SNIP> >> Indan > > -Ben

1 0

Modifying the root user thread's CSpace
by Ben McCart 16 Nov '24

16 Nov '24

Hello, I read the manual for v12.0 chapters 1-3, and 10. I have been attempting to experiment with CSpaces for the user space root thread. I am trying to modify the CSpace to support multiple CNode levels by changing the guard from all zero bits above the radix (16 bits of radix on PC99 x64), to support multiple CNode levels. I have been using seL4_TCB_SetSpace to modify the CSpace for seL4_CapInitThreadTCB. The result is seL4_NoError and once I make this call the previously working capabilities tutorial quits working as expected. (Calls taking the original seL4_CapInitThreadTCB value are now returning seL4_InvalidCapability). I have studied chapter three of the manual and I think I understand how the CSpace addressing works in depth. What I can't seem to figure out is how to construct a cspace_root_data argument for the call to seL4_TCB_SetSpace for the number of guard bits and the guard values I want to use. For example, if I wanted two levels each with a 4 bit guard and a 16 bit radix how would I construct cspace_root_data argument for a gaurd value of 0x0? And for a gaurd value of 0xF? (I intend to keep the original seL4_CapInitThreadTCB CNode as my level-1 CNode for this experimentation.) Thank you in advance if you can point me to some reference documentation that may cover how to construct the cspace_root_data argument, guidance, or direction you may be able to give. Sincerely, Ben McCart

3 6

Potential vulnerabilities
by Hugo V.C. 15 Nov '24

15 Nov '24

I'm forwarding this question here (tried on Mattermost Trustworthy Systems group first) hoping someone can put some light on this? --- Hi, I'm having a look to the vulns (in areas of the kernel that have not been formally verified) patched in seL4 13.0.0. We have: 1) "NULL pointer dereference when injecting an IRQ for a non-associated VCPU on SMP configurations." 2) "On AArch64, when seL4 runs in EL1 the kernel would fault with a data abort in seL4_ARM_Page_Invalidate_Data and seL4_ARM_VSpace_Invalidate_Data when the user requested a dc ivac cache maintenance operation on a page that is not mapped writeable." Extremely simple question: running version < 13.0.0 on top of Qemu (in example like https://docs.sel4.systems/projects/sel4webserver/) would it be vulnerable to any of those? --- Best,

4 13

seL4 developer hangout reminder
by Birgit Brecknell 11 Nov '24

11 Nov '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 13 Nov, 7:00am 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

ci-actions/preprocess
by Yanfeng 07 Nov '24

07 Nov '24

Dear experts, I am seL4 newbie. When I changed compile options in seL4/CMakeLists.txt, I got check errors from "ci-actions/preprocess" check like this one: https://github.com/seL4/seL4/actions/runs/11682457028/job/32529623251 Can someone teach where I can see details of "ci-actions/preprocess" check? Regards, yf

2 2

Introduction to seL4's Architecture & Concepts
by tunacici7＠gmail.com 03 Nov '24

03 Nov '24

Hey everyone. I've created an introductory documentation to seL4’s architecture & concepts. I thought it would be helpful for anyone interested in seL4 and wanted to share. The documentation includes many hand-written visualizations to make seL4 (and its abstractions) more accessible to people. You can access it on GitHub: https://github.com/TunaCici/seL4_Architecture Hope you enjoy it! NOTE: I’m sorry if this isn’t the best place to share this. I don’t know of any other active seL4 communities besides the mailing list.

6 6

AMD64 - how much virtual address space does the kernel map?
by Ben McCart 31 Oct '24

31 Oct '24

Hellow all, I have been working through the tutorials and doing some experimenting and ran into behavior that very much surprised me. I can seL4_X86_PageTable_Map & seL4_X86_Page_Map to virtual addresses starting at the 96 MB address (0x06000000) with no errors. However, as soon as I try to seL4_X86_PageDirectory_Map that same virtual address I get the error seL4_DeleteFirst. I didn't think the kernel mapped anything for the root address above 64 MB virtual address range for the root address in these tutorials. If it did I would have expected an error for seL4_X86_PageTable_Map & seL4_X86_Page_Map. What is going on? What am I missing? How can I avoid expecting to map a virtual address in a range already mapped by the kernel for the root process on a given architecture? - Ben McCart

2 1

seL4 fails to boot multiple core at CPU 0x1.
by Vishal Gupta 31 Oct '24

31 Oct '24

Dear All, I am a seL4 enthusiast , I am trying to port , build and test seL4 for ARM64 Cortex A53 based hardware. For Single core , I am able to boot via elf-loader then jump to kernel and successfully run Hello World program without any issues. But when I am trying to change it to multiple core SMP enabled on my hardware or even in ARM Qemu setup it is failing to boot. Can anyone please guide me , if seL4 supports multicore than for which version of ARM / board it currently supports , as I could see support for only Sabre-Arm32, which is ARMv7A. Boot log attach for reference. ———————————————————————— ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[40a4c000…40f57137] No DTB passed in from boot loader. Looking for DTB in CPIO archive…found at 40bacbe8. Loaded DTB from 40bacbe8. paddr=[4024c000…4024dfff] ELF-loading image ‘kernel’ to 40000000 paddr=[40000000…4024bfff] vaddr=[ffffff8040000000…ffffff804024bfff] virt_entry=ffffff8040000000 ELF-loading image ‘sel4test-driver’ to 4024e000 paddr=[4024e000…40654fff] vaddr=[400000…806fff] virt_entry=40e700 Boot cpu id = 0x0, index=0 HVC is not supported for PSCI! Failed to boot cpu 0x1: 18446744073709551615 abort() called. ——————————————————————————— Looking for any guidance, as it will be helpful for me to move forward . Regards, Vishal

2 1

seL4 developer hangout reminder
by Birgit Brecknell 28 Oct '24

28 Oct '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 29 Oct, 9:00pm 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Device memory access issue on sel4 user driver
by misbah khan 25 Oct '24

25 Oct '24

Hello sel4 developers, I am using seL4 for in our arm64 based hardware platform. I need to write a simple driver where i need to read/write some memory mapped registers The device physical address is "0x40520000" When i print the bootinfo using the below code: /*-- filter TaskContent("untyped-start", TaskContentType.ALL, subtask='init') -*/ printf(" CSlot \tPaddr \tSize\tType\n"); for (seL4_CPtr slot = info->untyped.start; slot != info->untyped.end; slot++) { seL4_UntypedDesc *desc = &info->untypedList[slot - info->untyped.start]; printf("%8p\t%16p\t2^%d\t%s\n", (void *) slot, (void *) desc->paddr, desc->sizeBits, desc->isDevice ? "device untyped" : "untyped"); I get the following output: CSlot Paddr Size Type 0x1ac 0 2^30 device untyped 0x1ad 0x40000000 2^28 device untyped 0x1ae 0x50000000 2^23 device untyped 0x1af 0x50810000 2^16 device untyped 0x1b0 0x50820000 2^17 device untyped I am mappint the physical address to virtual and trying to access it as: va = ps_io_map(&ops.io_mapper, (uintptr_t) 0x40520000,0x3000, PS_MEM_NORMAL); ZF_LOGE("Physical address 0x%x mapped to virtual address %p \n",DEV_REG_PADDR,va); for(int j=0;j<DEV_REG_SIZE;j+=sizeof(unsigned int)) { ZF_LOGE("Loc %d --> 0x%x ",j,*(unsigned int*)(va+j)); } I am able to access some registers, but then it gives a fault (after printing 5-6 register values) Similar is the behaviour with any reg between the range 0x40000000 - 0x50000000 Attaching the sample code and output: I am able to access first two address location, after that it gives halt. Regards, Misbah

2 2

sel4 for Imx8Plus
by janarthanan.b＠teclever.com 23 Oct '24

23 Oct '24

Hi sel4 dev team, I'm working on imx8 Plus board for that Building seL4test is done and generated the binary image file of "sel4test-driver-image-arm-imx8mp-evk" with the size of 5mb as per the procedure on sel4 websites. I moved this into sd card and trying to boot into board.but i cant able to boot it. What is the issue on this and how to solve it? if we need to do uboot what's the procedure for that?

3 4

seL4 hangs during invalidate local TLB
by Vishal Gupta 16 Oct '24

16 Oct '24

Dear seL4 developers, I am a seL4 enthusiast. I am trying to port seL4 on arm64 cortex a53. I am able to port elf-loader successfully and move to the kernel initialisation which reaches till “try_init_kernel->init_cpu->activate_global_pd->invalidateLocalTLB->asm volatile()”. Under InvalidatelocalTLB with asm volatile(“tlbi vmalle1”); in this , the system gets hanged and the asm function does not move forward. Any input or guidance would be really appreciated. Thank you . Regards, Vishal

1 0

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 16 Oct '24

16 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

seL4 developer hangout reminder
by Birgit Brecknell 30 Sep '24

30 Sep '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 1 Oct, 10:00pm 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

General Question On Object Methods
by tunacici7＠gmail.com 25 Sep '24

25 Sep '24

I've recently started to learn seL4 by following the Tutorials, which have been great so far. I've been also reading the Manual & API reference to understand and gain insight into different mechanisms. However, I have one fundamental question: Are the object methods system calls? It is said that seL4 only has 3 logical system calls: Send, Recv and Yield. (In all the slides, videos and other documents I have seen) And the rest is just variations of those ones. But what about object methods? Are they system calls? Are they executed in kernel space? If they are system calls, then wouldn't all the resources out there be misleading? Since there are way more than just Send, Recv and Yield. If they are not, then how are they handled? Does 'libsel4' have anything to do with it? I can't imagine 'seL4_Untype_Retype' executing in user space. Unfortunately, I couldn't find any answers to this question online. So that's why I'm asking it here. Maybe there are others who wonders the same thing. NOTE The API Reference page confuses me even more. It lists Object Methods in its own category (instead of being under System Calls). Does this means Object Methods are NOT system calls? Or the term System Call is just not what I think it is(basically an endpoint to kernel)?. END NOTE Thanks for the answers in advance. -T

8 21

seL4 developer hangout reminder
by Birgit Brecknell 16 Sep '24

16 Sep '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 18 Sep, 8:00am 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Less than 1 week left to get the early-bird registration for the seL4 summit
by Birgit Brecknell 09 Sep '24

09 Sep '24

Less than 1 week left to get the early-bird registration for the seL4 summit The early bird cut-off date for the seL4 summit 2024 [0] is 15 September 2024. The summit will be held in Sydney, Australia, 15-17 October 2024. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and dinner Register here [1] A number of informal social activities [2] are being organised by local Sydney-siders. Check out the list [2] and contact the organiser to register your interest. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://events.linuxfoundation.org/sel4-summit/register/ [2] https://sel4.systems/Foundation/Summit/2024/social-activities Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Virtual address ranges used in seL4 initial thread after boot?
by Ben McCart 06 Sep '24

06 Sep '24

I have read the manual in section 9.2 about userImageFrames and how to infer the virtual address range for the pages being used for the userland image, which I frankly do not concretely understand. For example, I can take the address of main() and that leads me to believe my first user image frame (page frame actually I suspect) is probably at 0x40000, but it feels like guessing. (Not good!) In addition, I like to know the address range used for the stack of the initial thread, as well as any other reserved regions (I read somewhere in the manual about reserved virtual address space for the kernel, but I can't remember where I read that and now I can't find it.) Are there any macros included in public header files that I can use in my project to get the starting addresses for any of these regions? Barring that, is there any straight-forward reliable way to find the starting address for these regions (or in the case of kernel reserved virtual address range is it documented anywhere?) I am on version 12.0 of seL4 for my project. Thank you! -Ben

2 2

Less than 2 weeks left to get the early-bird registration for the seL4 summit
by Birgit Brecknell 02 Sep '24

02 Sep '24

Less than 2 weeks left to get the early-bird registration for the seL4 summit The early bird cut-off date for the seL4 summit 2024 [0] is 15 September 2024. The summit will be held in Sydney, Australia, 15-17 October 2024. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and dinner Register here [1] A number of informal social activities [2] are being organised by local Sydney-siders. Check out the list [2] and contact the organiser to register your interest. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://events.linuxfoundation.org/sel4-summit/register/ [2] https://sel4.systems/Foundation/Summit/2024/social-activities Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 developer hangout reminder
by Birgit Brecknell 02 Sep '24

02 Sep '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 3 Sep, 10:00pm 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 developer hangout reminder
by Birgit Brecknell 19 Aug '24

19 Aug '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 21 Aug, 8:00am 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Gpu passthrough
by Hugo V.C. 15 Aug '24

15 Aug '24

Hi all, here a simple question: is there any example/tutorial off gpu passthrough to a Linux guest? Best,

4 6

Build failure for sel4 on raspberry pi 5
by l4＠photiczone.com 14 Aug '24

14 Aug '24

Hi everyone, I am getting a link failure during the build of sel4test-tests: /usr/bin/ld: apps/sel4test-driver/musllibc/build-temp/stage/lib/libc.a(__stdio_exit.o): copy relocation against non-copyable protected symbol `__stdin_used' collect2: error: ld returned 1 exit status Searching t'interwebs seems to imply this is a gnarly problem caused by the nuances of various build tools - but one that should not apply to Arm. You can summarise everything I did before the build like this: sudo apt install ninja-build libxml2-utils repo pip3 install pyyaml typing hardware pyfdt jinja2 jsonschema six future ply python3-protobuf grpcio-tools cd && mkdir xxx && cd xxx Then to follow your build repo init -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir build && cd build ../init-build.sh -DPLATFORM=bcm2711 ninja And yes I know it is not supported and the BCM2711 is for the Pi 4. I am evaluating ;) Any help greatly appreciated. Thanks, Smiley

3 4

I am interested in porting LionOS to X64 architecture
by Peter Relich 14 Aug '24

14 Aug '24

Hello, I am a researcher at Intellisense Systems, Inc. We are a small business that performs R&D for the U.S. Military. We have an active contractor to build a hypervisor for a microkernel. We recently selected Sel4 as the microkernel and I learned that the Army (our customer) used a camKes implementation of a VMM to host a fork of Ubuntu, but the limitations prompted them to try another approach. I think since that time, microkit has developed quite a bit and I saw the trustworthy systems has even been developing an operating system on the Sel4 microkernel. However, LionOS appears to be developed for ARM systems as the use case. For the Army use, we are using a Nuvo7000LP: https://www.neousys-tech.com/Resource/Product_Document/Nuvo-7000LP/Nuvo-700… Which is an X64 architecture. I just started learning microkit through your available tutorials and I am aware that building a comprehensive VMM is no easy task. However, I was wondering if you had some intuition or if you could provide me an estimate of the libraries in the LionOS that I would need to adjust/redesign to make an X64 architecture fork? Is this even a feasible approach? It looks like I just need to swap out the aarch64 libraries with compatible x64 libraries and do some testing. Before I commit, I just wanted to get some advice on the endeavor. Is forking LionOS to an X64 architecture feasible, or should I start at a lower level (i.e., redesigning the vmm?) Thanks so much for your time. Respectfully, Peter Relich Research Scientist Intellisense Systems, Inc. ________________________________ The information contained in this e-mail and any attachments from Intellisense Systems may contain confidential and/or proprietary information, and is intended only for the named recipient to whom it was originally addressed. If you are not the intended recipient, any disclosure, distribution, or copying of this e-mail or its attachments is strictly prohibited. If you have received this e-mail in error, please notify the sender immediately by return e-mail and permanently delete the e-mail and any attachments.

5 5

MCS round-robin scheduling not behaving as expected
by liam.vervecken＠gmail.com 12 Aug '24

12 Aug '24

Hello, I'm trying to understand MCS and how the scheduling works but I'm running into some issues. My setup: RISCV on BeagleVFire in sel4test I have configured 2 threads: seL4_SchedControl_ConfigureFlags(info->schedcontrol.start, sched_context_thread2, 1000000, 1000000, 0, 0, 0); seL4_SchedContext_Bind(sched_context_thread2, thread2_TCB); seL4_SchedControl_ConfigureFlags(info->schedcontrol.start, sched_context_thread3, 1000000, 1000000, 0, 0, 0); seL4_SchedContext_Bind(sched_context_thread3, thread3_TCB); The threads have the same priority. From the documentation I was expecting them to behave like this: - Thread1 does something - Thread2 does something - Thread1 does something - ... But it seems instead only the first thread gets scheduled, and it never allows the second thread to get any CPU time. Am I correct in assuming that 2 threads with period=budget and equal priority should be scheduled round-robin? I found that if I call seL4_SchedContext_Consumed(sched_context_thread) periodically in the threads they will switch if the budget has expired. It doesn't make much sense to me why this is the case, I thought they would switch automatically once their budget is expired and that seL4_SchedContext_Consumed() was simply used to keep track of this. I'm hoping it can offer some clue as to what I'm doing wrong. Any help or guidance would be greatly appreciated. Kind Regards, Liam

6 6

LionsOS as basis for mobile/handheld OS
by Isaac Beckett 10 Aug '24

10 Aug '24

I was looking at LionsOS docs recently, and noted it is meant for static systems with no support for changing hardware at runtime. This is less of a problem for phones and other handhelds given they generally keep the same hardware throughout their service life, but I was concerned about peripheral support. What if I want to be able to connect an external display to a phone or tablet running a LionsOS based userspace? Or I have privacy switches on the device that physically disconnect components such as the modem or camera assembly? Most of the system would be static, and only really changing for things such as loading isolated, untrusted application code (such as a Linux kernel, or something pretending to be a Linux kernel), but it would still have some hardware components that can be disconnected. Though at least in the case of privacy switches they would be the same components every time. What do y’all think? Does this idea of building a mobile phone OS on LionsOS have merit or would it make more sense to use a different framework or build something on seL4 directly?

3 3

LionOS Docs
by Hugo V.C. 09 Aug '24

09 Aug '24

Hi! I'm planning to switch from CAmkES to LionOS but I got a 404 on this link: https://github.com/au-ts/lionsos-docs that is on this URL: https://www.lionsos.org/docs/tutorials/ Best,

2 1

Release 0.2.0 of LionsOS
by Ivan Velickovic 06 Aug '24

06 Aug '24

Hello everyone, There has been a new release of LionsOS, 0.2.0. This release is primarily focused on maturing the existing OS services and making it easier to build LionsOS-based systems. You can find detailed release notes here: https://github.com/au-ts/lionsos/releases/tag/0.2.0 Thanks, Ivan

1 0

Release 0.5.0 of the seL4 Device Driver Framework
by Ivan Velickovic 06 Aug '24

06 Aug '24

Hello everyone, There has been a new release of the seL4 Device Driver Framework, 0.5.0. This release is primarily focused on making the various device classes we support more mature. You can find detailed release notes here: https://github.com/au-ts/sddf/releases/tag/0.5.0 You can find the latest design documentation attached to the release artefacts. Thanks, Ivan

1 0

Release 1.4.0 of Microkit
by Ivan Velickovic 05 Aug '24

05 Aug '24

Hello everyone, We have made a new release of the seL4 Microkit, version 1.4.0. This release contains a number of features requested by the community. You can find the release notes here: https://docs.sel4.systems/releases/microkit/1.4.0 You can find the SDK downloads here: https://github.com/seL4/microkit/releases/tag/1.4.0 Thanks, Ivan

1 0

seL4 developer hangout reminder
by Birgit Brecknell 05 Aug '24

05 Aug '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 6 Aug, 10:00pm 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

How do I reduce the size of the seL4 executable?
by liam.vervecken＠gmail.com 26 Jul '24

26 Jul '24

Hello, I'm trying to compile a simple 'hello world' sel4 program for the polarfire (riscv) and I want the executable to be as small as possible. According to the FAQ (https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html) the single core kernel can compile to a <200kb executable but in my testing, I always end up with an image of approx 2MB. I worked with this (https://github.com/mskordal/SeL4-hello-world) example project and changed main.c to work with seL4_DebugPutChar instead of printf. Besides that, I added opensbi to the tools folder and slightly modified line 32 of projects/hello/CMakeList.txt to target_link_libraries(hello sel4 sel4_autoconf sel4runtime sel4platsupport). After running ../init-build.sh -DPLATFORM=polarfire and ninja, I end up with an executable of about 2MB. I'm guessing musllibc, util_libs and sel4_libs contribute to the size, but if I change my cmakelist file to try to get rid of them the build will fail. I was hoping since my hello world only uses sel4 APIs I could compile it without musllibc, util_libs and sel4_libs but I haven't been able to figure out how. Any help or tips would be greatly appreciated. Kind Regards, Liam

1 0

next seL4 TSC meeting on Thu 25 Jul
by Gerwin Klein 24 Jul '24

24 Jul '24

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Thu, 25 Jul, 4pm - Central Europe: Thu, 25 Jul, 8am - US West Coast (LA/SF): Thu, 25 Jul, 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/89949317341?pwd=JSC976ciVYmbDJByjSFH0chh78sCsg.1 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 - discuss new FPU RFC: https://github.com/seL4/rfcs/pull/26 - hear about progress on PMU, budget limit, device driver framework - make decision on old RFC-4: https://github.com/seL4/rfcs/pull/12 - any feedback on GitHub RFC implementation - bump version of cmake-format (will break current formatting) to reduce python dependency hell 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

3 6

seL4 developer hangout reminder
by Birgit Brecknell 22 Jul '24

22 Jul '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 24 Jul, 8:00am 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Announcing beta.sel4.systems running on LionsOS
by James Archer 11 Jul '24

11 Jul '24

Trustworthy Systems is now serving a copy of the seL4.systems website from a beta LionsOS-based[1] webserver. It can be accessed at https://beta.sel4.systems/. The source code can be found in the LionsOS repository[2]. More information about the implementation can be found at https://beta.sel4.systems/Info/Website/. Any feedback or attempts to break it are welcome. [1] https://lionsos.org/ [2] https://github.com/au-ts/lionsos James

3 3

seL4_X86_Page_Map on seL4_X86_LargePageObject != 2MiB
by Ben McCart 10 Jul '24

10 Jul '24

I have created my own project on the PC99 architecture (x64) and have been working through the tutorial source (copy & pasted into my project) to learn and then prototype with seL4. I have done the mapping tutorial (pc99) and utilized that code within my project and everything seems to work just fine, but if I change out the seL4_X86_4K to seL4_X86_LargePageObject I don't end up with 2MiB of mappable virtual space. All the seL4 system calls through the client API return seL4_NoError. The seL4_LargePageBits value is 21 (2^21 == 2MB, and intel documentation for IA-32e shows that 2 MiB should be the large page size. However, if I address memory outside of the first 256 KiB it halts. The following works: seL4_Word *x = (seL4_Word *) TEST_VADDR; printf("Read x: %lu\n", *x); And this works: seL4_Word *x = (seL4_Word *) TEST_VADDR + 0x0003FFF0; printf("Read x: %lu\n", *x); But this halts when trying to dereference x to print it: seL4_Word *x = (seL4_Word *) TEST_VADDR + 0x00040000; printf("Read x: %lu\n", *x); I am running seL4 12.1 using QEMU with the following command line: qemu-system-x86_64 -cpu Nehalem,-vme,+pdpe1gb,-fsgsbase,-invpcid,+syscall,+lm,enforce -nographic -serial mon:stdio -m size=512M -s -S -kernel ../sel4-project/build/images/kernel-x86_64-pc99 -initrd build/cxxkit Does anybody have any idea why I might be having this issue and what I may do about it? -Ben McCart

2 2

seL4 developer hangout reminder
by Birgit Brecknell 08 Jul '24

08 Jul '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 9 Jul, 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

New release of seL4, Microkit, CAmkES, capDL and Rust support
by Gerwin Klein 02 Jul '24

02 Jul '24

We’re pleased to announce the release of - seL4 13.0.0: The seL4 microkernel https://docs.sel4.systems/releases/sel4/13.0.0 - Microkit 1.3.0: The seL4 Microkit for building static-architecture systems https://docs.sel4.systems/releases/microkit/1.3.0 - CAmkES 3.11.0: Component Architecture for microkernel-based Embedded Systems https://docs.sel4.systems/releases/camkes/camkes-3.11.0 - capDL 0.3.0: Tools for generating, parsing and loading capability distribution specifications https://docs.sel4.systems/releases/capdl/0.3.0 - rust-sel4 1.0.0: Rust support for seL4 userspace https://github.com/seL4/rust-sel4/releases/tag/v1.0.0 See https://github.com/seL4/rust-sel4/ for more information. Microkit 1.3.0 and rust-sel4-1.0.0 are the first official releases under the seL4 foundation. Cheers, Gerwin

1 0

New release of seL4, Microkit, CAmkES, capDL and Rust support
by Gerwin Klein 02 Jul '24

02 Jul '24

We’re pleased to announce the release of - seL4 13.0.0: The seL4 microkernel https://docs.sel4.systems/releases/sel4/13.0.0 - Microkit 1.3.0: The seL4 Microkit for building static-architecture systems https://docs.sel4.systems/releases/microkit/1.3.0 - CAmkES 3.11.0: Component Architecture for microkernel-based Embedded Systems https://docs.sel4.systems/releases/camkes/camkes-3.11.0 - capDL 0.3.0: Tools for generating, parsing and loading capability distribution specifications https://docs.sel4.systems/releases/capdl/0.3.0 - rust-sel4 1.0.0: Rust support for seL4 userspace https://github.com/seL4/rust-sel4/releases/tag/v1.0.0 See https://github.com/seL4/rust-sel4/ for more information. Microkit 1.3.0 and rust-sel4-1.0.0 are the first official releases under the seL4 foundation. Cheers, Gerwin

1 0

seL4 MCS flavour with RISCV
by David Martin 01 Jul '24

01 Jul '24

Hello, I'm trying to understand the current situation of the MCS branch. Our setup: - Microchip Polarfire SoC (1xE51 RV64IMAC + 4xU54 RV64IMAFD) We are starting to "play" with threads but when coming to the scheduling of them, I'm a bit lost. If I understand correctly, the latest version of seL4 (12.1.0) if compatible with RV64IMAFD, so floating point operations included. The latest MCS version (10.1.1-mcs) on the contrary is only RV64IMAC so no FPU support. I haven't seen any MR nor discussion about including that FPU support when using RISCV processors... Am I correct in here? or I am missing something? (It's not really clear to me when I read the docs to be honest) Thanks for your support. - David.

1 0

CPU/ISA tuned specifically for seL4?
by Isaac Beckett 26 Jun '24

26 Jun '24

Hello! I recall reading about old CPUs/ISAs made for Lisp machines, with features and optimized for specifically running Lisp. And I’ve heard people discuss how current CPUs are optimized for C code and similar programming paradigms, and vice versa: C and others are optimized for those CPUs. This got me wondering, what might a CPU or instruction set designed more specifically to run seL4 look like? I’m guessing it might involve capability hardware like CHERI to accelerate seL4’s software implementation of capabilities, but what else might be relevant? Thanks, Isaac Beckett

3 2

seL4 developer hangout reminder
by Gerwin Klein 23 Jun '24

23 Jun '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 26 Jun, 08:00 UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

Success and Effort in seL4 x86_64 Virtualbox
by thomas.j.hampton＠gmail.com 21 Jun '24

21 Jun '24

Hey; configuration is a pretty big space and I didn't see anything specific, and may have bumped into a bug along the way. Here's some details about getting seL4test working, and using the EGA driver on this platform. Here's the commits I'm on: - sel4test 95522e9 - seL4 ddeb18a01 I managed to get seL4test running in VirtualBox on a Tiger Lake chip some weeks ago, not terribly impressive, things worked pretty well, generally. - I discovered that on the platform I needed to manually set all the '*HAVE_TIMER*' flags in the code to 0 - to get the tests to succeed on VirtualBox; CMake doesn't appear to support this transformation. - a major stumbling block was that these changes were being reverted each time I re-ran CMake, under my feet. So that's pretty cool... Some further exploration I discovered that there's the pc99/ega (ega.c) driver, since I'm curious about the requirements for starting to build a custom OS on top of seL4 for this platform, and seeing it run on the hardware in front of me (again, a Tiger Lake laptop). I spent many weeks trying to massage things into place. Reading and learning along side the bootstrap pathway; multiboot.S -> head.S -> boot_sys -> common -> char_dev ... to no avail. However I came into some time and decided to revisit the problem. - #define MULTIBOOT_GRAPHICS_TEXT 2 is an error; Multiboot1 spec has that this should be 1, instead - When I was trying to boot UEFI, this would manifest as a Protection Fault - Fixing this left the system booting, utilizing high amount of CPU, and then going quiet. - UEFI on this platform has unclear / additional requirements / doesn't actually support EGA/VGA text mode - https://www.reddit.com/r/osdev/comments/st0psl/framebuffer_output_for_multi…

2 1

Assertion failure when booting seL4 image on x86 UEFI via Grub
by fennelfoxxo＠gmail.com 16 Jun '24

16 Jun '24

Hello all! This is my first time posting here, but I'll try to provide all the detail I can, and I'm grateful for any advice others have to fix this issue. I've been trying to boot the seL4 Hello World tutorial in QEMU with UEFI support on the x86 platform, with the help of the Grub bootloader. It seems I can load the kernel okay, but an error occurs when the kernel tries to load the rootserver: > seL4 failed assertion 'mods_end_paddr > boot_state.ki_p_reg.end' at /home/fennel/grubbuild/stacktest/sel4-tutorials/kernel/src/arch/x86/kernel/boot_sys.c:452 in function try_boot_sys From my research, it seems to be happening because grub is loading the rootserver module at a lower address than expected. These two lines from serial output during boot indeed show that the module end address is lower than the kernel end address: > module #0: start=0x751000 end=0x7954c8 size=0x444c8 name='' > Kernel loaded to: start=0x100000 end=0xc12000 size=0xb12000 entry=0x100298 When running the same hello world project using ./simulate in the build directory, the rootserver module is placed at a higher address and boots ok: > module #0: start=0xc13000 end=0xc574c8 size=0x444c8 name='images/hello-world-image-x86_64-pc99' > Kernel loaded to: start=0x100000 end=0xc12000 size=0xb12000 entry=0x100298 Does anyone know if this is a mistake in how I am compiling and building the project, my QEMU settings, or perhaps an issue with how Grub is handling loading the module? Booting from Grub should be possible in theory (https://docs.sel4.systems/Hardware/IA32.html) so any guidance is appreciated. Thank you! - Fennel STEPS TO REPRODUCE: # Contents of grub.cfg - place in current directory menuentry "Load seL4" --class os { insmod efi_gop insmod efi_uga insmod all_video set root='(hd0,gpt1)' multiboot2 /EFI/BOOT/sel4kernel module2 /EFI/BOOT/sel4rootserver } # End of grub.cfg # Compile Grub 2.06 from source to ./grub-2.06 wget https://ftp.gnu.org/gnu/grub/grub-2.06.tar.gz -O grub.tar.gz # Download grub source tar -xvzf grub.tar.gz -C ./ && rm grub.tar.gz # Unzip and remove original file cd grub-2.06 && ./autogen.sh && ./configure --target=x86_64 --with-platform=efi && make # Configure & compile # Install, configure, and compile hello-world seL4 project to ./sel4-tutorials mkdir sel4-tutorials cd sel4-tutorials repo init -u https://github.com/seL4/sel4-tutorials-manifest # Install tutorials repo sync ./init --plat pc99 --tut hello-world cd hello-world_build cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -DKernelHugePage=OFF -G Ninja . # Disable huge page requirement ninja # Create final image as disk.img mkdir EFI EFI/BOOT grub-2.06/grub-mkimage -d grub-2.06/grub-core -o EFI/BOOT/BOOTX64.EFI -O x86_64-efi -p "" configfile fat part_gpt gzio multiboot video efi_gop efi_uga normal chain boot multiboot2 all_video cp sel4-tutorials/hello-world_build/images/kernel-x86_64-pc99 EFI/BOOT/sel4kernel cp sel4-tutorials/hello-world_build/images/hello-world-image-x86_64-pc99 EFI/BOOT/sel4rootserver cp grub.cfg EFI/BOOT/grub.cfg dd if=/dev/zero of=disk.img bs=1M count=35 # 35MB is just about the smallest FAT32 partition possible mformat -i disk.img@@2048s -v "EFI SYSTEM" -F # Create fat32 partition 2048 sectors in mcopy -i disk.img@@2048s -s EFI :: parted -s disk.img mklabel gpt mkpart '"EFI SYSTEM"' fat32 2048s 100% set 1 esp on # Create partition entry for ESP # Run in QEMU (most of these arguments are copied from the seL4 ./simulate script - replace OVMF path with your path to OVMF_CODE.fd for UEFI boot) qemu-system-x86_64 -cpu Nehalem,-vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce -serial mon:stdio -m size=512M -drive if=pflash,format=raw,readonly=on,file=PATH_TO_OVMF_CODE.fd -drive file=disk.img

1 0

Unblocking the caller of seL4_Call when the receiver is killed
by Arya Stevinson 13 Jun '24

13 Jun '24

Hello, I'll give a brief introduction since this is my first message here. I'm an undergraduate research assistant at the University of British Columbia, and I'm working with Margo Seltzer (https://www.seltzer.com/margo/) in the Systopia Lab. I'm helping with development of Sid Agrawal's (https://sid-agrawal.ca/) project built on seL4. I'm trying to determine what is the correct way to handle this situation: 1. Process 1 makes an seL4_Call to an endpoint that Process 2 is listening on. 2. Process 2 receives the message, and since we are running in non-MCS kernel, it will get a reply capability in its TCB. 3. Process 2 dies, for whatever reason, before it can reply to Process 1. If we wanted to unblock Process 1, what would be the correct approach? - I can use seL4_CNode_SaveCaller in Process 2 as soon as it receives a message, and store the slot number in some shared memory with the root task. Then when Process 2 dies, the root task is able to move the reply capability into its own cspace and send a reply indicating an error. This is not ideal for our purpose, because we do not want Process 2 to be able to perform any operations on its own cspace, but it needs its own root cnode capability in order to perform seL4_CNode_SaveCaller. - Is seL4_Call the wrong function for this purpose? We also considered using NBRecv and considering the call a failure after some timeout period. This is also not ideal since we would lose the convenience of the Call's reply cap, etc. - Is there some other solution that we are missing? As an aside: I notice that for the MCS kernel, if the reply cap is deleted, Process 1's thread state would be moved from ThreadState_BlockedOnReceive to ThreadState_Inactive. In non-MCS kernel, it seems that the state would remain ThreadState_BlockedOnReceive? Is there a reason for this? Best, Arya

2 2

seL4 developer hangout reminder
by Birgit Brecknell 06 Jun '24

06 Jun '24

Hi all A friendly reminder that the seL4 developer hangout is on again next week. Tue 11 Jun, 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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Multikernel in RISCV
by David Martin 06 Jun '24

06 Jun '24

Hello, I'm currently working with seL4 & Polarfire (RISCV) and I'm working with a single core at the moment (doing some testing and understanding how seL4 works). Polarfire has 4 cores and I'd like to start using all of them in a multikernel configuration (every hart running its own sel4 kernel). I've found the following RFC: https://sel4.atlassian.net/browse/RFC-17 where Kent McLeod has done some work (https://github.com/kent-mcleod/camkes-manifest/blob/kent/multicore2/master.…) but only for ARM. Does someone know if the same approach will be taken for RISCV? or even better, if someone has already done it? Thanks, David.

3 5

seL4 developer hangout reminder
by Birgit Brecknell 27 May '24

27 May '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 29 May, 8: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 Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

sel4bench grub iso
by Bengt.Lennicke＠mailbox.tu-dresden.de 24 May '24

24 May '24

Hello everyone, I am trying to create a grub iso image in order to run sel4bench on real hardware. The target architecture is x86_64 and I would prefer a grub iso because no changes to the hardware setup would be necessary then. What I did so far: I create the sel4bench images as follows mkdir sel4bench cd sel4bench repo init -u -u https://github.com/seL4/sel4bench-manifest.git repo sync mkdir build cd build ../init-build.sh -DPLATFORM=x86_64 ninja I get two elf images in the build/images directory as expected. Now in order to creat a bootable iso image i followed this guide https://www.gnu.org/software/grub/manual/grub/html_node/Making-a-GRUB-boota… Which means: mkdir -p iso/boot/grub grub-mkrescue -o grub.iso cp /path/to/kernel-x86_64-pc99 iso cp /path/to/sel4benchapp-image-x86_64-pc99 iso Then I add the grub.cfg under iso/boot/grub/grub.cfg menuentry "Load seL4 VM" --class os { multiboot /kernel-x86_64-pc99 module /sel4benchapp-image-x86_64-pc99 } There are a few lines missing from your offered grub stanza here https://docs.sel4.systems/Hardware/IA32 Mainly because I was having issues with getting it to run with them and without them I got further. Then I run grub-mkrescue -o grub.iso iso And try out the resulting iso as follows: qemu-system-x86_64 -cdrom grub.iso -nographic -enable-kvm -cpu Haswell,-vme,+pdpe1gb,+xsave,+xsaveopt,-xsavec,+fsgsbase,+invpcid,+syscall,+lm,enforce -m size=512M I get the following output: seL4 Benchmark ============== Switching to a safer, bigger stack... Setting up global fault handler... Failed to allocate object of size 140737488355328, error 1 Failed to allocate object of size 70368744177664, error 1 Failed to allocate object of size 35184372088832, error 1 Failed to allocate object of size 17592186044416, error 1 Failed to allocate object of size 8796093022208, error 1 Failed to allocate object of size 4398046511104, error 1 Failed to allocate object of size 2199023255552, error 1 Failed to allocate object of size 1099511627776, error 1 Failed to allocate object of size 549755813888, error 1 Failed to allocate object of size 274877906944, error 1 Failed to allocate object of size 137438953472, error 1 Failed to allocate object of size 68719476736, error 1 Failed to allocate object of size 34359738368, error 1 Failed to allocate object of size 17179869184, error 1 Failed to allocate object of size 8589934592, error 1 Failed to allocate object of size 4294967296, error 1 Failed to allocate object of size 2147483648, error 1 Failed to allocate object of size 1073741824, error 1 Failed to allocate object of size 536870912, error 1 Failed to allocate object of size 268435456, error 1 ipc Benchmarks ============== irquser Benchmarks ============== arch_simple_get_IOPort_cap not implemented Failed to get capability for IOPort range 0x43-0x43 PIT command failed! [Cond failed: error] Failed to init timer Benchmark failed, result 1 Register dump: rip: 0x4138a0 rsp: 0x10011640 rflags: 0x246 rax: 0x10000000 rbx: 0x10011660 rcx: 0x420c48 rdx: 0xffffffffffffffff rsi: 0x1 rdi: 0x2 rbp: 0x10011680 r8: 0x2b r9: 0x12008180c100f r10: 0x1 r11: 0x206 r12: 0x10011d88 r13: 0x10011d98 r14: 0x0 r15: 0x0 fs_base: 0x7494d0 gs_base: 0x0 [Cond failed: result == NULL] Failed to run benchmark irquser So ipc seems to run fine but irquser is not. Now I am only interested in the benchmark IPC for now. And maybe FAULT as well later. So I do not need to get irquser to run. Therefore I do the following setup again: mkdir sel4bench cd sel4bench repo init -u -u https://github.com/seL4/sel4bench-manifest.git repo sync mkdir build cd build ../init-build.sh -DPLATFORM=x86_64 and not i run ccmake . which opens a configuration screen where I can choose which benchmarks I want to include in the image. I disable everything except FASTPATH (this does not seem to be a benchmark) and IPC. I run ninja again and use the resulting images are build into an iso as stated above. Now running qemu results in this: Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa87000 end=0xd4e6a0 size=0x2c76a0 name='' Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 1fee0000 type 1 Adding physical memory region 0x100000-0x1ffe0000 Physical Memory Region from 1ffe0000 size 20000 type 2 Physical Memory Region from feffc000 size 4000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Got VBE info in multiboot. Current video mode is 3 ACPI: RSDP paddr=0xf5b20 ACPI: RSDP vaddr=0xf5b20 ACPI: RSDT paddr=0x1ffe1550 ACPI: RSDT vaddr=0x1ffe1550 Kernel loaded to: start=0x100000 end=0xa14000 size=0x914000 entry=0x10040b ACPI: RSDT paddr=0x1ffe1550 ACPI: RSDT vaddr=0x1ffe1550 ACPI: FADT paddr=0x1ffe1404 ACPI: FADT vaddr=0x1ffe1404 ACPI: FADT flags=0x80a5 ACPI: 0 IOMMUs detected ACPI: MADT paddr=0x1ffe1478 ACPI: MADT vaddr=0x1ffe1478 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: size=0x242000 v_entry=0x449631 v_start=0x400000 v_end=0x642000 p_start=0xd4f000 p_end=0xf91000 Moving loaded userland images to final location: from=0xd4f000 to=0xa14000 size=0x242000 Starting node #0 with APIC ID 0 Mapping kernel window is done available phys memory regions: 1 [100000..1ffe0000] reserved virt address space regions: 1 [ffffff8000100000..ffffff8000c56000] Booting all finished, dropped to user space seL4 Benchmark ============== Switching to a safer, bigger stack... Setting up global fault handler... vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 140737488355328, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 70368744177664, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 35184372088832, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 17592186044416, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 8796093022208, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 4398046511104, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 2199023255552, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 1099511627776, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 549755813888, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 274877906944, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 137438953472, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 68719476736, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 34359738368, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 17179869184, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 8589934592, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 4294967296, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 2147483648, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 1073741824, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 536870912, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 268435456, error 1 ipc Benchmarks ============== libsel4muslcsys: Error attempting syscall 228 libsel4muslcsys: Error attempting syscall 96 JSON OUTPUT [{"Benchmark": "One way IPC microbenchmarks", "Results": [{"Function": "seL4_Call", "Direction": "client->server", "Client Prio": 254, "Server Prio": 254, "Same vspace?": true, "IPT .... All is well in the universe. Fin So the benchmark runs but now a libsel4muslcsys error is new. syscall 228 is sys_clock_gettime so I assume it is important for the benchmark and even so it is not terminating I am not sure whether the results are correct with that error. So somehow removing the other benchmarks resulted in an error in the ipc benchmark which was not there or at least not shown there when compiling with all benchmarks. When trying to find out which removal is causing the problem a variety of other problems is appearing. Do you think the musllib error is related to the missing lines in the grub.cfg? If so do you have an idea which one? Why do the different benchmarks influence each other, am I compiling it wrong? If there are information missing feel free to let me know and I will try to add them Kind regards, Bengt

2 2

Register for the seL4 summit 2024
by Birgit Brecknell 17 May '24

17 May '24

The seL4 summit 2024 [0] will be held in Sydney, Australia, 15-17 October 2024. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: * Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions * Networking with other seL4 experts and enthusiasts * Reception and dinner Register here [1] The early bird cut-off date is 15 September 2024. Local seL4 Sydney-siders will look into organising some informal activities for Monday 14 October 2024, before the summit kicks off, for anyone who wants to join. Gernot may also organise a bush walk for the weekend before the summit. Stayed tuned for more info! [0] https://sel4.systems/Foundation/Summit/2024 [1] https://events.linuxfoundation.org/sel4-summit/ Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Loading a large sel4test image on Odroid-C4 Fails
by Linh Pham 16 May '24

16 May '24

Hello, I am running into an issue with booting up an sel4test image on the Odroid-C4. When the calculated memory bound for the sel4test-driver's ELF is around 100MB or larger, I get an asychronous data abort like so: ELF-loader started on CPU: ARM Ltd. Cortex-A55 r1p0 paddr=[c3d2000..e068117] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at c502760. Loaded DTB from c502760. paddr=[256000..261fff] ELF-loading image 'kernel' to 0 paddr=[0..255fff] vaddr=[8000000000..8000255fff] virt_entry=8000000000 ELF-loading image 'sel4test-driver' to 262000 paddr=[262000..6cd7fff] vaddr=[400000..6e75fff] virt_entry=443090 "Error" handler, esr 0xbe000011 elr: ffffffff1a4996e4 lr : ffffffff1a497654 (reloc) elr: 000000000c3d96e4 lr : 000000000c3d7654 x0 : 0000000001ad7340 x1 : 0000000000000000 x2 : 0000000006a75348 x3 : 000000000c3dfdc0 x4 : 0000000001b494c8 x5 : 000000000c3dca50 x6 : 0000000000262000 x7 : 0000000000000001 x8 : 0000000000000008 x9 : ffffffffffffffff x10: 0000000000000000 x11: 0000000000000002 x12: 00000000f4fef9e0 x13: 0000000000000001 x14: 00000000f4fef9e0 x15: 0000000000000000 x16: 0000000020000000 x17: 0000000000c0c0c0 x18: 00000000f0f3dda0 x19: 000000000c3dfff0 x20: 0000000020000000 x21: 0000000000000002 x22: 00000000f0f769c0 x23: 0000000000000002 x24: 00000000f2ff556c x25: 0000000000000000 x26: 0000000000000000 x27: 0000000000000000 x28: 00000000f0f6d380 x29: 000000000c3dfda0 Code: f94017e0 91002000 f90017e0 f94007e0 (f1001c1f) Resetting CPU ... Our sel4test image is large because we're using a static heap. Note that the relevant region from the log output is [262000..6cd7fff], the exception occurs when trying to write into memory in this range. After some investigation, writing to physical address 0x5100000 is what causes the problem. I haven't been able to find any documentation on why this physical address range can't be written to. Is this some sort of device memory region? I was able to eventually boot by changing the ELF loader to load into a much higher memory address (e.g. somewhere around 0x80000000), but I would like to have a clearer idea of the Odroid's memory layout so that I could choose an address range that is definitely safe to load the image into. Thank you, Linh

2 2

seL4 docker support for Apple Silicon
by Gerwin Klein 15 May '24

15 May '24

The seL4 development docker containers at https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles now provide multi-architecture images for x86 and arm64. That means development on Apple Silicon (M1/2/3) with docker for seL4 should now work properly (including qemu) and should also be much faster than before. Intel machines should work as before. You should not need to do anything special or different to before, Docker should be pulling the correct kind of container for your architecture. This is brand new (as of today), so please check it out and report any issues you find. If you haven’t used the containers before, have a look at the README in the repository above. If you have been using them and want to make sure that the new versions are picked up: cd seL4-CAmkES-L4v-dockerfiles/ git checkout master git pull make pull_camkes_image user Enjoy! Gerwin

1 0

Re: Announcing release v0.2 of Neptune OS: a Windows NT personality for the seL4 microkernel
by Hugo V.C. 14 May '24

14 May '24

Are we talking about the same ReactOS ... ? As far I can see here: https://reactos.org/forum/ they have an active community. Try to post there. You also have this LinkedIn resource: https://www.linkedin.com/company/reactos-foundation/ Let me know if you have any problem contacting them and I'll try to help you. seL4 + ReactOS looks like a killer combination for the industry, they need to know about your work. Best, El lun, 13 may 2024 a las 15:07, Dr. Chang Liu, PhD. (<cl91tp(a)gmail.com>) escribió: > Dear Hugo, > > Thank you very much for your interest. I did try to find the ReactOS > mailing list to post this announcement in but it seems that their mailing > list has long been dead since late 2022, so I'm not sure where the main > communication channel of ReactOS development is. Perhaps you could point me > to the right place. > > Best regards, > > On Mon, May 13, 2024, 12:50 AM Hugo V.C. <skydivebcn(a)gmail.com> wrote: > >> Hats off. >> I'll test it and give my feedback. I'm very interested in your project, >> IMHO is one of the most interesting ones I have seen in years. >> >> BTW: are you in contact with ReactOS guys? Maybe would make sense to join >> efforts with them...? >> >> El dom, 12 may 2024 a las 17:40, Dr. Chang Liu, PhD. (<cl91tp(a)gmail.com>) >> escribió: >> >>> Dear seL4 community, >>> >>> I'm announcing the release of v0.2 of Neptune OS, an operating system >>> that >>> I have been developing that aims to create a Windows NT personality on >>> top >>> of the seL4 microkernel, by implementing the upper layer of the Windows >>> kernel called the NT Executive, as well as Windows kernel drivers, as >>> userspace processes under seL4. For those that remember the release of >>> v0.1 >>> two years ago and have been wondering, yes, the project is still alive. I >>> have been a bit busy with postdoc work (academia is hard!!) last year but >>> finally got a bit of free time lately to get enough work done that I >>> think >>> is interesting enough to warrant a v0.2 release. The project can be found >>> on github (https://github.com/cl91/NeptuneOS) >>> >>> The biggest feature of the v0.2 release is a (I hope) reasonably complete >>> file system stack supporting read-ahead and write-back caching, that >>> includes a FAT12/16/32 file system driver and a floppy controller driver, >>> both of which are ported over from ReactOS (but running in userspace >>> instead of kernel space). I'll explain the technical points below but you >>> can watch a short video (https://www.youtube.com/watch?v=o3FLRnkh0ic) >>> that >>> demonstrates the basic file system commands, including cd, dir, copy, >>> move, >>> del, md, and mount/umount. >>> >>> Arguably the biggest challenge for a userspace file system stack is >>> minimizing the performance penalties of the additional context switches. >>> There are radical solutions to this problem along the lines of Unikernels >>> that require linking the FS code with the applications. These solutions >>> are >>> not very practical for everyday desktop or server OSes. On traditional >>> OSes >>> there is FUSE on Linux/Unix which is often regarded as having inferior >>> performance compared to equivalent kernel-mode drivers. To some extent >>> this >>> problem is inevitable, as context switches are always more expensive than >>> function calls, no matter how much you optimize the former. However, that >>> doesn't mean we can't optimize our OS design so that the performance >>> penalties of running file systems in userspace are small enough that the >>> benefit of userspace file systems outweighs their performance cons. >>> >>> The key to this performance goal I believe is an efficient cache design. >>> Indeed, for FUSE it is possible to tune the cache parameters to >>> drastically >>> increase its performance (see [1] and the citation therein). On Neptune >>> OS >>> we cache aggressively: not only do we cache the underlying block device >>> pages, we also maintain the relationship between file regions and their >>> underlying disk regions. In other words, the primary role of the file >>> system driver is to translate an offset of a file object into an offset >>> of >>> the underlying storage device, and this relationship is cached since they >>> are not expected to change, at least for currently open files. >>> Furthermore, >>> we cache file attributes as well as the file hierarchy itself, so that >>> if a >>> process opened a file and the file system driver returned a valid handle, >>> we do not need to query the FS driver again (at least not before the >>> first >>> process closes the handle) when another process opens the same file with >>> the same attributes (because we know it exists and know about its >>> attributes). Of course, we need to be careful when things get >>> closed/deleted/moved, etc, so we need a mechanism to synchronize >>> information with the file system driver process. This is done by sending >>> messages using the seL4 IPC. >>> >>> What is amazing is the fact that despite these changes to the inner >>> workings of the NT cache manager, not to mention the fact that all >>> drivers >>> are now running in userspace, the Windows kernel driver API remains >>> largely >>> unchanged, so that it is indeed possible to port the relevant ReactOS >>> drivers to our architecture without doing too much work (I believe I >>> spent >>> three to four man-weeks worth of work porting the FAT file system >>> itself). >>> The vast majority of work is in fact removing code rather than writing >>> new >>> code, because of the simplifications of locking and other synchronization >>> issues that simply disappear when drivers run in userspace. For those who >>> are interested in knowing more about our architecture and are perhaps >>> interested in porting drivers from ReactOS, I am in the process of >>> writing >>> a book (found under the docs of the github repo) called "Neptune OS >>> Developer Guide" that explains all these things. Note this is very much a >>> work-in-progress. >>> >>> In addition to the cache manager work, in order for the file system stack >>> to function, several other system components must be implemented, most >>> notably DMA and Win32 SEH (structured exception handling). Our DMA >>> architecture supports both PCI bus mastering and the weird ISA DMA that >>> must go through the ISA DMA controller. The latter requires managing the >>> so-called "map registers" that must be shared across different ISA >>> devices. >>> Again we find that the Windows kernel API can be adapted to a seL4-based >>> userspace driver model almost straightforwardly. This is perhaps not so >>> surprising, because NT was allegedly originally designed as a microkernel >>> OS (this is inevitably an urban legend, but early NT design documents >>> refer >>> to the code beneath the NT Executive as the "microkernel", so there is >>> reason to believe). >>> >>> To summarize, what I hope is that with the design outlined above, we can >>> in >>> fact have a practical, reasonably performant userspace file system stack >>> without resorting to radical departures from traditional desktop/server >>> computing paradigms. Of course, it's ridiculous to talk about performance >>> for floppy disk controllers, so the primary goal of the next release is >>> to >>> port the ATA/AHCI hard disk drivers from ReactOS to Neptune OS, in order >>> to >>> produce a valid benchmark against equivalent kernel mode designs. Anyway, >>> if you read so far, I hope you find the work interesting (I personally >>> do!). If you have any comments, or even better if you ran the code and >>> found bugs/issues, please do open an issue in the github repo. Thank you! >>> >>> [1] >>> >>> https://medium.com/@xiaolongjiang/linux-fuse-file-system-performance-learni… >>> >>> --- >>> Dr. Chang Liu, PhD. >>> github.com/cl91/NeptuneOS >>> _______________________________________________ >>> Devel mailing list -- devel(a)sel4.systems >>> To unsubscribe send an email to devel-leave(a)sel4.systems >>> >>

1 0

seL4 developer hangout reminder
by Birgit Brecknell 13 May '24

13 May '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 14 May, 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

Announcing release v0.2 of Neptune OS: a Windows NT personality for the seL4 microkernel
by Dr. Chang Liu, PhD. 13 May '24

13 May '24

Dear seL4 community, I'm announcing the release of v0.2 of Neptune OS, an operating system that I have been developing that aims to create a Windows NT personality on top of the seL4 microkernel, by implementing the upper layer of the Windows kernel called the NT Executive, as well as Windows kernel drivers, as userspace processes under seL4. For those that remember the release of v0.1 two years ago and have been wondering, yes, the project is still alive. I have been a bit busy with postdoc work (academia is hard!!) last year but finally got a bit of free time lately to get enough work done that I think is interesting enough to warrant a v0.2 release. The project can be found on github (https://github.com/cl91/NeptuneOS) The biggest feature of the v0.2 release is a (I hope) reasonably complete file system stack supporting read-ahead and write-back caching, that includes a FAT12/16/32 file system driver and a floppy controller driver, both of which are ported over from ReactOS (but running in userspace instead of kernel space). I'll explain the technical points below but you can watch a short video (https://www.youtube.com/watch?v=o3FLRnkh0ic) that demonstrates the basic file system commands, including cd, dir, copy, move, del, md, and mount/umount. Arguably the biggest challenge for a userspace file system stack is minimizing the performance penalties of the additional context switches. There are radical solutions to this problem along the lines of Unikernels that require linking the FS code with the applications. These solutions are not very practical for everyday desktop or server OSes. On traditional OSes there is FUSE on Linux/Unix which is often regarded as having inferior performance compared to equivalent kernel-mode drivers. To some extent this problem is inevitable, as context switches are always more expensive than function calls, no matter how much you optimize the former. However, that doesn't mean we can't optimize our OS design so that the performance penalties of running file systems in userspace are small enough that the benefit of userspace file systems outweighs their performance cons. The key to this performance goal I believe is an efficient cache design. Indeed, for FUSE it is possible to tune the cache parameters to drastically increase its performance (see [1] and the citation therein). On Neptune OS we cache aggressively: not only do we cache the underlying block device pages, we also maintain the relationship between file regions and their underlying disk regions. In other words, the primary role of the file system driver is to translate an offset of a file object into an offset of the underlying storage device, and this relationship is cached since they are not expected to change, at least for currently open files. Furthermore, we cache file attributes as well as the file hierarchy itself, so that if a process opened a file and the file system driver returned a valid handle, we do not need to query the FS driver again (at least not before the first process closes the handle) when another process opens the same file with the same attributes (because we know it exists and know about its attributes). Of course, we need to be careful when things get closed/deleted/moved, etc, so we need a mechanism to synchronize information with the file system driver process. This is done by sending messages using the seL4 IPC. What is amazing is the fact that despite these changes to the inner workings of the NT cache manager, not to mention the fact that all drivers are now running in userspace, the Windows kernel driver API remains largely unchanged, so that it is indeed possible to port the relevant ReactOS drivers to our architecture without doing too much work (I believe I spent three to four man-weeks worth of work porting the FAT file system itself). The vast majority of work is in fact removing code rather than writing new code, because of the simplifications of locking and other synchronization issues that simply disappear when drivers run in userspace. For those who are interested in knowing more about our architecture and are perhaps interested in porting drivers from ReactOS, I am in the process of writing a book (found under the docs of the github repo) called "Neptune OS Developer Guide" that explains all these things. Note this is very much a work-in-progress. In addition to the cache manager work, in order for the file system stack to function, several other system components must be implemented, most notably DMA and Win32 SEH (structured exception handling). Our DMA architecture supports both PCI bus mastering and the weird ISA DMA that must go through the ISA DMA controller. The latter requires managing the so-called "map registers" that must be shared across different ISA devices. Again we find that the Windows kernel API can be adapted to a seL4-based userspace driver model almost straightforwardly. This is perhaps not so surprising, because NT was allegedly originally designed as a microkernel OS (this is inevitably an urban legend, but early NT design documents refer to the code beneath the NT Executive as the "microkernel", so there is reason to believe). To summarize, what I hope is that with the design outlined above, we can in fact have a practical, reasonably performant userspace file system stack without resorting to radical departures from traditional desktop/server computing paradigms. Of course, it's ridiculous to talk about performance for floppy disk controllers, so the primary goal of the next release is to port the ATA/AHCI hard disk drivers from ReactOS to Neptune OS, in order to produce a valid benchmark against equivalent kernel mode designs. Anyway, if you read so far, I hope you find the work interesting (I personally do!). If you have any comments, or even better if you ran the code and found bugs/issues, please do open an issue in the github repo. Thank you! [1] https://medium.com/@xiaolongjiang/linux-fuse-file-system-performance-learni… --- Dr. Chang Liu, PhD. github.com/cl91/NeptuneOS

2 1

seL4 multicore boot failed on arm64
by Leonid Meyerovich 10 May '24

10 May '24

Hello, I run my seL4 application on 4 core ARMv8. Recently I have developed some more application code (I mention it because file system size is increased an I believe it may change boot time) and from time to time I observed that boot process failed (stuck after the following print) calling schedule calling activate thread kernel boot done.. CPU=1 calling schedule calling activate thread kernel boot done.. CPU=2 calling schedule calling activate thread kernel boot done.. CPU=3 Booting all finished, dropped to user space calling schedule calling activate thread kernel boot done.. CPU=0 Some time I see that only 2 CPU have been booted (like CPU1 and CPU3, or CPU2 and CPU3) Last print is the last one in init_kernel() function Thanks you, Leonid

2 3

Building seL4test 12.1.0 fails on Ubuntu 22.04 (WSL2)
by Ben McCart 09 May '24

09 May '24

I have run into the following build error when running ninja to build seL4test (following instructions at: https://docs.sel4.systems/GettingStarted#setting-up-your-machine) Here is what I get for output. Any suggestions on a work-around? (Do I have the wrong version of a python tool or library?) -- [65/263] Generating circular_includes_valid FAILED: kernel/circular_includes_valid /home/dev/seL4test/build-x86/kernel/circular_includes_valid cd /home/dev/seL4test/build-x86/kernel && /home/dev/seL4test/kernel/tools/circular_includes.py --ignore kernel_all_copy.c < kernel_all.i && touch circular_includes_valid Traceback (most recent call last): File "/home/dev/seL4test/kernel/tools/circular_includes.py", line 74, in <module> sys.exit(main(args)) File "/home/dev/seL4test/kernel/tools/circular_includes.py", line 61, in main while file_stack[-1] != header: IndexError: list index out of range [66/263] Invoking muslc build system /home/dev/seL4test/projects/musllibc/src/prng/seed48.c:6:40: warning: argument 1 of type ‘short unsigned int *’ declared as a pointer [-Warray-parameter=] 6 | unsigned short *seed48(unsigned short *s) | ~~~~~~~~~~~~~~~~^ In file included from /home/dev/seL4test/projects/musllibc/src/prng/seed48.c:1: /home/dev/seL4test/projects/musllibc/include/stdlib.h:133:25: note: previously declared as an array ‘short unsigned int[3]’ 133 | unsigned short *seed48 (unsigned short [3]); | ^~~~~~~~~~~~~~~~~~ /home/dev/seL4test/projects/musllibc/src/unistd/getcwd.c: In function ‘getcwd’: cc1: warning: function may return address of local variable [-Wreturn-local-addr] /home/dev/seL4test/projects/musllibc/src/unistd/getcwd.c:9:14: note: declared here 9 | char tmp[PATH_MAX]; | ^~~ ninja: build stopped: subcommand failed.

2 2

seL4 developer hangout reminder
by Birgit Brecknell 29 Apr '24

29 Apr '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 1 May, 8: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 summit: deadline extension to 29 April 2024
by Birgit Brecknell 22 Apr '24

22 Apr '24

The deadline to submit a presentation to the seL4 summit 2024 [0] has been extended by 1 week. You now have until 29 April 2024 to propose a talk [1], by uploading an abstract of one page or less to the submission portal [2]. 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. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://sel4.systems/Foundation/Summit/2024/cfp [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