Enable mapping extra TCB and SC caps into PD's

libmicrokit/include/microkit.h

@@ -28,7 +28,9 @@ typedef seL4_MessageInfo_t microkit_msginfo;
 #define BASE_VM_TCB_CAP 266
 #define BASE_VCPU_CAP 330
 #define BASE_IOPORT_CAP 394
+#define BASE_USER_CAPS 458
 
+#define MICROKIT_MAX_USER_CAPS 128
 #define MICROKIT_MAX_CHANNELS 62
 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1)
 #define MICROKIT_MAX_IOPORT_ID MICROKIT_MAX_CHANNELS

tool/microkit/src/capdl/builder.rs

@@ -11,8 +11,8 @@ use std::{
 };
 
 use sel4_capdl_initializer_types::{
-    object, CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId, Spec,
-    Word,
+    object, Cap, CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId,
+    Spec, Word,
 };
 
 use crate::{
@@ -24,8 +24,8 @@ use crate::{
     },
     elf::ElfFile,
     sdf::{
-        CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME,
-        MONITOR_PRIORITY,
+        CapMapType, CpuCore, SysMap, SysMapPerms, SystemDescription, BUDGET_DEFAULT,
+        MONITOR_PD_NAME, MONITOR_PRIORITY,
     },
     sel4::{Arch, Config, PageSize},
     util::{ranges_overlap, round_down, round_up},
@@ -95,8 +95,14 @@ 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;
-
-pub const PD_CAP_SIZE: u32 = 512;
+// 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;
 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;
@@ -573,11 +579,17 @@ pub fn build_capdl_spec(
         None
     };
 
+    // Mapping between pd name and id for faster lookups
+    let mut pd_name_to_id: HashMap<&String, usize> = HashMap::new();
+
     // Keep tabs on each PD's CSpace, Notification and Endpoint objects so we can create channels between them at a later step.
     let mut pd_id_to_cspace_id: HashMap<usize, ObjectId> = HashMap::new();
     let mut pd_id_to_ntfn_id: HashMap<usize, ObjectId> = HashMap::new();
     let mut pd_id_to_ep_id: HashMap<usize, ObjectId> = HashMap::new();
 
+    // Keep tabs on caps such as TCB and SC so that we can create additional mappings for the cap into other PD's cspaces.
+    let mut pd_shadow_cspace: HashMap<usize, HashMap<CapMapType, Cap>> = HashMap::new();
+
     // Keep track of the global count of vCPU objects so we can bind them to the monitor for setting TCB name in debug config.
     // Only used on ARM and RISC-V as on x86-64 VMs share the same TCB as PD's which will have their TCB name set separately.
     let mut monitor_vcpu_idx = 0;
@@ -588,6 +600,9 @@ pub fn build_capdl_spec(
     for (pd_global_idx, pd) in system.protection_domains.iter().enumerate() {
         let elf_obj = &elfs[pd_global_idx];
 
+        pd_name_to_id.insert(&pd.name, pd_global_idx);
+
+        let mut pd_shadow_cspace_inner: HashMap<CapMapType, Cap> = HashMap::new();
         let mut caps_to_bind_to_tcb: Vec<CapTableEntry> = Vec::new();
         let mut caps_to_insert_to_pd_cspace: Vec<CapTableEntry> = Vec::new();
 
@@ -597,20 +612,22 @@ pub fn build_capdl_spec(
             .unwrap();
         let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id);
 
+        let pd_tcb_obj = capdl_util_make_tcb_cap(pd_tcb_obj_id);
+        let pd_vspace_obj = capdl_util_make_page_table_cap(pd_vspace_obj_id);
+
+        pd_shadow_cspace_inner.insert(CapMapType::Tcb, pd_tcb_obj.clone());
+        pd_shadow_cspace_inner.insert(CapMapType::VSpace, pd_vspace_obj.clone());
+
         // In the benchmark configuration, we allow PDs to access their own TCB.
         // This is necessary for accessing kernel's benchmark API.
         if kernel_config.benchmark {
-            caps_to_insert_to_pd_cspace.push(capdl_util_make_cte(
-                PD_TCB_CAP_IDX as u32,
-                capdl_util_make_tcb_cap(pd_tcb_obj_id),
-            ));
+            caps_to_insert_to_pd_cspace
+                .push(capdl_util_make_cte(PD_TCB_CAP_IDX as u32, pd_tcb_obj));
         }
 
         // Allow PD to access their own VSpace for ops such as cache cleaning on ARM.
-        caps_to_insert_to_pd_cspace.push(capdl_util_make_cte(
-            PD_VSPACE_CAP_IDX as u32,
-            capdl_util_make_page_table_cap(pd_vspace_obj_id),
-        ));
+        caps_to_insert_to_pd_cspace
+            .push(capdl_util_make_cte(PD_VSPACE_CAP_IDX as u32, pd_vspace_obj));
 
         // Step 3-2: Map in all Memory Regions
         for map in pd.maps.iter() {
@@ -688,6 +705,9 @@ pub fn build_capdl_spec(
             0x100 + pd_global_idx as u64,
         );
         let pd_sc_cap = capdl_util_make_sc_cap(pd_sc_obj_id);
+
+        pd_shadow_cspace_inner.insert(CapMapType::Sc, pd_sc_cap.clone());
+
         caps_to_bind_to_tcb.push(capdl_util_make_cte(
             TcbBoundSlot::SchedContext as u32,
             pd_sc_cap,
@@ -1001,6 +1021,7 @@ pub fn build_capdl_spec(
         );
         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);
+        pd_shadow_cspace_inner.insert(CapMapType::CSpace, pd_cnode_cap.clone());
         caps_to_bind_to_tcb.push(capdl_util_make_cte(
             TcbBoundSlot::CSpace as u32,
             pd_cnode_cap,
@@ -1052,6 +1073,7 @@ pub fn build_capdl_spec(
                 capdl_util_make_ntfn_cap(pd_ntfn_obj_id, true, true, 0),
             );
         }
+        pd_shadow_cspace.insert(pd_global_idx, pd_shadow_cspace_inner);
     }
 
     // *********************************
@@ -1118,7 +1140,35 @@ pub fn build_capdl_spec(
     }
 
     // *********************************
-    // Step 5. Sort the root objects
+    // Step 5. Handle extra cap mappings
+    // *********************************
+
+    for (pd_dest_idx, pd) in system.protection_domains.iter().enumerate() {
+        let pd_dest_cspace_id = pd_id_to_cspace_id[&pd_dest_idx];
+        for cap_map in pd.cap_maps.iter() {
+            let pd_src_idx = pd_name_to_id.get(&cap_map.pd_name).ok_or(format!(
+                "PD: '{}', does not exist when trying to map extra TCB cap into PD: '{}'",
+                cap_map.pd_name, pd.name
+            ))?;
+
+            let pd_shadow_cspace_inner = pd_shadow_cspace.get(pd_src_idx).unwrap();
+
+            let pd_obj = pd_shadow_cspace_inner
+                .get(&cap_map.cap_type)
+                .unwrap()
+                .clone();
+            // 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.dest_cspace_slot) as u32,
+                pd_obj,
+            );
+        }
+    }
+
+    // *********************************
+    // Step 6. Sort the root objects
     // *********************************
     // The CapDL initialiser expects objects with paddr to come first, then sorted by size so that the
     // allocation algorithm at run-time can run more efficiently.

tool/microkit/src/sdf.rs

@@ -21,7 +21,7 @@ use crate::sel4::{
 };
 use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool};
 use crate::MAX_PDS;
-use std::collections::HashSet;
+use std::collections::{HashMap, HashSet};
 use std::fmt::Display;
 use std::fs;
 use std::path::{Path, PathBuf};
@@ -38,6 +38,10 @@ use std::path::{Path, PathBuf};
 const PD_MAX_ID: u64 = 61;
 const VCPU_MAX_ID: u64 = PD_MAX_ID;
 
+/// This is the maximum slot allowed for cap maps. This can change if you wish,
+/// but also update the MICROKIT_MAX_USER_CAPS define in `microkit.h`.
+const CAP_MAP_MAX_SLOT: u64 = 128;
+
 pub const MONITOR_PRIORITY: u8 = 255;
 const PD_MAX_PRIORITY: u8 = 254;
 /// In microseconds
@@ -277,6 +281,7 @@ pub struct ProtectionDomain {
     pub irqs: Vec<SysIrq>,
     pub ioports: Vec<IOPort>,
     pub setvars: Vec<SysSetVar>,
+    pub cap_maps: Vec<CapMap>,
     pub virtual_machine: Option<VirtualMachine>,
     /// Only used when parsing child PDs. All elements will be removed
     /// once we flatten each PD and its children into one list.
@@ -291,6 +296,23 @@ pub struct ProtectionDomain {
     text_pos: Option<roxmltree::TextPos>,
 }
 
+#[derive(Debug, PartialEq, Eq, Copy, Clone, Hash)]
+pub enum CapMapType {
+    Tcb,
+    Sc,
+    VSpace,
+    CSpace,
+}
+
+#[derive(Debug, PartialEq, Eq)]
+pub struct CapMap {
+    pub cap_type: CapMapType,
+    pub pd_name: String,
+    pub dest_cspace_slot: u64,
+    /// Location in the parsed SDF file
+    text_pos: roxmltree::TextPos,
+}
+
 #[derive(Debug, PartialEq, Eq)]
 pub struct VirtualMachine {
     pub vcpus: Vec<VirtualCpu>,
@@ -606,6 +628,7 @@ impl ProtectionDomain {
         let mut ioports = Vec::new();
         let mut setvars: Vec<SysSetVar> = Vec::new();
         let mut child_pds = Vec::new();
+        let mut cap_maps = Vec::new();
 
         let mut program_image = None;
         let mut program_image_for_symbols = None;
@@ -1128,6 +1151,9 @@ impl ProtectionDomain {
 
                     virtual_machine = Some(vm);
                 }
+                "cap" => {
+                    cap_maps.push(CapMap::from_xml(xml_sdf, &child)?);
+                }
                 _ => {
                     let pos = xml_sdf.doc.text_pos_at(child.range().start);
                     return Err(format!(
@@ -1166,6 +1192,7 @@ impl ProtectionDomain {
             irqs,
             ioports,
             setvars,
+            cap_maps,
             child_pds,
             virtual_machine,
             has_children,
@@ -1306,6 +1333,47 @@ impl VirtualMachine {
     }
 }
 
+impl CapMap {
+    fn from_xml(xml_sdf: &XmlSystemDescription, node: &roxmltree::Node) -> Result<CapMap, String> {
+        check_attributes(xml_sdf, node, &["type", "pd", "dest_cspace_slot"])?;
+        let text_pos = xml_sdf.doc.text_pos_at(node.range().start);
+
+        let xml_cap_type = checked_lookup(xml_sdf, node, "type")?;
+        let cap_type = match xml_cap_type {
+            "tcb" => CapMapType::Tcb,
+            "sc" => CapMapType::Sc,
+            "vspace" => CapMapType::VSpace,
+            "cspace" => CapMapType::CSpace,
+            _ => {
+                return Err(format!(
+                    "Cap type: '{xml_cap_type}' is not supported at '{}'",
+                    loc_string(&xml_sdf, text_pos)
+                ))
+            }
+        };
+
+        let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string();
+        let dest_cspace_slot =
+            sdf_parse_number(checked_lookup(xml_sdf, node, "dest_cspace_slot")?, node)?;
+
+        if dest_cspace_slot >= CAP_MAP_MAX_SLOT {
+            return Err(value_error(
+                xml_sdf,
+                node,
+                format!("There are only {CAP_MAP_MAX_SLOT} destination cspace slots available.")
+                    .to_string(),
+            ));
+        }
+
+        Ok(CapMap {
+            cap_type,
+            pd_name,
+            dest_cspace_slot,
+            text_pos,
+        })
+    }
+}
+
 impl SysMemoryRegion {
     fn determine_size(
         xml_sdf: &XmlSystemDescription,
@@ -1815,7 +1883,6 @@ pub fn parse(
     let mut root_pds = vec![];
     let mut mrs = vec![];
     let mut channels = vec![];
-
     let system = doc
         .root()
         .children()
@@ -2080,6 +2147,37 @@ pub fn parse(
         }
     }
 
+    // Ensure that there are no overlapping extra cap maps in the user caps region
+    // and we are not mapping in the same cap from the same source more than once
+    for pd in &pds {
+        let mut user_cap_slots = HashMap::<u64, Vec<_>>::new();
+
+        for cap_map in &pd.cap_maps {
+            user_cap_slots
+                .entry(cap_map.dest_cspace_slot)
+                .and_modify(|v| v.push(cap_map))
+                .or_insert(vec![cap_map]);
+        }
+
+        for (slot, cap_maps) in user_cap_slots.iter() {
+            if cap_maps.len() > 1 {
+                let mut lines = String::new();
+                for mapping in cap_maps {
+                    lines.push_str(&format!(
+                        "\n  type {:?} from '{}' at '{}'",
+                        mapping.cap_type,
+                        mapping.pd_name,
+                        loc_string(&xml_sdf, mapping.text_pos)
+                    ));
+                }
+                return Err(format!(
+                    "Error: overlapping user caps in slot {slot} of protection domain '{}':{}",
+                    pd.name, lines
+                ));
+            }
+        }
+    }
+
     // Ensure MRs with physical addresses do not overlap
     let mut checked_mrs = Vec::with_capacity(mrs.len());
     for mr in &mrs {

tool/microkit/tests/sdf/pd_cap_mappings_invalid.system

@@ -0,0 +1,17 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="pd_a">
+        <program_image path="test" />
+    </protection_domain>
+
+    <protection_domain name="pd_b">
+        <program_image path="test" />
+
+        <cap type="gerbils" pd="pd_a" dest_cspace_slot="4" />
+    </protection_domain>
+</system>

tool/microkit/tests/sdf/pd_cap_mappings_overlapping.system

@@ -0,0 +1,25 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="pd_a">
+        <program_image path="test" />
+
+        <!-- not a duplicate slot -->
+        <cap type="tcb"    pd="pd_a" dest_cspace_slot="1" />
+    </protection_domain>
+
+    <protection_domain name="pd_b">
+        <program_image path="test" />
+
+        <cap type="tcb"    pd="pd_a" dest_cspace_slot="1" />
+        <cap type="sc"     pd="pd_a" dest_cspace_slot="2" />
+        <cap type="vspace" pd="pd_a" dest_cspace_slot="3" />
+        <cap type="cspace" pd="pd_a" dest_cspace_slot="4" />
+        <!-- duplicate slot -->
+        <cap type="cspace" pd="pd_a" dest_cspace_slot="4" />
+    </protection_domain>
+</system>