From 728352c78ccd69fd7b48ca2d82e1173972816b90 Mon Sep 17 00:00:00 2001 From: Terry Bai Date: Fri, 26 Jun 2026 14:52:54 +1000 Subject: [PATCH 1/3] Make two-level CNodes for PD's CSpace This adds a smaller CNode as PD's cspace and moves the original Microkit resource CNode to the root's first slot, as this makes the CSpace management more flexible. The changes are: - size of root CNode: 64 - size of Microkit CNode: 1024 -> 512 - guard size of root CNode: 0 - guard size of Microkit CNode: seL4_WordBits - 6 - 9 This also fixes the capability creation for shared VSpace and CSpace. Signed-off-by: Terry Bai --- libmicrokit/include/microkit.h | 8 +++- tool/microkit/src/capdl/builder.rs | 67 +++++++++++++++++++++++------- 2 files changed, 57 insertions(+), 18 deletions(-) diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 1b59319d2..79b612452 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -33,6 +33,10 @@ typedef seL4_MessageInfo_t microkit_msginfo; #define BASE_IOPORT_CAP 394 #define BASE_USER_CAPS 458 +/* This should be kept in sync with `PD_ROOT_CAP_BITS` in capdl/builder.rs */ +#define PD_ROOT_CAP_BITS 6 +#define PD_ROOT_CAP_SIZE (1ULL << PD_ROOT_CAP_BITS) + #define MICROKIT_MAX_USER_CAPS 128 #define MICROKIT_MAX_CHANNELS 62 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1) @@ -594,9 +598,9 @@ static inline void microkit_deferred_irq_ack(microkit_channel ch) **/ static inline seL4_CPtr microkit_cspace_root_slot_to_cptr(seL4_Word slot) { - if (slot > MICROKIT_MAX_USER_CAPS) { + if (slot == 0 || slot >= PD_ROOT_CAP_SIZE) { return seL4_CapNull; } - return BASE_USER_CAPS + slot; + return slot << (seL4_WordBits - PD_ROOT_CAP_BITS); } diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 5bb401be0..533b2d248 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -95,14 +95,11 @@ const PD_BASE_PD_TCB_CAP: u64 = PD_BASE_IRQ_CAP + 64; const PD_BASE_VM_TCB_CAP: u64 = PD_BASE_PD_TCB_CAP + 64; const PD_BASE_VCPU_CAP: u64 = PD_BASE_VM_TCB_CAP + 64; const PD_BASE_IOPORT_CAP: u64 = PD_BASE_VCPU_CAP + 64; -// The following region can be used for whatever the user wants to map into their -// cspace. We restrict them to use this region so that they don't accidently -// overwrite other parts of the cspace. The cspace slot that the users provide -// for mapping in extra caps such as TCBs and SCs will be as an offset to this -// index. We are bounding this to 128 slots for now. -const PD_BASE_USER_CAPS: u64 = PD_BASE_IOPORT_CAP + 64; - -pub const PD_CAP_SIZE: u32 = 1024; + +/* This should be kept in sync with `PD_ROOT_CAP_BITS` in libmicrokit/include/microkit.h */ +const PD_ROOT_CAP_SIZE: u32 = 64; +const PD_ROOT_CAP_BITS: u8 = PD_ROOT_CAP_SIZE.ilog2() as u8; +pub const PD_CAP_SIZE: u32 = 512; const PD_CAP_BITS: u8 = PD_CAP_SIZE.ilog2() as u8; const PD_SCHEDCONTEXT_EXTRA_SIZE: u64 = 256; const PD_SCHEDCONTEXT_EXTRA_SIZE_BITS: u64 = PD_SCHEDCONTEXT_EXTRA_SIZE.ilog2() as u64; @@ -120,6 +117,7 @@ pub struct ExpectedAllocation { struct PDShadowCspace { cspace: ObjectId, + microkit_cnode: ObjectId, notification: ObjectId, endpoint: Option, sched_context: ObjectId, @@ -1014,11 +1012,29 @@ pub fn build_capdl_spec( 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_guard_size = + kernel_config.cap_address_bits - PD_CAP_BITS as u64 - PD_ROOT_CAP_BITS as u64; let pd_cnode_cap = capdl_util_make_cnode_cap(pd_cnode_obj_id, 0, pd_guard_size as u8); + + let pd_root_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + &(pd.name.clone() + "_root"), + PD_ROOT_CAP_BITS, + Vec::new(), + ); + // leave the guard size root cnode as 0 + let pd_root_cnode_cap = capdl_util_make_cnode_cap(pd_root_cnode_obj_id, 0, 0); + // place microkit managed cnode at slot 0 + capdl_util_insert_cap_into_cspace( + &mut spec_container, + pd_root_cnode_obj_id, + 0, + pd_cnode_cap, + ); + caps_to_bind_to_tcb.push(capdl_util_make_cte( TcbBoundSlot::CSpace as u32, - pd_cnode_cap, + pd_root_cnode_cap, )); // Step 3-14 Set the TCB parameters and all the various caps that we need to bind to this TCB. @@ -1070,7 +1086,8 @@ pub fn build_capdl_spec( pd_shadow_cspaces.insert( pd_global_idx, PDShadowCspace { - cspace: pd_cnode_obj_id, + cspace: pd_root_cnode_obj_id, + microkit_cnode: pd_cnode_obj_id, endpoint: pd_ep_obj_id, notification: pd_ntfn_obj_id, sched_context: pd_sc_obj_id, @@ -1084,8 +1101,8 @@ pub fn build_capdl_spec( // Step 4. Create channels // ********************************* for channel in system.channels.iter() { - let pd_a_cspace_id = pd_shadow_cspaces[&channel.end_a.pd].cspace; - let pd_b_cspace_id = pd_shadow_cspaces[&channel.end_b.pd].cspace; + let pd_a_cspace_id = pd_shadow_cspaces[&channel.end_a.pd].microkit_cnode; + let pd_b_cspace_id = pd_shadow_cspaces[&channel.end_b.pd].microkit_cnode; let pd_a_ntfn_id = pd_shadow_cspaces[&channel.end_a.pd].notification; let pd_b_ntfn_id = pd_shadow_cspaces[&channel.end_b.pd].notification; @@ -1162,15 +1179,33 @@ pub fn build_capdl_spec( let cap_map_obj = match cap_map.cap_type { CapMapType::Tcb => capdl_util_make_tcb_cap(pd_src_shadow_cspace.tcb), CapMapType::Sc => capdl_util_make_sc_cap(pd_src_shadow_cspace.sched_context), - CapMapType::VSpace => capdl_util_make_sc_cap(pd_src_shadow_cspace.vspace), - CapMapType::CSpace => capdl_util_make_sc_cap(pd_src_shadow_cspace.cspace), + CapMapType::VSpace => capdl_util_make_page_table_cap(pd_src_shadow_cspace.vspace), + CapMapType::CSpace => { + let Some(named_object) = + spec_container.get_root_object(pd_src_shadow_cspace.cspace) + else { + unreachable!("internal bug: couldn't find cnode with given obj id."); + }; + let Object::CNode(ref cnode) = named_object.object else { + unreachable!( + "internal bug: got a non-CNode object id {} with name '{}'", + usize::from(pd_src_shadow_cspace.cspace), + named_object.name.as_ref().unwrap() + ); + }; + + let guard_size = + kernel_config.cap_address_bits as u8 - PD_ROOT_CAP_BITS - cnode.size_bits; + + capdl_util_make_cnode_cap(pd_src_shadow_cspace.cspace, 0, guard_size) + } }; // Map this into the destination pd's cspace and the specified slot. capdl_util_insert_cap_into_cspace( &mut spec_container, pd_dest_cspace_id, - (PD_BASE_USER_CAPS + cap_map.slot) as u32, + cap_map.slot as u32, cap_map_obj, ); } From a585bd43ddda767d3cdd8da0b0250243e1efc2fb Mon Sep 17 00:00:00 2001 From: Terry Bai Date: Fri, 26 Jun 2026 15:03:52 +1000 Subject: [PATCH 2/3] example: add rules for QEMU tests in Makefile This adds rules for QEMU tests on x86 and enables the 'capdl_spec.json' file generation for analysis. Signed-off-by: Terry Bai --- example/cap_sharing/Makefile | 35 +++++++++++++++++++++++++++++++++-- 1 file changed, 33 insertions(+), 2 deletions(-) diff --git a/example/cap_sharing/Makefile b/example/cap_sharing/Makefile index 567863e8e..0901a34c9 100644 --- a/example/cap_sharing/Makefile +++ b/example/cap_sharing/Makefile @@ -55,6 +55,8 @@ LIBS := -lmicrokit -Tmicrokit.ld IMAGE_FILE = $(BUILD_DIR)/loader.img REPORT_FILE = $(BUILD_DIR)/report.txt +SPEC = $(BUILD_DIR)/capdl_spec.json +KERNEL_32B = $(BUILD_DIR)/sel4_32.elf all: $(IMAGE_FILE) @@ -67,5 +69,34 @@ $(BUILD_DIR)/%.o: %.c Makefile | $(BUILD_DIR) $(BUILD_DIR)/%.elf: $(BUILD_DIR)/%.o $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ -$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) cap_sharing.system - $(MICROKIT_TOOL) cap_sharing.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) +$(IMAGE_FILE) $(KERNEL_32B) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) cap_sharing.system + $(MICROKIT_TOOL) cap_sharing.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) --capdl-json $(SPEC) + +ifeq ($(ARCH),x86_64) +qemu: $(KERNEL_32B) $(IMAGE_FILE) + qemu-system-x86_64 \ + -cpu qemu64,+fsgsbase,+pdpe1gb,+xsaveopt,+xsave \ + -m "1G" \ + -display none \ + -serial mon:stdio \ + -kernel $(KERNEL_32B) \ + -initrd $(IMAGE_FILE) +else ifeq ($(ARCH),aarch64) +qemu: $(IMAGE_FILE) + qemu-system-aarch64 \ + -machine virt,virtualization=on -cpu cortex-a53 \ + -nographic \ + -m size=2G \ + -serial mon:stdio \ + -device loader,file=$(IMAGE_FILE),addr=0x70000000,cpu-num=0 +else ifeq ($(ARCH),riscv64) +qemu: $(IMAGE_FILE) + qemu-system-riscv64 \ + -machine virt \ + -kernel $(IMAGE_FILE) \ + -nographic \ + -m size=2G \ + -serial mon:stdio +else +$(error Unsupported ARCH) +endif From 48e4486d317cc7576ab107c9d4f5efd3f0306b32 Mon Sep 17 00:00:00 2001 From: Terry Bai Date: Fri, 26 Jun 2026 16:36:38 +1000 Subject: [PATCH 3/3] tool: check slot of extra caps This checks if people try to place extra caps in slot 0, which is reserved for Microkit CNode, and adds a test case for it. Signed-off-by: Terry Bai --- tool/microkit/src/sdf.rs | 8 ++++++++ .../sdf/cap_mappings_slot_invalid.system | 19 +++++++++++++++++++ tool/microkit/tests/test.rs | 9 +++++++++ 3 files changed, 36 insertions(+) create mode 100644 tool/microkit/tests/sdf/cap_mappings_slot_invalid.system diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 55f40bf8e..da0da5c71 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -1372,6 +1372,14 @@ impl CapMap { let slot = sdf_parse_number(checked_lookup(xml_sdf, node, "slot")?, node)?; + if slot == 0 { + return Err(value_error( + xml_sdf, + node, + ("The destination slot 0 has been reserved for Microkit CNode").to_string(), + )); + } + // TODO: Rework this so that we don't have a fixed upper limit. if slot >= CAP_MAP_MAX_SLOT { return Err(value_error( diff --git a/tool/microkit/tests/sdf/cap_mappings_slot_invalid.system b/tool/microkit/tests/sdf/cap_mappings_slot_invalid.system new file mode 100644 index 000000000..60cae4116 --- /dev/null +++ b/tool/microkit/tests/sdf/cap_mappings_slot_invalid.system @@ -0,0 +1,19 @@ + + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 1c5046ebb..d3340e69c 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -1040,6 +1040,15 @@ mod system { ) } + #[test] + fn test_cap_mappings_slot_invalid() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "cap_mappings_slot_invalid.system", + "Error: The destination slot 0 has been reserved for Microkit CNode on element 'cap_sc'", + ) + } + #[test] fn test_cap_mappings_invalid() { check_error(