February 2026 - Devel - lists.sel4.systems

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

seL4 developer hangout reminder
by Birgit Brecknell 02 Feb '26

02 Feb '26

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