- Devel - lists.sel4.systems

seL4 developer hangout reminder
by Birgit Brecknell 24 Apr '26

24 Apr '26

Hi all A friendly reminder that the seL4 developer hangout is on again next week. Wed 29 Apr, 8:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar 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

Last day to submit a talk proposal to the sel4 summit!
by June Andronick 21 Apr '26

21 Apr '26

It only requires an abstract describing your talk proposal. https://form.jotform.com/260147181364858 Looking forward to your submissions. Cheers, June

1 1

seL4 summit 2026: one week to go to submit a talk
by Birgit Brecknell 13 Apr '26

13 Apr '26

One week to go to submit a talk [0] for the seL4 Summit 2026 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. **Abstracts are due on 20 April 2026.** **NEW!** The 2026 edition of the seL4 summit will feature a **full first day** dedicated to **applications, overviews, and perspectives** on seL4-based systems and formally verified software in the real world. This will be followed by Days 2 and 3 focusing on more technical development, research, reports, and discussions. We are particularly keen to **welcome people who are new to seL4** or still developing their familiarity with the technology. The event will offer an **ideal opportunity to gain a high-level view of the landscape and ecosystem** of seL4 and its associated tools, frameworks and languages, as well as formally verified software in general, and to take stock of the latest updates. The seL4 Summit 2026 will be held 1 - 3 September 2026 at the Hyatt Regency Vancouver, Vancouver, Canada. The summit will be an in-person event. We’re looking forward to many exciting proposals! [0] https://sel4.systems/Summit/2026/cfp [1] https://sel4.systems/Summit/2026/ [2] https://form.jotform.com/260147181364858 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 13 Apr '26

13 Apr '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 14 Apr, 22:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar 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 31 Mar '26

31 Mar '26

We're pleased to announce the release of - seL4 15.0.0: The seL4 microkernel https://docs.sel4.systems/releases/sel4/15.0.0 - Microkit 2.2.0: The seL4 Microkit for building static-architecture systems https://docs.sel4.systems/releases/microkit/2.2.0 - CAmkES 3.12.0: Component Architecture for microkernel-based Embedded Systems https://docs.sel4.systems/releases/camkes/camkes-3.12.0 - capDL 0.5.0: Tools for generating, parsing and loading capability distribution specifications https://docs.sel4.systems/releases/capdl/0.5.0 - rust-sel4 4.0.0: Rust support for seL4 userspace https://github.com/seL4/rust-sel4/releases/tag/v4.0.0 seL4 15.0.0 and the corresponding Rust support come with new features and will require updates if you are using the seL4 API directly. CAmkES and the capDL tool add domain schedules as a new feature and applications will need updates if they use the seL4 domain scheduler. The Microkit release should not require any update of user code compared to Microkit 2.1.0. Enjoy! Gerwin

1 0

seL4 developer hangout reminder
by Birgit Brecknell 30 Mar '26

30 Mar '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 1 Apr, 7:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar 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 16 Mar '26

16 Mar '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 17 Mar, 21:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar 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 02 Mar '26

02 Mar '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 4 Mar, 7:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar 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 16 Feb '26

16 Feb '26

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 17 Feb, 21:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar 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

issue with elfloader ret instruction while enabling the MMU on armv8-a
by Christian Bruel 11 Feb '26

11 Feb '26

Hello seL4 team, I would like to share an issue found with the port of seL4 and VMs to the STM32MP2 SoC, which features Armv8-A dual Cortex-A35 cores: When activating the secondary core, The RET instruction crashes while executing the arm_enable_mmu(). The exception stack and ESR register show no useful information. Simply replacing the RET instruction with BR X30 resolves the issue. Furthermore, before RET, a check with the AT S1E1R, X30 shows correct memory translation in the PAR_EL1 register, confirming proper MMU setting, which is also supported by the successful BR X30 workaround. Just to be sure I tried to replace the current 1Gb translation table with a finer 4Bb granularity and P:EX U:NX and RO access flags for the Non Secure code execution. Same results. I also set the ASID bits, same result. So back to the current implementation and BR X30 workaround: According to the Arm Architecture Reference Manual [1], the RET instruction behaves identically to BR but provides an additional hint that this is a return from a subroutine. AFAIU, such hints can be related to the branch predictor or the return address stack used for ROP protection, (if the feature is available). In “Requirements for branch predictor maintenance” [2], branch prediction maintenance operations must be performed after enabling or disabling the MMU. However, these operations translate as a NOP if the branch predictor hardware is not architecturally visible. Therefore, the ‘BL/RET’ behavior from different translation regime seems to to be implementation-dependent or dependent on optional architectural features Thus, replacing MMU enable sequence: enable_mmu sctlr_el1 x8 ldp x29,x30,[sp],#16 ret with a trampoline: adr x30,mmu_on ldp x29,x9,[sp],#16 ret mmu_on: enable_mmu sctlr_el1,x8 br x9 is enough to start seL4 with SMP=on NUM_NODES=2 and run a dual core Linux on the CAmkES VM. This is semantically equivalent to the BL X30 workaround, but this is more explicit regarding the MMU translation regime around BL/RET. NB: arm_enable_hyp_mmu() needs the same change as the issue happens equivalently in EL1 or EL2. Thank you very much for your thoughts on this issue. Best Regards Christian References: [1] Arm Architecture Reference Manual (DTI 0487) [2] Arm Architecture Reference Manual ARMv7-A and ARMv7-R edition

2 4