- Devel - lists.sel4.systems

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

Question about LionsOS
by Isaac Beckett 20 Apr '24

20 Apr '24

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

11 26

Release 0.1.0 of LionsOS
by Ivan Velickovic 16 Apr '24

16 Apr '24

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

1 0

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

15 Apr '24

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

1 0

seL4 developer hangout reminder
by Birgit Brecknell 15 Apr '24

15 Apr '24

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

1 0

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

14 Apr '24

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

2 2

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

09 Apr '24

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

1 0

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

08 Apr '24

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

1 0

sel4test CACHEFLUSH0001 failed
by Leonid Meyerovich 29 Mar '24

29 Mar '24

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

2 2

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

26 Mar '24

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

3 3

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

25 Mar '24

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

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 25 Mar '24

25 Mar '24

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

1 0

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

25 Mar '24

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

2 1

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

20 Mar '24

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

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 18 Mar '24

18 Mar '24

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

1 0

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

15 Mar '24

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

2 1

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

09 Mar '24

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

2 2

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

09 Mar '24

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

1 0

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

09 Mar '24

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

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 04 Mar '24

04 Mar '24

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

1 0

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

26 Feb '24

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

2 1

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

19 Feb '24

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

5 5

Reminder seL4 developer hangout
by Birgit Brecknell 19 Feb '24

19 Feb '24

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

1 0

new RFCs
by Gerwin Klein 13 Feb '24

13 Feb '24

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

1 0

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

12 Feb '24

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

3 4

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

08 Feb '24

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

2 6

Reminder seL4 developer hangout
by Birgit Brecknell 05 Feb '24

05 Feb '24

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

1 0

fault processing
by Leonid Meyerovich 27 Jan '24

27 Jan '24

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

2 3

seL4 fault processing
by Leonid Meyerovich 25 Jan '24

25 Jan '24

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

4 5

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

25 Jan '24

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

1 0

seL4 fault handling
by Leonid Meyerovich 24 Jan '24

24 Jan '24

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

3 3

Reminder seL4 developer hangout
by Birgit Brecknell 22 Jan '24

22 Jan '24

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

1 0

Reminder seL4 developer hangout
by Gerwin Klein 09 Jan '24

09 Jan '24

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

1 0

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

18 Dec '23

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

2 2

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

14 Dec '23

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

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 11 Dec '23

11 Dec '23

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

1 0

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

05 Dec '23

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

2 9

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

29 Nov '23

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

2 3

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

29 Nov '23

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

2 2