Handoff untypeds to a PD after initialisation

Cargo.toml

@@ -12,12 +12,16 @@ members = [
 ]
 
 [workspace.dependencies.sel4-capdl-initializer]
-git = "https://github.com/seL4/rust-seL4"
-rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4"
+git = "https://github.com/au-ts/rust-seL4"
+branch = "szymon/handoff-untypeds"
+#git = "https://github.com/seL4/rust-seL4"
+#rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4"
 
 [workspace.dependencies.sel4-capdl-initializer-types]
-git = "https://github.com/seL4/rust-seL4"
-rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4"
+git = "https://github.com/au-ts/rust-seL4"
+branch = "szymon/handoff-untypeds"
+#git = "https://github.com/seL4/rust-seL4"
+#rev = "0ac1c27ee6cb9edac7a1a41a69b0d421e170d6a4"
 
 [profile.release.package.microkit-tool]
 strip = true

example/handoff_untypeds/Makefile

@@ -0,0 +1,72 @@
+#
+# Copyright 2026, UNSW
+# Copyright 2021, Breakaway Consulting Pty. Ltd.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+ifeq ($(strip $(BUILD_DIR)),)
+$(error BUILD_DIR must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_SDK)),)
+$(error MICROKIT_SDK must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_BOARD)),)
+$(error MICROKIT_BOARD must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_CONFIG)),)
+$(error MICROKIT_CONFIG must be specified)
+endif
+
+BOARD_DIR := $(MICROKIT_SDK)/board/$(MICROKIT_BOARD)/$(MICROKIT_CONFIG)
+
+ARCH := ${shell grep 'CONFIG_SEL4_ARCH  ' $(BOARD_DIR)/include/kernel/gen_config.h | cut -d' ' -f4}
+
+ifeq ($(ARCH),aarch64)
+  TARGET_TRIPLE := aarch64-none-elf
+  CFLAGS_ARCH := -mstrict-align
+else ifeq ($(ARCH),riscv64)
+  TARGET_TRIPLE := riscv64-unknown-elf
+  CFLAGS_ARCH := -march=rv64imafdc_zicsr_zifencei -mabi=lp64d
+else ifeq ($(ARCH),x86_64)
+	TARGET_TRIPLE := x86_64-elf
+	CFLAGS_ARCH := -march=x86-64 -mtune=generic
+else
+$(error Unsupported ARCH)
+endif
+
+ifeq ($(strip $(LLVM)),True)
+  CC := clang -target $(TARGET_TRIPLE)
+  AS := clang -target $(TARGET_TRIPLE)
+  LD := ld.lld
+else
+  CC := $(TARGET_TRIPLE)-gcc
+  LD := $(TARGET_TRIPLE)-ld
+  AS := $(TARGET_TRIPLE)-as
+endif
+
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
+
+HELLO_OBJS := hello.o
+
+IMAGES := hello.elf
+CFLAGS := -nostdlib -ffreestanding -g -O3 -Wall  -Wno-unused-function -Werror -I$(BOARD_DIR)/include $(CFLAGS_ARCH)
+LDFLAGS := -L$(BOARD_DIR)/lib
+LIBS := -lmicrokit -Tmicrokit.ld
+
+IMAGE_FILE = $(BUILD_DIR)/loader.img
+REPORT_FILE = $(BUILD_DIR)/report.txt
+SPEC = $(BUILD_DIR)/capdl_spec.json
+
+all: $(IMAGE_FILE)
+
+$(BUILD_DIR)/%.o: %.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/hello.elf: $(addprefix $(BUILD_DIR)/, $(HELLO_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) handoff_untypeds.system
+	$(MICROKIT_TOOL) handoff_untypeds.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) --capdl-json ${SPEC}

example/handoff_untypeds/README.md

@@ -0,0 +1,23 @@
+<!--
+     Copyright 2026, UNSW
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+# Example - Handoff untypeds
+
+This is a basic example that has a single protection domain
+that receives capabilities to all remaining untyped memory,
+prints information about the untypeds upon initialisation and
+has an example of using these untypeds for creating new kernel objects.
+
+All supported platforms are supported in this example.
+
+## Building
+
+```sh
+mkdir build
+make BUILD_DIR=build MICROKIT_BOARD=<board> MICROKIT_CONFIG=<debug/release/benchmark> MICROKIT_SDK=/path/to/sdk
+```
+
+## Running
+
+See instructions for your board in the manual.

