aarch64: Restrict address mappings in loader.rs by bruelc · Pull Request #464 · seL4/microkit

bruelc · 2026-04-01T11:28:11Z

Hello,

This is a rework of the existing support committed in elfloader:
seL4/seL4_tools#244
and discussed here:
https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/DJNDO5CUQBKGIA4SQHXCNQ3T6SKZEY4A/

This patch limits the 1:1 address mapping in the loader to cover only the necessary blocks using level-2 translation tables with 2MB blocks. The UART MMIO address is now exposed as a global uart_addr variable.

This prevents speculative accesses to device or secure memory, which could otherwise cause faults or unwanted side effects.

This has been tested only on STM32MP2. Testers on other platforms would be greatly appreciated.

Thank you for your review.

midnightveil

Fine. Just some minor code cleanups to do.

midnightveil · 2026-04-02T06:11:36Z

+            .expect("Could not find 'end' symbol");
+
+        if Aarch64::lvl1_index(text_addr) != Aarch64::lvl1_index(end_addr) {
+            eprintln!("ERROR: We only map 1GiB, but elfloader paddr range covers multiple GiB");


I think we tend to use panic!("INTERNAL: <message>") here.

I'd also reword this: specifically the issue is the microkit loader (not elfloader) crosses a GiB boundary [or really that it requires multiple level 1 page tables].

It likely makes sense to do this change to both AArch64 and Riscv64, no sense it being different for either.

I am not familiar with the Riscv64 MMU tables, and I do not have access to a testing platform. Is there any volunteer to do the adaptation?

That's fair. We're planning on changing a few things after these are good to go, anyway, and having to retest.

thank you. I noticed the CI doesn’t build for riscv64 without uart_addr. I’ll guard it to fix the build before your changes.

midnightveil · 2026-04-02T06:16:17Z

+        if let Ok((uart_addr, _)) = elf.find_symbol("uart_addr") {
+	    let data = elf
+	        .get_data(uart_addr, 8)
+		.expect("uart_addr not initialized");
+	    let uart_base = u64::from_le_bytes(data[0..8].try_into().unwrap());


(Not something you need to fix, just making this comment so I can link to it later):

It'd be nice if the kernel exposed the virtual address of where it wants its UART so we can map that in and get this feature working again.

midnightveil · 2026-04-02T06:19:02Z

+
+        let mut boot_lvl2_lower: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
+
+        let pt_entry = (boot_lvl2_lower_addr | 3).to_le_bytes();


can we be consistent with the other examples and split out the meanings of the 3 flags into the individual bits?

This this is a 2 bit marker for the 1GB L1 table entry here, not individual bits

Ah, right, we do |3 in a bunch of places below. I'll change that at a later point.

Thanks, better to handle it globally yes. I’ll add a comment since “3” means different things depending on the granule (page or table)

midnightveil · 2026-04-10T05:04:40Z

+            let pt_entry: u64 = (entry_idx as u64 + start_addr) |
+                (1 << 10) | // Access flag
+                (3 << 8) | // Sharable
+                (3 << 2) | // MT_NORMAL memory


Looking at this more. Did you intentionally make this 3 << 2? That would correspond to MT_NORMAL_NC, not MT_NORMAL.

Argh no! That’s an early debugging trace… thanks for noticing.

Fixed: Note that I also had to update #465 to flush the cache before jumping to the secondary core

midnightveil · 2026-04-23T03:09:50Z

~~OK, I'll note that this appears to have broken most of our boards even in non-SMP mode. They all seem to error out with: (e.g. for the MaaXboard)~~

EDIT: no this was just a dirty build. rerunning it everything works in debug mode (for non-smp)

log

Bootstrapping kernel
available phys memory regions: 1
  [40000000..c0000000)
reserved virt address space regions: 2
  [8040000000..8040246000)
  [8040246000..804029e000)
Booting all finished, dropped to user space
panicked at /home/julia/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/rkyv-0.8.12/src/option.rs:38:17:
called `ArchivedOption::unwrap()` on a `None` value
(aborted)
Found thread has no fault handler while trying to handle:
unknown fault
in thread 0x80bfc07400 "rootserver" at address 0x2219e8
With stack:
0x24dc80: 0x221bd8
0x24dc88: 0x24dcd8
0x24dc90: 0x221b5c
0x24dc98: 0x221b5c
0x24dca0: 0x221b30
0x24dca8: 0x24dcd8
0x24dcb0: 0x22d550
0x24dcb8: 0x24f2ec
0x24dcc0: 0x0
0x24dcc8: 0x2055c8
0x24dcd0: 0x67
0x24dcd8: 0x24dcc8
0x24dce0: 0x205600
0x24dce8: 0x1
0x24dcf0: 0x0
0x24dcf8: 0x221118

~~This is just building the hello world example in debug mode.~~
~~I'm somewhat unsure how, though.~~

Limit the 1:1 address mapping in the loader to cover only the necessary blocks using level-2 translation tables and with 2MB blocks. Don't map device memory at all, therefore, printf must not be used in the elfloader after the MMU is enabled. This prevents speculative accesses to device or secure memory which otherwise would cause faults or unwanted side-effects. Signed-off-by: Christian Bruel <christian.bruel@foss.st.com>

The previous commit restricts the loader to only mapping itself rather than the first 1GB of memory. This is fine for most platforms as the only other thing they need to access is the UART which is now also separately mapped in. The one exception is the BCM2711/Raspberry Pi 4B where the a spin table is used for SMP booting which is located in the first page of memory, so we need to explicitly map that in as well. This code is a bit of hack since it assumes the CPU release addrs are always in the first 2MB of memory but the only platform we have right now that uses spin tables is the Raspberry Pi 4B. So we can merge the previous patch, we add this so that we don't have to regress the Raspberry Pi 4B. Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>

Ivan-Velickovic · 2026-04-24T04:30:46Z

Rebased on main + pushed a temporary fix for the Raspberry Pi 4B so we don't regress that platform with this change. Also changed the mapping code so that it still maps the loader as strongly ordered, we did this because we don't want to worry about flushing caches for this PR (without flushing caches we'd still have issues on Raspberry Pi 4B).

Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>

Ivan-Velickovic · 2026-04-24T04:36:39Z

temporary fix for the Raspberry Pi 4B

I should add that the reason I say 'temporary' is since @midnightveil has in-progress patches to re-write all of this loader mapping code to be easier to read/better structured so we'll revisit as part of that.

midnightveil · 2026-04-24T04:52:01Z

I'm also going to note down here why this was necessary, as it's not completely obvious from the fact, as the 1GB mapping the loader used was already DEVICE_nGnRnE ('strongly ordered').

See this discussion: seL4/seL4_tools#244 (comment)

The conclusion is that ARM seems to allow speculative reads of instructions even in DEVICE_nGnRnE memory unless the XN bit is set. This contrasts to data loads/stores which are not (speculatively) permitted.

References in ARM ARM DDI 0487L.B, under §D8.4.4 "Effects on instruction execution permissions and restrictions on instruction fetch":

$I_{PTMPK}$ If Device memory is not execute-never, then speculative instruction fetch from that memory region is permitted.
$I_{ZZSZZ}$ For all Exception levels from which a read-sensitive memory region can be accessed, to avoid the possibility of a speculative fetch affecting that memory region, software is expected to define that memory region as execute-never.

In contrast, under §B2.10.2 "Device memory", it states:

Speculative data accesses are not permitted to any memory location with any Device memory attribute. This means that each memory access to any Device memory type must be one that would be generated by a simple sequential execution of the program.
[...]
Hardware does not prevent speculative instruction fetches from a memory location with any of the Device memory attributes unless the memory location is also marked as execute-never for all Exception levels.

bruelc · 2026-04-24T09:06:24Z

Just noticed that the commit log was copied from the CAmKes tool loader and the sentence:

Don't map device memory at all, therefore, printf must not be used in the elfloader after the MMU is enabled.

doesn't apply for Microkit elf loader.

Could you please amend the committed log and remove this sentence ?

sorry about this, thank you.

bruelc mentioned this pull request Apr 1, 2026

Add stm32mp2 support #446

Open

midnightveil approved these changes Apr 2, 2026

View reviewed changes

midnightveil mentioned this pull request Apr 2, 2026

fix aarch64 MMU fixes - don't disable it #466

Open

bruelc mentioned this pull request Apr 2, 2026

loader,smp: Enable caches on all cores for shareability #465

Open

bruelc force-pushed the master-mmuloader branch 3 times, most recently from 0b1d9ca to 12dd82c Compare April 7, 2026 10:33

midnightveil reviewed Apr 8, 2026

View reviewed changes

Comment thread tool/microkit/src/loader.rs Outdated

bruelc force-pushed the master-mmuloader branch from 12dd82c to 9dbc0d7 Compare April 8, 2026 07:38

midnightveil reviewed Apr 10, 2026

View reviewed changes

bruelc force-pushed the master-mmuloader branch from 9dbc0d7 to b62c440 Compare April 10, 2026 08:43

midnightveil approved these changes Apr 14, 2026

View reviewed changes

bruelc and others added 2 commits April 24, 2026 13:56

Ivan-Velickovic force-pushed the master-mmuloader branch from 38a2907 to 2ca916e Compare April 24, 2026 04:26

Loader name consistency

b9ccceb

Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>

Ivan-Velickovic merged commit dd818c1 into seL4:main Apr 24, 2026
1 check passed


		let mut boot_lvl2_lower: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];

		let pt_entry = (boot_lvl2_lower_addr \| 3).to_le_bytes();

Conversation

bruelc commented Apr 1, 2026

Uh oh!

midnightveil left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

bruelc Apr 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

midnightveil commented Apr 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Ivan-Velickovic commented Apr 24, 2026

Uh oh!

Uh oh!

Ivan-Velickovic commented Apr 24, 2026

Uh oh!

midnightveil commented Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

bruelc commented Apr 24, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

bruelc Apr 8, 2026 •

edited

Loading

midnightveil commented Apr 23, 2026 •

edited

Loading

midnightveil commented Apr 24, 2026 •

edited

Loading