example/handoff_untypeds/handoff_untypeds.system

@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <memory_region name="remaining_untypeds" size="0x2000" receive_all_untypeds="true"/>
+    <protection_domain name="hello">
+        <program_image path="hello.elf" />
+        <map mr="remaining_untypeds" vaddr="0x20_000_000" setvar_vaddr="remaining_untypeds_vaddr" />
+    </protection_domain>
+</system>

example/handoff_untypeds/hello.c

@@ -0,0 +1,68 @@
+/*
+ * Copyright 2026, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stdint.h>
+#include <microkit.h>
+//#include <types.h>
+#include <sel4/bootinfo_types.h>
+
+uintptr_t remaining_untypeds_vaddr;
+typedef struct {
+    seL4_CNode untyped_cnode_cptr;
+    seL4_SlotRegion untypeds;
+    seL4_UntypedDesc untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS];
+} capDLBootInfo_t;
+
+capDLBootInfo_t *capDLBootInfo; 
+
+void print_64(seL4_Word w) {
+    microkit_dbg_put32((seL4_Uint32) (w >> 32));
+    microkit_dbg_put32((seL4_Uint32) w);
+}
+void init(void)
+{
+    capDLBootInfo = (capDLBootInfo_t*) remaining_untypeds_vaddr;
+    microkit_dbg_puts("hello, world\nuntyped_cnode_cptr: ");
+    microkit_dbg_put32((seL4_Uint32) (capDLBootInfo->untyped_cnode_cptr >> 32));
+    microkit_dbg_putc(32);
+    microkit_dbg_put32((seL4_Uint32) capDLBootInfo->untyped_cnode_cptr);
+    microkit_dbg_puts("\nend\n");
+
+    microkit_dbg_puts("idx  paddr    sizeBits    isDevice\n");
+    for (uint32_t i = capDLBootInfo->untypeds.start; i < capDLBootInfo->untypeds.end; i++) {
+        microkit_dbg_put32(i);
+        microkit_dbg_puts("  ");
+        print_64(capDLBootInfo->untypedList[i].paddr);
+        microkit_dbg_puts("  ");
+        print_64(capDLBootInfo->untypedList[i].sizeBits);
+        microkit_dbg_puts("  ");
+        if(capDLBootInfo->untypedList[i].isDevice) {
+            microkit_dbg_puts("true\n");
+        } else {
+            microkit_dbg_puts("false\n");
+        }
+    }
+
+    // Try retype untyped idx 39
+    uint32_t untyped_idx = 40;
+    microkit_dbg_puts("Creating new untyped from Untyped Idx ");
+    microkit_dbg_put32(untyped_idx);
+    microkit_dbg_puts(" of size 4 at idx ");
+    microkit_dbg_put32(capDLBootInfo->untypeds.end);
+    seL4_Error err = seL4_Untyped_Retype(capDLBootInfo->untyped_cnode_cptr + untyped_idx, seL4_UntypedObject, 4, capDLBootInfo->untyped_cnode_cptr, 0, 0, capDLBootInfo->untypeds.end, 1);
+    // XXX: add Capability to the root CNode for Djawula (maybe?)
+    //seL4_Error err = seL4_Untyped_Retype(capDLBootInfo->untyped_cnode_cptr + 39, seL4_CNodeObject, 4, (uint64_t) 2 << (64-6), 0, 0, 68, 1);
+
+    microkit_dbg_puts("\nseL4_NoError: ");
+    microkit_dbg_put32(seL4_NoError);
+    microkit_dbg_puts("\n");
+    microkit_dbg_puts("err: ");
+    microkit_dbg_put32(err);
+    microkit_dbg_puts("\n");
+}
+
+void notified(microkit_channel ch)
+{
+}

tool/microkit/src/capdl/builder.rs

@@ -246,6 +246,7 @@ impl CapDLSpecContainer {
                     &format!("elf_{pd_name}_{frame_sequence:09}"),
                     None,
                     PageSize::Small.fixed_size_bits(sel4_config) as u8,
+                    false,
                 );
                 let frame_cap = capdl_util_make_frame_cap(
                     frame_obj_id,
@@ -286,6 +287,7 @@ impl CapDLSpecContainer {
             &format!("ipcbuf_{pd_name}"),
             None,
             PageSize::Small.fixed_size_bits(sel4_config) as u8,
+            false,
         );
         let ipcbuf_frame_cap =
             capdl_util_make_frame_cap(ipcbuf_frame_obj_id, true, true, false, true);
@@ -439,6 +441,7 @@ pub fn build_capdl_spec(
             capdl_util_make_cte(MON_REPLY_CAP_IDX as u32, mon_reply_cap),
         ]
         .to_vec(),
+        false,
     );
     let mon_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64;
     let mon_cnode_cap = capdl_util_make_cnode_cap(mon_cnode_obj_id, 0, mon_guard_size as u8);
@@ -452,6 +455,7 @@ pub fn build_capdl_spec(
         &format!("{MONITOR_PD_NAME}_stack"),
         None,
         PageSize::Small.fixed_size_bits(kernel_config) as u8,
+        false,
     );
     let mon_stack_frame_cap =
         capdl_util_make_frame_cap(mon_stack_frame_obj_id, true, true, false, true);
@@ -506,6 +510,8 @@ pub fn build_capdl_spec(
         let mut frame_ids = Vec::new();
         let frame_size_bits = mr.page_size.fixed_size_bits(kernel_config);
 
+        // If this MR is supposed to receive untyped metadata, mark the first frame in the spec
+        let mut receive_all_untypeds = mr.receive_all_untypeds;
         for frame_sequence in 0..mr.page_count {
             let paddr = mr
                 .paddr()
@@ -518,7 +524,10 @@ pub fn build_capdl_spec(
                 &format!("mr_{}_{:09}", mr.name, frame_sequence),
                 paddr,
                 frame_size_bits as u8,
+                receive_all_untypeds,
             ));
+            // Only mark the first frame in the Memory Region
+            receive_all_untypeds = false;
         }
 
         mr_name_to_frames.insert(&mr.name, frame_ids);
@@ -629,6 +638,7 @@ pub fn build_capdl_spec(
                 &format!("{}_stack_{:09}", pd.name, stack_frame_seq),
                 None,
                 PageSize::Small.fixed_size_bits(kernel_config) as u8,
+                false,
             );
             let stack_frame_cap =
                 capdl_util_make_frame_cap(stack_frame_obj_id, true, true, false, true);
@@ -839,6 +849,7 @@ pub fn build_capdl_spec(
                         &format!("{}_{}", virtual_machine.name, vcpu.id),
                         PD_CAP_BITS,
                         [].to_vec(),
+                        false,
                     );
                     let vm_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64;
                     let vm_cnode_cap =
@@ -858,6 +869,7 @@ pub fn build_capdl_spec(
                         None,
                         // Must be consistent with the granule bits used in spec serialisation
                         PageSize::Small.fixed_size_bits(kernel_config) as u8,
+                        false,
                     );
                     let vm_ipcbuf_frame_cap =
                         capdl_util_make_frame_cap(vm_ipcbuf_frame_obj_id, true, true, false, true);
@@ -955,19 +967,88 @@ pub fn build_capdl_spec(
         }
 
         // Step 3-13 Create CSpace and add all caps that the PD code and libmicrokit need to access.
-        let pd_cnode_obj_id = capdl_util_make_cnode_obj(
-            &mut spec_container,
-            &pd.name,
-            PD_CAP_BITS,
-            caps_to_insert_to_pd_cspace,
-        );
-        let pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64;
-        let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8);
-        caps_to_bind_to_tcb.push(capdl_util_make_cte(
-            TcbBoundSlot::CSpace as u32,
-            pd_cnode_cap,
-        ));
-        pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id);
+        // If this pd is supposed to receive all remaining untypeds, do what
+        // https://github.com/Neutrality-ch/microkit/commit/34d4b8d2e246dd77bcd538027277e37a5ba97764
+        // proposed: create a new root CNode, and insert the Microkit CNode at index 0, (this means
+        // old CPtr's will still point to valid capabilities in the Microkit CNode), and create a
+        // placeholder CNode at index 1 of the new root CNode which will be receiving the untypeds.
+        // Mark the receiving CNode.
+        if pd.receive_all_untypeds {
+            let root_cnode_size_bits = 6; // XXX: for now 64 slots (2^{64})
+            let receiving_untyped_cnode_size_bits = 8; // TODO:
+                                                            // log2(MAX_NUM_BOOTINFO_UNTYPED_CAPS)?,
+                                                            // some other precalculated value?
+            // Populate the below with pd_cnode_cap and pd_receiving_untyped_cnode_cap or use
+            // capdl_util_insert_cap_into_cspace instead? (whats the benefit of the first
+            // approach?)
+            //let mut caps_to_insert_to_pd_root_cspace: Vec<CapTableEntry> = Vec::new();
+            // TODO: slots: for pd_root_cnode_obj will need to contain the original Microkit CNode
+            // and the to-be-populated untyped receiving CNode
+            let pd_cnode_obj_id = capdl_util_make_cnode_obj(
+                &mut spec_container,
+                &pd.name,
+                PD_CAP_BITS,
+                caps_to_insert_to_pd_cspace,
+                false,
+            );
+            let mut pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64 - root_cnode_size_bits as u64;
+            println!("pd cnode guard size: {}", pd_guard_size);
+            let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8);
+
+            let pd_receiving_untyped_cnode_obj_id = capdl_util_make_cnode_obj(
+                &mut spec_container,
+                &(pd.name.clone() + "_receiving_untypeds"),
+                receiving_untyped_cnode_size_bits,
+                Vec::new(),
+                true,
+            );
+            // OLD: pd_guard_size = kernel_config.cap_address_bits - receiving_untyped_cnode_size_bits as u64 - root_cnode_size_bits as u64;
+            pd_guard_size = kernel_config.cap_address_bits - receiving_untyped_cnode_size_bits as u64 - root_cnode_size_bits as u64;
+            // XXX: for the cap, do guard size up to the size_bits, so when addressing from the
+            // receiving_untypeds_cnode_cap, one can use max depth
+            println!("receivning untyped guard size: {}", pd_guard_size);
+            let pd_receiving_untyped_cnode_cap = capdl_util_make_cnode_cap(pd_receiving_untyped_cnode_obj_id, 0, pd_guard_size as u8);
+            let pd_receiving_untyped_cnode_cap_self_ref = capdl_util_make_cnode_cap(pd_receiving_untyped_cnode_obj_id, 0, pd_guard_size as u8);
+            capdl_util_insert_cap_into_cspace(&mut spec_container, pd_receiving_untyped_cnode_obj_id, 0, pd_receiving_untyped_cnode_cap_self_ref);
+
+            let pd_root_cnode_obj_id = capdl_util_make_cnode_obj(
+                &mut spec_container,
+                &(pd.name.clone() + "_root"),
+                root_cnode_size_bits,
+                Vec::new(),
+                false,
+            );
+            pd_guard_size = 0; // so the old Microkit CNode indexes work as expected, but other
+                               // CNode's (such as receiving untyped one) can be addressed at the
+                               // root_cnode_size_bits most significant bits of the address.
+            println!("root cnode guard size: {}", pd_guard_size);
+            let pd_root_cnode_cap = capdl_util_make_cnode_cap(pd_root_cnode_obj_id, 0, pd_guard_size as u8);
+            capdl_util_insert_cap_into_cspace(&mut spec_container, pd_root_cnode_obj_id, 0, pd_cnode_cap);
+            capdl_util_insert_cap_into_cspace(&mut spec_container, pd_root_cnode_obj_id, 1, pd_receiving_untyped_cnode_cap);
+
+            caps_to_bind_to_tcb.push(capdl_util_make_cte(
+                TcbBoundSlot::CSpace as u32,
+                pd_root_cnode_cap,
+            ));
+            // XXX: change this to root? or is this fine
+            pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id);
+        } else {
+            let pd_cnode_obj_id = capdl_util_make_cnode_obj(
+                &mut spec_container,
+                &pd.name,
+                PD_CAP_BITS,
+                caps_to_insert_to_pd_cspace,
+                pd.receive_all_untypeds,
+            );
+            let pd_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64;
+            let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8);
+            caps_to_bind_to_tcb.push(capdl_util_make_cte(
+                TcbBoundSlot::CSpace as u32,
+                pd_cnode_cap,
+            ));
+            pd_id_to_cspace_id.insert(pd_global_idx, pd_cnode_obj_id);
+        }
+
 
         // Step 3-14 Set the TCB parameters and all the various caps that we need to bind to this TCB.
         if let Object::Tcb(pd_tcb) = &mut spec_container