From 91768eab856c10376e5ac540f11010d33e647d50 Mon Sep 17 00:00:00 2001 From: Guangtao Zhu Date: Wed, 5 Aug 2026 16:52:52 +1000 Subject: [PATCH 1/8] sdf: introduce 'delegatee' PD and 'delegated' elements Microkit abstractions such as memory regions, IRQs, and IOports can be dynamic by delegating the ability to modify themselves to a PD other than the PDs who use the abstractions. Such a PD is called a 'delegatee' PD, while the dynamic resources are called 'delegated' resources, which are backed up by 'delegated' capabilities. A 'delegatee' PD is a PD that receives all 'delegated' caps of its child PDs or template PDs, which also means a PD without parent is not allowed to delegate the ability to control its resources to others. Signed-off-by: Guangtao Zhu --- example/cap_delegate/Makefile | 111 +++++ example/cap_delegate/README.md | 431 ++++++++++++++++++ example/cap_delegate/cap_delegate.system | 32 ++ example/cap_delegate/delegatee.c | 120 +++++ example/cap_delegate/delegation.h | 38 ++ example/cap_delegate/delegator.c | 219 +++++++++ example/cap_delegate/server.c | 19 + tool/microkit/src/capdl/builder.rs | 264 +++++++++-- tool/microkit/src/capdl/memory.rs | 24 +- tool/microkit/src/sdf.rs | 1 + tool/microkit/src/sdf/channels.rs | 32 +- tool/microkit/src/sdf/consts.rs | 5 +- tool/microkit/src/sdf/cspace.rs | 20 +- tool/microkit/src/sdf/irq.rs | 1 + tool/microkit/src/sdf/memory_region.rs | 30 ++ tool/microkit/src/sdf/pd_vm.rs | 121 ++++- tool/microkit/src/sdf/util.rs | 16 + .../sdf/pd_delegate_child_as_delegatee.system | 16 + .../sdf/pd_delegate_invalid_channel.system | 24 + .../sdf/pd_delegate_invalid_ioport.system | 16 + .../tests/sdf/pd_delegate_invalid_irq.system | 16 + .../tests/sdf/pd_delegate_invalid_map.system | 18 + .../sdf/pd_delegate_without_delegatee.system | 14 + tool/microkit/tests/test.rs | 54 +++ 24 files changed, 1592 insertions(+), 50 deletions(-) create mode 100644 example/cap_delegate/Makefile create mode 100644 example/cap_delegate/README.md create mode 100644 example/cap_delegate/cap_delegate.system create mode 100644 example/cap_delegate/delegatee.c create mode 100644 example/cap_delegate/delegation.h create mode 100644 example/cap_delegate/delegator.c create mode 100644 example/cap_delegate/server.c create mode 100644 tool/microkit/tests/sdf/pd_delegate_child_as_delegatee.system create mode 100644 tool/microkit/tests/sdf/pd_delegate_invalid_channel.system create mode 100644 tool/microkit/tests/sdf/pd_delegate_invalid_ioport.system create mode 100644 tool/microkit/tests/sdf/pd_delegate_invalid_irq.system create mode 100644 tool/microkit/tests/sdf/pd_delegate_invalid_map.system create mode 100644 tool/microkit/tests/sdf/pd_delegate_without_delegatee.system diff --git a/example/cap_delegate/Makefile b/example/cap_delegate/Makefile new file mode 100644 index 000000000..28ccf4984 --- /dev/null +++ b/example/cap_delegate/Makefile @@ -0,0 +1,111 @@ +# +# Copyright 2026, UNSW +# +# 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-linux-gnu + 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 + +DELEGATOR_OBJS := delegator.o +DELEGATEE_OBJS := delegatee.o +SERVER_OBJS := server.o + +IMAGES := delegator.elf delegatee.elf server.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 + +APP_NAME := cap_delegate +IMAGE_FILE = $(BUILD_DIR)/$(APP_NAME).img +REPORT_FILE = $(BUILD_DIR)/report.txt + +all: $(IMAGE_FILE) + +$(BUILD_DIR)/%.o: %.c Makefile + $(CC) -c $(CFLAGS) $< -o $@ + +$(BUILD_DIR)/%.o: %.s Makefile + $(AS) -g -mcpu=$(CPU) $< -o $@ + +$(BUILD_DIR)/server.elf: $(addprefix $(BUILD_DIR)/, $(SERVER_OBJS)) + $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ + +$(BUILD_DIR)/delegator.elf: $(addprefix $(BUILD_DIR)/, $(DELEGATOR_OBJS)) + $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ + +$(BUILD_DIR)/delegatee.elf: $(addprefix $(BUILD_DIR)/, $(DELEGATEE_OBJS)) + $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ + +$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) $(APP_NAME).system + $(MICROKIT_TOOL) $(APP_NAME).system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) + +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 diff --git a/example/cap_delegate/README.md b/example/cap_delegate/README.md new file mode 100644 index 000000000..09709c82b --- /dev/null +++ b/example/cap_delegate/README.md @@ -0,0 +1,431 @@ +# Capability Delegation + +Capability delegation allows a parent protection domain (the **delegatee**) to dynamically control a subset of capabilities associated with one of its child protection domains (the **delegator**). + +Instead of installing every capability directly into the delegator PD's CSpace, capabilities marked as *delegated="true"* are placed into a separate **delegation CNode**. The delegation CNode is controlled by the delegatee PD and represents the delegation relationship between one delegatee-delegator pair. + +This allows capability availability to be changed dynamically at runtime without changing the static structure of the system. + +## Delegation Model + +For every `(delegatee, delegator)` PD pair, Microkit creates one delegation CNode. + +The delegation CNode stores: + +1. capabilities to the delegator PD's CSpace objects: + + * the delegator PD's root CNode; + * the delegator PD's microkit CNode; + * the delegation CNode itself; + +2. capabilities for all resources of the delegator PD that are marked as delegated. + +Conceptually: + +```text +Delegatee PD Delegator PD +(parent) (child) + + root CNode ----> root CNode (A) + | | | + | | | + +-- Microkit CNode | +-- Microkit CNode (B) + | | ^ + -> +-- delegation CNode (C) | | + | | | | + | +-- cap -> A ------- | + | +-- cap -> B -------------------- + cap <-C -- + + | + +-- delegated resource caps +``` + +The delegation CNode is therefore not simply another CNode belonging to the delegator. It acts as a capability container associated with the delegation relationship between the delegatee and delegator. + +By default, the delegatee can access the delegation CNode, while the delegator cannot. + +## SDF Interface + +Capability delegation is expressed through attributes in the system description. + +A protection domain that manages delegated capabilities is marked with: + +```xml +delegatee="true" +``` + +A child PD that is permitted to participate in delegation contains resources that are marked as delegated. For example, a channel end or a memory region can use: + +```xml +delegated="true" +``` + +### Example + +```xml + + + + + + + + + + + + + + + + + +``` + +In this example: + +* `delegatee` is responsible for managing delegated capabilities; +* `delegator` is a child PD whose capabilities may be delegated; +* the channel end belonging to `delegator` is marked as delegated. + +Normally, the channel capability used by `delegator` would be installed in the delegator's Microkit CNode. + +Because the channel end is marked with `delegated="true"`, this capability is instead created inside: + +```text +delegation_cnode(delegatee, delegator) +``` + +As a result, the channel is not directly usable by the delegator when the system starts. + +## CSpace Layout + +Microkit PDs use a two-level CSpace. + +A PD has a small root CNode (radix=6) and a larger Microkit CNode (radix=9): + +```text +PD root CNode + | + +-- slot 0 -> Microkit CNode +``` + +For delegation, the delegatee (parent) additionally contains one delegation CNode for each delegator (child). + +For example: + +```text +Delegatee PD + +root CNode +| ++-- slot 0 -> delegatee Microkit CNode +| ++-- slot 48 -> delegation CNode for delegator 0 ++-- slot 49 -> delegation CNode for delegator 1 ++-- ... +``` + +A delegation CNode contains both delegation-management capabilities and delegated resource capabilities: + +```text +Delegation CNode +| ++-- slot 0 -> delegation CNode self-reference ++-- slot 1 -> delegator Microkit CNode ++-- slot 2 -> delegator root CNode ++-- slot 3 -> grantable delegation CNode cap ++-- slot 4 -> delegator VSpace +| ++-- resource slots + +-- delegated notification caps + +-- delegated endpoint caps + +-- delegated memory-region frame caps + +-- delegated I/O port caps +``` + +Delegated resource capabilities retain the same slot number that they would normally occupy in the delegator's Microkit CNode. + +For example, notification channel `0` normally uses: + +```text +BASE_OUTPUT_NOTIFICATION_CAP + 0 +``` + +which is slot `10`. + +If the corresponding channel end is delegated, the capability is placed at: + +```text +delegation CNode slot 10 +``` + +instead of: + +```text +delegator Microkit CNode slot 10 +``` + +This makes moving a capability between the delegation CNode and the normal Microkit CNode straightforward. + +## Capability Management + +There are two possible ways to manage delegated capabilities. + +### Delegatee-Managed Delegation + +The simplest model is for the delegatee to perform all CSpace operations. + +Initially: + +```text +delegation CNode[10] + | + +-- notification capability + +delegator Microkit CNode[10] + | + +-- empty +``` + +When the delegator requests access to the resource, it performs a protected procedure call to the delegatee. + +The delegatee then copies the capability: + +```text +delegation CNode[10] + | + | seL4_CNode_Copy + v +delegator Microkit CNode[10] +``` + +The delegator can then use the normal Microkit API: + +```c +microkit_notify(10); +``` + +When the capability should no longer be available, the delegatee can remove it from the delegator's CSpace. + +The control flow is therefore: + +```text +Delegator Delegatee + + | | + | request capability | + |------------------------->| + | | + | copy capability + | into delegator + | | + |<-------------------------| + | + | use capability + | +``` + +This model keeps all capability management inside the delegatee. + +## Delegator Self-Management + +Capability management can also be temporarily offloaded to the delegator. + +In this model, instead of copying individual resource capabilities on behalf of the delegator (child), the delegatee (parent) temporarily grants the delegator (child) access to its delegation CNode. + +This requires two assumptions: + +1. the delegatee (parent) explicitly grants access to the delegation CNode; +2. the capability-management code executed by the delegator (child) is trusted to follow the delegation protocol. + +The delegation CNode already contains: + +```text +slot 1 -> delegator Microkit CNode +slot 2 -> delegator root CNode +``` + +so once the delegator gains access to the delegation CNode, it can manage its own delegated capabilities. + +### Grant + +Initially: + +```text +Delegator root CNode +| ++-- delegation access slot -> empty +``` + +The delegator asks the delegatee for temporary access. + +The delegatee (parent) installs a capability to the *delegation CNode* into a reserved slot of the delegator's (child) root CNode: + +```text +Delegator root CNode +| ++-- slot N -> delegation CNode +``` + +At this point, the delegator can directly access the delegation CNode. + +### Restore a delegated capability + +Suppose notification channel `0` is stored at delegation CNode slot `10`. + +The delegator can use the Microkit CNode capability stored in delegation CNode slot `1` as the destination: + +```text +delegation CNode +| ++-- slot 1 -> delegator Microkit CNode +| ++-- slot 10 -> notification cap + | + | seL4_CNode_Copy + v + delegator Microkit CNode[10] +``` + +After this operation: + +```text +delegator Microkit CNode[10] + | + +-- notification capability +``` + +and normal Microkit APIs can be used. + +### Release + +Once the delegator (child) finishes using the delegated resources, it removes the temporary resource capabilities from its normal Microkit CNode. It then calls back into the delegatee (parent) to indicate that capability self-management is complete. The delegatee (parent) finally removes the temporary delegation CNode capability from the delegator's (child) root CNode. + +The complete flow is: + +```text +Delegator Delegatee + + | | + | request delegation access | + |-------------------------------->| + | | + | grant access to + | delegation CNode + | | + |<--------------------------------| + | + | copy delegated caps into + | own Microkit CNode + | + | use delegated resources + | + | remove temporary resource caps + | + | release delegation access + |-------------------------------->| + | | + | remove access to + | delegation CNode + | | + |<--------------------------------| +``` + +This mode reduces the amount of per-capability management performed by the delegatee. + +The delegatee controls when self-management begins and ends, while the delegator performs the individual capability operations. + + +## Demo + +This example demonstrates delegation of a notification capability. + +The system contains three PDs: + +```text +delegatee + | + +-- delegator + +server +``` + +There is a notification channel between `delegator` and `server`. + +The delegator's channel end is marked: + +```xml +delegated="true" +``` + +Therefore, at system startup: + +```text +delegator Microkit CNode[10] = empty + +delegation CNode[10] = + notification capability to server +``` + +The demo first attempts: + +```c +microkit_notify(10); +``` + +before the capability has been restored. + +The capability is then made available using one of the delegation-management modes described above. + +After the capability is installed into: + +```text +delegator Microkit CNode[10] +``` + +the same call: + +```c +microkit_notify(CH_SERVER); +``` + +can successfully use the delegated channel. + +### Log + +``` +Booting all finished, dropped to user space +INFO [sel4_capdl_initializer::initialize] Starting CapDL initializer +INFO [sel4_capdl_initializer::initialize] Starting threads +MON|INFO: Microkit Monitor started! + (server) init +[delegatee] init + hello world + request delegation CNode +[delegatee] grant delegation CNode + notify server from channel: 10 +<> + notify server from channel: 10 +<> + notify server from channel: 10 +<> + restore cap: 10 + notify server from channel: 10 + (server) received signal from delegator + notify server from channel: 10 + (server) received signal from delegator + notify server from channel: 10 + (server) received signal from delegator + remove cap: 10 + release delegation CNode +[delegatee] release delegation CNode +[delegatee] notify delegator +::notified: received signal from delegatee +::notified: try notifying server +<> +``` diff --git a/example/cap_delegate/cap_delegate.system b/example/cap_delegate/cap_delegate.system new file mode 100644 index 000000000..b155eb4a4 --- /dev/null +++ b/example/cap_delegate/cap_delegate.system @@ -0,0 +1,32 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/example/cap_delegate/delegatee.c b/example/cap_delegate/delegatee.c new file mode 100644 index 000000000..53e04876c --- /dev/null +++ b/example/cap_delegate/delegatee.c @@ -0,0 +1,120 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include "delegation.h" + +#define CH_DELEGATEE ((microkit_channel)1) + +// Delegation CNode in the delegatee CSpace. +#define CPTR_DGT_CND \ + (microkit_cspace_root_slot_to_cptr(48)) + +void init(void) +{ + microkit_dbg_puts("[delegatee] init\n"); +} + +void notified(microkit_channel ch) +{ +} + +seL4_MessageInfo_t protected(microkit_channel ch, microkit_msginfo msginfo) +{ + seL4_Error err; + seL4_Word label = microkit_msginfo_get_label(msginfo); + + switch (label) { + case PPC_DELEGATION_GRANT: + microkit_dbg_puts("[delegatee] grant delegation CNode\n"); + + // Copy the delegation CNode cap into delegator.root[15]. + // slot 15 must be (reserved) free... +#ifdef ANALYSIS_FOR_ARGS + err = seL4_CNode_Copy( +// CPTR_DGT_CNG = 48 << (64 - 6) | 0 +// DELEGATION_SLOT_ROOT_CNODE = 2 +// +// DGT_CPTR__DGTR_ROOT_CND(CPTR_DGT_CND) +// = (CPTR_DGT_CND) | DELEGATION_SLOT_ROOT_CNODE +// = (CPTR_DGT_CND) | 2 +// +// => slot 2 of delegation CNode points to +// + the cap of the root CNode of the delegator PD +// + with guard_size = 0 +// => during a CNode capability lookup process +// the root cap will consume the first 6 bits of the CPtr +// given that the CPtr is (48 << (64 - 6) | 2) +// the higher 6 bits is then 110000b = 48 +// now we will get slot 48 of the root CNode of current PD +// which points to the cap of the delegation CNode of the first delegator +// (valid range: 48 ~ 63, for delegators 0 ~ 15) +// with guard_size = (64-6) - 9 (set by microkit tool) +// = milestone => reached 'delegation CNode' of the first delegator +// if we continue and use the remaining (64-6) bits to minus guard_size +// we will still have 9 bits left for CNode cap lookup +// currently the remaining 9 bits is 000000010b (from the CPtr) +// which points to slot 2 of the delegation CNode +// and now all lookup address bits are used +// so, we will get the cap of the slot 2 of the delegation CNode +// which is the cap of the root CNode of the target delegator PD +// => final => reached delegator PD's 'root CNode' +// => Once this CNode cap lookup is finished, +// we can use GRANT_SLOT to perform the actual lookup +// for the destination slot in the target CNode +// i.e., slot 15 +// +// +// LOOKUP_DEPTH__RT = 6 +// (target CNode => delegator PD's 'root CNode' with guard_size = 0) +// +// => the root CNode cap has guard_size = 0, so all +// LOOKUP_DEPTH__RT = 6 bits are used as radix bits. +// so 'slot' directly selects root CNode[slot]. +// => we will finally get the cap in the 'slot' of 'root CNode' +// + DGT_CPTR__DGTR_ROOT_CND(CPTR_DGT_CND), GRANT_SLOT, LOOKUP_DEPTH__RT, +// Similarly, slot 3 of delegation CNode of the first delegator PD +// points to the cap of the delegation CNode itself (i.e., a self-pointing cap) +// (for lookup analysis, check delegator.c for details...) + CPTR_DGT_CND, DELEGATION_SLOT_GRANT_CAP, LOOKUP_DEPTH__DL, + seL4_AllRights + ); +#else + err = seL4_CNode_Copy( + DGT_CPTR__DGTR_ROOT_CND(CPTR_DGT_CND), GRANT_SLOT, LOOKUP_DEPTH__RT, + CPTR_DGT_CND, DELEGATION_SLOT_GRANT_CAP, LOOKUP_DEPTH__DL, + seL4_AllRights + ); +#endif + if (err != seL4_NoError) { + microkit_dbg_puts("[delegatee] failed to grant delegation CNode\n"); + for (;;); + } + break; + + case PPC_DELEGATION_RELEASE: + microkit_dbg_puts("[delegatee] release delegation CNode\n"); + + // Remove the delegation CNode cap from delegator.root[15]. + err = seL4_CNode_Delete( + DGT_CPTR__DGTR_ROOT_CND(CPTR_DGT_CND), GRANT_SLOT, LOOKUP_DEPTH__RT + ); + + if (err != seL4_NoError) { + microkit_dbg_puts("[delegatee] failed to remove delegation CNode\n"); + for (;;); + } + + microkit_dbg_puts("[delegatee] notify delegator\n"); + microkit_notify(CH_DELEGATEE); + break; + + default: + microkit_dbg_puts("[delegatee] invalid delegation request\n"); + break; + } + + return microkit_msginfo_new(0, 0); +} diff --git a/example/cap_delegate/delegation.h b/example/cap_delegate/delegation.h new file mode 100644 index 000000000..7f06a986d --- /dev/null +++ b/example/cap_delegate/delegation.h @@ -0,0 +1,38 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include + +// Size of microkit/delegation CNode +#define MK_CAP_BITS 9 +// Size of root CNode +#define ROOT_CAP_BITS 6 + +#define LOOKUP_DEPTH__MK (MK_CAP_BITS) +#define LOOKUP_DEPTH__RT (ROOT_CAP_BITS) +#define LOOKUP_DEPTH__DL (seL4_WordBits - ROOT_CAP_BITS - MK_CAP_BITS) + +// Request types provided by the delegatee... +#define PPC_DELEGATION_GRANT 0 +#define PPC_DELEGATION_RELEASE 1 + +// Delegatee PD will put the cap of delegation CNode to this slot +// at the root CNode of the delegator PD temporarily, in response +// to the "PPC_DELEGATION_GRANT" request... +#define GRANT_SLOT 15 + +// Delegation CNode layout. +#define DELEGATION_SLOT_MICROKIT_CNODE 1 +#define DELEGATION_SLOT_ROOT_CNODE 2 +#define DELEGATION_SLOT_GRANT_CAP 3 + +// Delegator PD's Microkit CNode, accessible through the delegation CNode. +#define DGT_CPTR__DGTR_MK_CND(CPTR_DGT_CND) \ + (CPTR_DGT_CND | DELEGATION_SLOT_MICROKIT_CNODE) + +// Delegator PD's root CNode, accessible through the delegation CNode. +#define DGT_CPTR__DGTR_ROOT_CND(CPTR_DGT_CND) \ + (CPTR_DGT_CND | DELEGATION_SLOT_ROOT_CNODE) diff --git a/example/cap_delegate/delegator.c b/example/cap_delegate/delegator.c new file mode 100644 index 000000000..5b3219393 --- /dev/null +++ b/example/cap_delegate/delegator.c @@ -0,0 +1,219 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include "delegation.h" + +#define CH_SERVER ((microkit_channel)0) +#define CH_DELEGATEE ((microkit_channel)1) + +// Delegation CNode temporarily installed in this PD's root CNode. +#define CPTR_DGT_CND \ + (microkit_cspace_root_slot_to_cptr(GRANT_SLOT)) + +typedef void (*entry_t)(void); + +static void delegation_restore_cap(seL4_Word slot) +{ + microkit_dbg_puts(" restore cap: "); + microkit_dbg_put32(slot); + microkit_dbg_puts("\n"); + + // to => 'microkit' CNode (of delegator PD) + // from <= 'delegation' CNode + // + seL4_Error err = +#ifdef ANALYSIS_FOR_ARGS + seL4_CNode_Copy( /* DGT_CPTR__DGTR_MK_CND(CPTR_DGT_CND), slot, LOOKUP_DEPTH__MK, */ +// ANALYSIS for below: +// +// CPTR_DGT_CND = 15 << (64 - 6) | 0 +// DELEGATION_SLOT_MICROKIT_CNODE = 1 +// +// DGT_CPTR__DGTR_MK_CND(CPTR_DGT_CND) +// = (CPTR_DGT_CND) | DELEGATION_SLOT_MICROKIT_CNODE +// = (CPTR_DGT_CND) | 1 +// +// => slot 1 of delegation CNode points to +// + the cap of the microkit CNode of the delegator PD +// + with guard_size = 0 +// => during a CNode capability lookup process +// the root cap will consume the first 6 bits of the CPtr +// given that the CPtr is (15 << (64 - 6) | 1) +// the higher 6 bits is then 001111b = 15 +// now we will get slot 15 of the root CNode of current PD +// which points to the cap of the delegation CNode +// with guard_size = (64-6) - 9 (set by microkit tool) +// = milestone => reached 'delegation CNode' +// if we continue and use the remaining (64-6) bits to minus guard_size +// we will still have 9 bits left for CNode cap lookup +// currently the remaining 9 bits is 000000001b (from the CPtr) +// which points to slot 1 of the delegation CNode +// and now all lookup address bits are used +// so, we will get the cap of the slot 1 of the delegation CNode +// which is the cap of the microkit CNode of the delegator PD +// => final => reached delegator PD's 'microkit CNode' +// => Once this CNode cap lookup is finished, +// we can use the 'slot' arg to perform the actual lookup +// for the destination slot in the target CNode +// +// LOOKUP_DEPTH__MK = 9 +// (target CNode => delegator PD's 'microkit CNode' with guard_size = 0) +// +// => The Microkit CNode cap has guard_size = 0, so all +// LOOKUP_DEPTH__MK = 9 bits are used as radix bits. +// so 'slot' directly selects Microkit CNode[slot]. +// => we will finally get the cap in the 'slot' of 'microkit CNode' +// + DGT_CPTR__DGTR_MK_CND(CPTR_DGT_CND), slot, LOOKUP_DEPTH__MK, + +// ANALYSIS for below: +// +// CPTR_DGT_CND = 15 << (64 - 6) | 0 +// +// => slot 0 of delegation CNode is a self-pointing cap +// => during a CNode capability lookup process +// the root CNode will consume the first 6 bit +// and 15 points to the cap of delegation CNode cap +// which is initialised with guard_size = 64 - 6 - 9 +// the current remaining lookup bits are 58 +// once the guard size is consumed, the final bits are 9 +// 9 equals to the radix of delegation CNode +// and the remanining 9 bit is 000000000b +// which points to slot 0, i.e., the self-pointing cap +// so CPTR_DGT_CND will give you the cap of the delegation CNode +// +// => Once this CNode cap lookup is finished, +// we can use the 'slot' arg to perform the actual lookup +// for the source slot in the target CNode +// +// LOOKUP_DEPTH__DL = 64 - 6 - 9 = 49 +// (target CNode => delegator PD's 'delegation CNode' with guard_size = 40) +// (i.e., self-pointing cap has guard size = (64 - 6 - 9 - 9) = 40) +// +// => during the final cap lookup process, we will use 40 bits out of LOOKUP_DEPTH__DL +// for parsing the guard size of target CNode (i.e., the 'delegation CNode') +// Since 'slot' only occupies the low 9 bits, the upper 40 bits +// of the 49-bit source index are zero and match the self-cap's +// zero-valued 40-bit guard. The remaining 9 bits of the lookup depth +// matches with the radix of the 'delegation CNode' +// => we will finally get the cap in the 'slot' of 'delegation CNode' +// + CPTR_DGT_CND, /* access via delegtor */ slot, LOOKUP_DEPTH__DL, + seL4_AllRights + ); +#else + seL4_CNode_Copy( + DGT_CPTR__DGTR_MK_CND(CPTR_DGT_CND), slot, LOOKUP_DEPTH__MK, + CPTR_DGT_CND, /* access via delegtor */ slot, LOOKUP_DEPTH__DL, + seL4_AllRights + ); +#endif + if (err != seL4_NoError) { + microkit_dbg_puts(" failed to restore cap: "); + microkit_dbg_put32(slot); + microkit_dbg_puts("\n"); + for (;;); + } +} + +static void delegation_remove_cap(seL4_Word slot) +{ + microkit_dbg_puts(" remove cap: "); + microkit_dbg_put32(slot); + microkit_dbg_puts("\n"); + + seL4_Error err = + seL4_CNode_Delete( +// Delete the slot cap from the microkit CNode of the delegator PD +// (when the cap of the microkit CNode is accessed via the delegation CNode) + DGT_CPTR__DGTR_MK_CND(CPTR_DGT_CND), slot, LOOKUP_DEPTH__MK + ); + + if (err != seL4_NoError) { + microkit_dbg_puts(" failed to remove cap: "); + microkit_dbg_put32(slot); + microkit_dbg_puts("\n"); + for (;;); + } +} + +static void request_delegation_cnode(void) +{ + microkit_dbg_puts(" request delegation CNode\n"); + microkit_ppcall( + CH_DELEGATEE, + microkit_msginfo_new(PPC_DELEGATION_GRANT, 0) + ); +} + +static void release_delegation_cnode(void) +{ + microkit_dbg_puts(" release delegation CNode\n"); + microkit_ppcall( + CH_DELEGATEE, + microkit_msginfo_new(PPC_DELEGATION_RELEASE, 0) + ); +} + +// +// This function uses the 'test_func' to test the validity of 'slot' +// The slot must be a slot of delegated capability +// +static void delegator_self_mng_test(seL4_Word slot, entry_t test_func) +{ + // This should fail, + // as the channel capability is delegated. + int loop = 3; + do { + test_func(); + } while (--loop); + + // Restore the delegated channel cap to its normal Microkit slot. + delegation_restore_cap(slot); + + // This will succeed, + // as the channel capability is now valid. + loop = 3; + do { + test_func(); + } while (--loop); + + // Remove the restored capability before releasing delegation access. + delegation_remove_cap(slot); +} + +static void delegator_self_mng_test_wrapper(seL4_Word slot, entry_t test_func) +{ + // Ask the delegatee for temporary access to the delegation CNode. + request_delegation_cnode(); + + // Perform test... + delegator_self_mng_test(slot, test_func); + + release_delegation_cnode(); +} + +static void signal_test(void) +{ + microkit_dbg_puts(" notify server from channel: "); + microkit_dbg_put32(CH_SERVER + BASE_OUTPUT_NOTIFICATION_CAP); + microkit_dbg_puts("\n"); + + microkit_notify(CH_SERVER); +} + +void init(void) +{ + microkit_dbg_puts(" hello world\n"); + + delegator_self_mng_test_wrapper(CH_SERVER + BASE_OUTPUT_NOTIFICATION_CAP, signal_test); +} + +void notified(microkit_channel ch) +{ + microkit_dbg_puts("::notified: received signal from delegatee\n"); + microkit_dbg_puts("::notified: try notifying server\n"); + microkit_notify(CH_SERVER); +} diff --git a/example/cap_delegate/server.c b/example/cap_delegate/server.c new file mode 100644 index 000000000..407bf2918 --- /dev/null +++ b/example/cap_delegate/server.c @@ -0,0 +1,19 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include + +#define CH_CLIENT ((microkit_channel) 0) + +void init(void) +{ + microkit_dbg_puts(" (server) init\n"); +} + +void notified(microkit_channel ch) +{ + microkit_dbg_puts(" (server) received signal from delegator\n"); +} diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 5266ca168..afc2bbd39 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -96,11 +96,24 @@ const PD_BASE_IOPORT_CAP: u64 = PD_BASE_VCPU_CAP + 64; /* 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; + +const PD_ROOT_CAP_SLOT_RSVD: u32 = 16; +const PD_ROOT_CAP_SLOT_RSVD_START: u32 = PD_ROOT_CAP_SIZE - PD_ROOT_CAP_SLOT_RSVD; + 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; +const DLG_CNODE_SELF_CNODE_CAP: u32 = 0; +const DLG_CNODE_DGTR_MK_CNODE_CAP: u32 = 1; +const DLG_CNODE_DGTR_RT_CNODE_CAP: u32 = 2; +const DLG_CNODE_DGTR_DL_CNODE_CAP: u32 = 3; +const DLG_CNODE_DGTR_VSPACE_CAP: u32 = 4; + +const DLG_PPC_CAP: u32 = PD_BASE_OUTPUT_ENDPOINT_CAP as u32; +const DLG_MR_CAP: u32 = DLG_PPC_CAP + 64; + pub const SLOT_BITS: u64 = 5; pub const SLOT_SIZE: u64 = 1 << SLOT_BITS; @@ -303,6 +316,7 @@ impl CapDLSpecContainer { frame_cap, page_size_bytes, cur_vaddr, + false, /* MR for provided elf cannot be delegated */ ) { Ok(_) => { frame_sequence += 1; @@ -361,18 +375,36 @@ fn map_memory_region( page_sz: u64, target_address_space: &AddressSpace, frames: &[ObjectId], + mut delegation: Option<(&mut Vec, u32)>, ) -> Result<(), String> { let mut cur_vaddr = map.addr(); let read = map.read(); let write = map.write(); let execute = map.execute(); + let delegated = map.delegated(); + if delegated != delegation.is_some() { + return Err(format!( + "invalid delegation arguments for {} '{}': delegated={}, delegation={}", + map.element(), + map.mr_name(), + delegated, + delegation.is_some(), + )); + } for frame_obj_id in frames.iter() { // Make a cap for this frame. let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, read, write, execute, map.cached()); // Map it into this PD address space. target_address_space - .map_page(spec_container, sel4_config, frame_cap, page_sz, cur_vaddr) + .map_page( + spec_container, + sel4_config, + frame_cap.clone(), + page_sz, + cur_vaddr, + delegated, + ) .map_err(|err| { format!( "failed to map {} for MR '{}' into address-space '{}' at {} {:#x}: {err}", @@ -384,6 +416,13 @@ fn map_memory_region( ) })?; cur_vaddr += page_sz; + + if let Some((cnode, slot)) = delegation.as_mut() { + cnode.push(capdl_util_make_cte(*slot, frame_cap)); + + *slot += 1; + assert!(*slot <= PD_CAP_SIZE); + } } Ok(()) } @@ -468,6 +507,7 @@ pub fn build_capdl_spec( mon_stack_frame_cap, PageSize::Small as u64, kernel_config.pd_stack_bottom(MON_STACK_SIZE), + false, ) .unwrap(); @@ -489,6 +529,7 @@ pub fn build_capdl_spec( mon_ipcbuf_frame_cap.clone(), PageSize::Small as u64, kernel_config.pd_ipc_buffer(), + false, ) .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); @@ -627,11 +668,15 @@ pub fn build_capdl_spec( // Keep tabs on each PD's stack bottom so we can write it out to the monitor for stack overflow detection. let mut pd_stack_bottoms: Vec = Vec::new(); + let mut delegation_cnodes: HashMap = HashMap::new(); + let mut delegation_cnode_caps: HashMap> = HashMap::new(); + for (pd_global_idx, pd) in system.protection_domains.iter().enumerate() { let elf_obj = &elfs[pd_global_idx]; let mut caps_to_bind_to_tcb: Vec = Vec::new(); let mut caps_to_insert_to_pd_cspace: Vec = Vec::new(); + let mut caps_to_insert_to_pd_delegation_cnode: Vec = Vec::new(); // Step 3-1: Create TCB and VSpace with all ELF loadable frames mapped in. let pd_elf_spec = spec_container @@ -656,6 +701,13 @@ pub fn build_capdl_spec( capdl_util_make_page_table_cap(pd_vspace_obj_id), )); + if pd.allow_delegation { + caps_to_insert_to_pd_delegation_cnode.push(capdl_util_make_cte( + DLG_CNODE_DGTR_VSPACE_CAP, + capdl_util_make_page_table_cap(pd_vspace_obj_id), + )) + } + // Step 3-2: Map in all Memory Regions for map in pd.maps.iter() { let frames = &mr_name_to_frames[&map.mr]; @@ -681,14 +733,27 @@ pub fn build_capdl_spec( } } - map_memory_region( - &mut spec_container, - kernel_config, - map, - page_size_bytes, - &pd_elf_spec.address_space, - frames, - )?; + if map.delegated() { + map_memory_region( + &mut spec_container, + kernel_config, + map, + page_size_bytes, + &pd_elf_spec.address_space, + frames, + Some((&mut caps_to_insert_to_pd_delegation_cnode, DLG_MR_CAP)), + )?; + } else { + map_memory_region( + &mut spec_container, + kernel_config, + map, + page_size_bytes, + &pd_elf_spec.address_space, + frames, + None, + )?; + } } // Step 3-3a: Create and map in the IPC buffer @@ -709,6 +774,7 @@ pub fn build_capdl_spec( ipcbuf_frame_cap.clone(), PageSize::Small as u64, kernel_config.pd_ipc_buffer(), + false, /* ipc buffer should never be delegated */ ) .expect("should be able to map the IPC buffer as we checked overlaps in sel4.rs"); caps_to_bind_to_tcb.push(capdl_util_make_cte( @@ -740,6 +806,7 @@ pub fn build_capdl_spec( stack_frame_cap, PageSize::Small as u64, cur_stack_vaddr, + false, /* default stack should never be delegated*/ ) .unwrap(); cur_stack_vaddr += PageSize::Small as u64; @@ -893,6 +960,7 @@ pub fn build_capdl_spec( page_size_bytes, &vm_address_space, frames, + None, /* VM does not support delegated MR now */ )?; } @@ -1150,6 +1218,107 @@ pub fn build_capdl_spec( tcb: pd_tcb_obj_id, }, ); + + if pd.allow_delegation { + delegation_cnode_caps.insert(pd_global_idx, caps_to_insert_to_pd_delegation_cnode); + } + } + + // Step 3-16. Create delegation CNodes + for (delegatee_idx, pd_delegatee) in system + .protection_domains + .iter() + .enumerate() + .filter(|(_, pd)| pd.delegatee) + { + let pd_delegators: Vec<(usize, _)> = system + .protection_domains + .iter() + .enumerate() + .filter(|(_, child)| child.parent == Some(delegatee_idx) && child.allow_delegation) + .collect(); + + if pd_delegators.len() > PD_ROOT_CAP_SLOT_RSVD as usize { + return Err(format!( + "ERROR: delegatee PD '{}' has {} children with allow_delegation, \ + but only {} delegation CNode slots are available", + pd_delegatee.name, + pd_delegators.len(), + PD_ROOT_CAP_SLOT_RSVD, + )); + } + + let delegatee_cspace = &pd_shadow_cspaces[&delegatee_idx]; + + for (slot_offset, (id_delegator, pd_delegator)) in pd_delegators.into_iter().enumerate() { + let caps = delegation_cnode_caps + .remove(&id_delegator) + .unwrap_or_default(); + + let delegation_cnode = capdl_util_make_cnode_obj( + &mut spec_container, + &format!( + "delegation_cnode_{}_{}", + pd_delegatee.name, pd_delegator.name + ), + PD_CAP_BITS, + caps, + ); + + let guard_size = + kernel_config.cap_address_bits - PD_ROOT_CAP_BITS as u64 - 2 * PD_CAP_BITS as u64; + + // Slot 0: self-reference. + capdl_util_insert_cap_into_cspace( + &mut spec_container, + delegation_cnode, + DLG_CNODE_SELF_CNODE_CAP, + capdl_util_make_cnode_cap(delegation_cnode, 0, guard_size as u8), + ); + + // Slot 1: microkit CNode of the delegator PD. + let delegator_cspace = &pd_shadow_cspaces[&id_delegator]; + capdl_util_insert_cap_into_cspace( + &mut spec_container, + delegation_cnode, + DLG_CNODE_DGTR_MK_CNODE_CAP, + capdl_util_make_cnode_cap( + delegator_cspace.microkit_cnode, + 0, + 0, /* guard_size */ + ), + ); + + // Slot 2: root CNode of the delegator PD. + capdl_util_insert_cap_into_cspace( + &mut spec_container, + delegation_cnode, + DLG_CNODE_DGTR_RT_CNODE_CAP, + capdl_util_make_cnode_cap(delegator_cspace.cspace, 0, 0 /* guard_size */), + ); + + // Slot 3: delegation CNode cap for granting to the delegator PD. + let delegatee_guard_size = + kernel_config.cap_address_bits - PD_ROOT_CAP_BITS as u64 - PD_CAP_BITS as u64; + + capdl_util_insert_cap_into_cspace( + &mut spec_container, + delegation_cnode, + DLG_CNODE_DGTR_DL_CNODE_CAP, + capdl_util_make_cnode_cap(delegation_cnode, 0, delegatee_guard_size as u8), + ); + + // allow the delegatees to access the delegation cnodes + delegatee_cspace.insert_cap_into_root_cnode( + &mut spec_container, + PD_ROOT_CAP_SLOT_RSVD_START + slot_offset as u32, + capdl_util_make_cnode_cap(delegation_cnode, 0, delegatee_guard_size as u8), + ); + + // records each delegation(delegatee, delegator) pair + // (the delegatee is implicitly recorded as the parent of delegator) + delegation_cnodes.insert(id_delegator, delegation_cnode); + } } // ********************************* @@ -1166,22 +1335,40 @@ pub fn build_capdl_spec( let pd_a_ntfn_cap_idx = PD_BASE_OUTPUT_NOTIFICATION_CAP + channel.end_a.id; let pd_a_ntfn_badge = 1 << channel.end_b.id; let pd_a_ntfn_cap = capdl_util_make_ntfn_cap(pd_b_ntfn_id, true, true, pd_a_ntfn_badge); - pd_a_shadow_cspace.insert_cap_into_microkit_cnode( - &mut spec_container, - pd_a_ntfn_cap_idx as u32, - pd_a_ntfn_cap, - ); + if channel.end_a.delegated { + capdl_util_insert_cap_into_cspace( + &mut spec_container, + delegation_cnodes[&channel.end_a.pd], + pd_a_ntfn_cap_idx as u32, + pd_a_ntfn_cap, + ); + } else { + pd_a_shadow_cspace.insert_cap_into_microkit_cnode( + &mut spec_container, + pd_a_ntfn_cap_idx as u32, + pd_a_ntfn_cap, + ); + } } if channel.end_b.notify { let pd_b_ntfn_cap_idx = PD_BASE_OUTPUT_NOTIFICATION_CAP + channel.end_b.id; let pd_b_ntfn_badge = 1 << channel.end_a.id; let pd_b_ntfn_cap = capdl_util_make_ntfn_cap(pd_a_ntfn_id, true, true, pd_b_ntfn_badge); - pd_b_shadow_cspace.insert_cap_into_microkit_cnode( - &mut spec_container, - pd_b_ntfn_cap_idx as u32, - pd_b_ntfn_cap, - ); + if channel.end_b.delegated { + capdl_util_insert_cap_into_cspace( + &mut spec_container, + delegation_cnodes[&channel.end_b.pd], + pd_b_ntfn_cap_idx as u32, + pd_b_ntfn_cap, + ); + } else { + pd_b_shadow_cspace.insert_cap_into_microkit_cnode( + &mut spec_container, + pd_b_ntfn_cap_idx as u32, + pd_b_ntfn_cap, + ); + } } if channel.end_a.pp { @@ -1192,11 +1379,20 @@ pub fn build_capdl_spec( .expect("exists as needs_ep() is true"); let pd_a_ep_cap = capdl_util_make_endpoint_cap(pd_b_ep_id, true, true, true, pd_a_ep_badge); - pd_a_shadow_cspace.insert_cap_into_microkit_cnode( - &mut spec_container, - pd_a_ep_cap_idx as u32, - pd_a_ep_cap, - ); + if channel.end_a.delegated { + capdl_util_insert_cap_into_cspace( + &mut spec_container, + delegation_cnodes[&channel.end_a.pd], + pd_a_ep_cap_idx as u32, + pd_a_ep_cap, + ); + } else { + pd_a_shadow_cspace.insert_cap_into_microkit_cnode( + &mut spec_container, + pd_a_ep_cap_idx as u32, + pd_a_ep_cap, + ); + } } if channel.end_b.pp { @@ -1207,11 +1403,20 @@ pub fn build_capdl_spec( .expect("exists as needs_ep() is true"); let pd_b_ep_cap = capdl_util_make_endpoint_cap(pd_a_ep_id, true, true, true, pd_b_ep_badge); - pd_b_shadow_cspace.insert_cap_into_microkit_cnode( - &mut spec_container, - pd_b_ep_cap_idx as u32, - pd_b_ep_cap, - ); + if channel.end_b.delegated { + capdl_util_insert_cap_into_cspace( + &mut spec_container, + delegation_cnodes[&channel.end_b.pd], + pd_b_ep_cap_idx as u32, + pd_b_ep_cap, + ); + } else { + pd_b_shadow_cspace.insert_cap_into_microkit_cnode( + &mut spec_container, + pd_b_ep_cap_idx as u32, + pd_b_ep_cap, + ); + } } } @@ -1249,6 +1454,7 @@ pub fn build_capdl_spec( page_size_bytes, address_space, &mr_name_to_frames[&iomap.mr], + None, /* IOMMU does not support delegated MR now */ )?; } diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index 67a73626f..dc732befd 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -92,6 +92,7 @@ impl AddressSpace { frame_cap: Cap, frame_size_bytes: u64, addr: u64, + delegated: bool, ) -> Result<(), String> { self.map_recursive( spec_container, @@ -101,6 +102,7 @@ impl AddressSpace { frame_cap, frame_size_bytes, addr, + delegated, ) } @@ -192,6 +194,7 @@ impl AddressSpace { frame_cap: Cap, frame_size_bytes: u64, addr: u64, + delegated: bool, ) -> Result<(), String> { if cur_level >= self.address_space_levels(sel4_config) { unreachable!("internal bug: recursed past the final address-space level"); @@ -201,14 +204,18 @@ impl AddressSpace { let leaf_level = self.get_leaf_level(sel4_config, frame_size_bytes); if cur_level == leaf_level { - self.insert_cap_into_level( - spec_container, - sel4_config, - cur_level_obj_id, - cur_level, - slot, - frame_cap, - ) + if !delegated { + self.insert_cap_into_level( + spec_container, + sel4_config, + cur_level_obj_id, + cur_level, + slot, + frame_cap, + ) + } else { + Ok(()) + } } else { let next_obj_id = self.map_intermediary_level_helper( spec_container, @@ -226,6 +233,7 @@ impl AddressSpace { frame_cap, frame_size_bytes, addr, + delegated, ) } } diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index ffb40b5d2..47283da82 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -183,6 +183,7 @@ pub fn parse( &xml_sdf, &*child, ProtectionDomainRole::Normal, + false, /* top-level PDs are not allowed to delegate cap controls */ &domains, )?), "channel" => channel_nodes.push(child), diff --git a/tool/microkit/src/sdf/channels.rs b/tool/microkit/src/sdf/channels.rs index e400cf0aa..18f22d135 100644 --- a/tool/microkit/src/sdf/channels.rs +++ b/tool/microkit/src/sdf/channels.rs @@ -6,7 +6,9 @@ use super::consts::*; use super::pd_vm::ProtectionDomain; -use super::util::{check_attributes, checked_lookup, loc_string, value_error}; +use super::util::{ + check_attributes, checked_lookup, ensure_delegation_allowed, loc_string, value_error, +}; use super::{SdfNode, SystemDescriptionFile}; use crate::util::str_to_bool; @@ -18,6 +20,7 @@ pub struct ChannelEnd { pub notify: bool, pub pp: bool, pub setvar_id: Option, + pub delegated: bool, } #[derive(Debug)] @@ -42,7 +45,11 @@ impl ChannelEnd { )); } - check_attributes(xml_sdf, node, &["pd", "id", "pp", "notify", "setvar_id"])?; + check_attributes( + xml_sdf, + node, + &["pd", "id", "pp", "notify", "setvar_id", "delegated"], + )?; let end_pd = checked_lookup(xml_sdf, node, "pd")?; let end_id = checked_lookup(xml_sdf, node, "id")?.parse::().unwrap(); @@ -58,6 +65,21 @@ impl ChannelEnd { return Err(value_error(xml_sdf, node, "id must be >= 0".to_string())); } + let delegated = if let Some(xml_delegated) = node.attribute("delegated") { + match str_to_bool(xml_delegated) { + Some(val) => val, + None => { + return Err(value_error( + xml_sdf, + node, + "delegated must be 'true' or 'false'".to_string(), + )) + } + } + } else { + false + }; + let notify = node .attribute("notify") .map(str_to_bool) @@ -78,14 +100,18 @@ impl ChannelEnd { value_error(xml_sdf, node, "pp must be 'true' or 'false'".to_string()) })?; - if let Some(pd_idx) = pds.iter().position(|pd| pd.name == end_pd) { + if let Some((pd_idx, pd)) = pds.iter().enumerate().find(|(_, pd)| pd.name == end_pd) { let setvar_id = node.attribute("setvar_id").map(ToOwned::to_owned); + if node.attribute("delegated").is_some() { + ensure_delegation_allowed(pd.allow_delegation, xml_sdf, node)?; + } Ok(ChannelEnd { pd: pd_idx, id: end_id.try_into().unwrap(), notify, pp, setvar_id, + delegated, }) } else { Err(value_error( diff --git a/tool/microkit/src/sdf/consts.rs b/tool/microkit/src/sdf/consts.rs index d391f7018..54f6d7b62 100644 --- a/tool/microkit/src/sdf/consts.rs +++ b/tool/microkit/src/sdf/consts.rs @@ -18,7 +18,10 @@ pub 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`. -pub const CAP_MAP_MAX_SLOT: u64 = 128; +pub const CAP_MAP_MAX_SLOT: u64 = 64; + +pub const PD_ROOT_CAP_SLOT_RSVD: u64 = 16; +pub const PD_ROOT_CAP_SLOT_RSVD_START: u64 = CAP_MAP_MAX_SLOT - PD_ROOT_CAP_SLOT_RSVD; pub const MONITOR_PRIORITY: u8 = 255; pub const PD_MAX_PRIORITY: u8 = 254; diff --git a/tool/microkit/src/sdf/cspace.rs b/tool/microkit/src/sdf/cspace.rs index 71f5f9b0c..b4bff2155 100644 --- a/tool/microkit/src/sdf/cspace.rs +++ b/tool/microkit/src/sdf/cspace.rs @@ -45,6 +45,7 @@ impl CapMap { cap_type: CapMapType, xml_sdf: &SystemDescriptionFile, node: &dyn SdfNode, + acpt_delegators: bool, ) -> Result { // At the moment the four cap maps we support all have the 'pd' element, // so we can include it here. When that stops being the case we will @@ -70,6 +71,18 @@ impl CapMap { node, format!("There are only {CAP_MAP_MAX_SLOT} destination cspace slots available."), )); + } else if slot >= PD_ROOT_CAP_SLOT_RSVD_START && acpt_delegators { + return Err(value_error( + xml_sdf, + node, + format!( + "slot {} overlaps with the final {} slots ({}...{}), which are reserved for delegators", + slot, + PD_ROOT_CAP_SLOT_RSVD, + PD_ROOT_CAP_SLOT_RSVD_START, + CAP_MAP_MAX_SLOT - 1, + ), + )); } Ok(CapMap { @@ -87,6 +100,7 @@ impl CSpace { pub(super) fn from_xml( xml_sdf: &SystemDescriptionFile, node: &dyn SdfNode, + acpt_delegators: bool, ) -> Result { check_attributes(xml_sdf, node, &[])?; @@ -94,9 +108,9 @@ impl CSpace { for child in node.children() { cap_maps.push(match child.tag_name() { - "cap_tcb" => CapMap::from_xml(CapMapType::Tcb, xml_sdf, &*child)?, - "cap_sc" => CapMap::from_xml(CapMapType::Sc, xml_sdf, &*child)?, - "cap_vspace" => CapMap::from_xml(CapMapType::VSpace, xml_sdf, &*child)?, + "cap_tcb" => CapMap::from_xml(CapMapType::Tcb, xml_sdf, &*child, acpt_delegators)?, + "cap_sc" => CapMap::from_xml(CapMapType::Sc, xml_sdf, &*child, acpt_delegators)?, + "cap_vspace" => CapMap::from_xml(CapMapType::VSpace, xml_sdf, &*child, acpt_delegators)?, child_name => { let location = loc_string(xml_sdf, child.range().start); if let Some(type_name) = child_name.strip_prefix("cap_") { diff --git a/tool/microkit/src/sdf/irq.rs b/tool/microkit/src/sdf/irq.rs index 56dc2c7a7..552261b00 100644 --- a/tool/microkit/src/sdf/irq.rs +++ b/tool/microkit/src/sdf/irq.rs @@ -35,6 +35,7 @@ pub enum SysIrqKind { pub struct SysIrq { pub id: u64, pub kind: SysIrqKind, + pub delegated: bool, } impl SysIrq { diff --git a/tool/microkit/src/sdf/memory_region.rs b/tool/microkit/src/sdf/memory_region.rs index 88ac061fd..63db7ab87 100644 --- a/tool/microkit/src/sdf/memory_region.rs +++ b/tool/microkit/src/sdf/memory_region.rs @@ -50,6 +50,7 @@ pub struct SysMap { pub vaddr: u64, pub perms: u8, pub cached: bool, + pub delegated: bool, /// Location in the parsed SDF file. Because this struct is /// used in a non-XML context, we make the position optional. pub text_pos: Option, @@ -66,6 +67,7 @@ pub trait Map { fn write(&self) -> bool; fn execute(&self) -> bool; fn cached(&self) -> bool; + fn delegated(&self) -> bool; } impl Map for SysMap { @@ -108,6 +110,10 @@ impl Map for SysMap { fn cached(&self) -> bool { self.cached } + + fn delegated(&self) -> bool { + self.delegated + } } impl Map for SysIOMap { @@ -150,6 +156,10 @@ impl Map for SysIOMap { fn cached(&self) -> bool { false } + + fn delegated(&self) -> bool { + false + } } #[derive(Debug, PartialEq, Eq, Clone)] @@ -258,6 +268,7 @@ impl SysMap { xml_sdf: &SystemDescriptionFile, node: &dyn SdfNode, allow_setvar: bool, + allow_delegation: bool, max_vaddr: u64, ) -> Result { let mut attrs = vec!["mr", "vaddr", "perms", "cached"]; @@ -266,6 +277,9 @@ impl SysMap { attrs.push("setvar_size"); attrs.push("setvar_prefill_size"); } + if allow_delegation { + attrs.push("delegated"); + } check_attributes(xml_sdf, node, &attrs)?; let mr = checked_lookup(xml_sdf, node, "mr")?.to_string(); @@ -320,11 +334,27 @@ impl SysMap { true }; + let delegated = if let Some(xml_delegated) = node.attribute("delegated") { + match str_to_bool(xml_delegated) { + Some(val) => val, + None => { + return Err(value_error( + xml_sdf, + node, + "delegated must be 'true' or 'false'".to_string(), + )) + } + } + } else { + false + }; + Ok(SysMap { mr, vaddr, perms, cached, + delegated, text_pos: Some(node.range().start), }) } diff --git a/tool/microkit/src/sdf/pd_vm.rs b/tool/microkit/src/sdf/pd_vm.rs index 5ec6f5570..4ae2b3961 100644 --- a/tool/microkit/src/sdf/pd_vm.rs +++ b/tool/microkit/src/sdf/pd_vm.rs @@ -16,8 +16,8 @@ use super::irq::{SysIrq, SysIrqKind}; use super::memory_region::SysMap; use super::pci::PciDevice; use super::util::{ - check_attributes, checked_add_setvar, checked_lookup, ensure_setvar_allowed, loc_string, - sdf_parse_number, value_error, + check_attributes, checked_add_setvar, checked_lookup, ensure_delegation_allowed, + ensure_setvar_allowed, loc_string, sdf_parse_number, value_error, }; use super::{SdfLocation, SdfNode, SystemDescriptionFile}; @@ -47,6 +47,7 @@ pub struct IOPort { pub addr: u64, pub size: u64, pub text_pos: SdfLocation, + pub delegated: bool, } #[derive(Debug, PartialEq, Eq)] @@ -83,6 +84,8 @@ pub struct ProtectionDomain { pub sched_params: SchedulingParams, pub passive: bool, pub stack_size: u64, + pub delegatee: bool, + pub allow_delegation: bool, pub smc: bool, pub cpu: CpuCore, pub domain: Option, @@ -148,6 +151,7 @@ impl ProtectionDomain { xml_sdf: &SystemDescriptionFile, node: &dyn SdfNode, role: ProtectionDomainRole, + allow_delegation: bool, domains: &Domains, ) -> Result { let mut attrs = vec![ @@ -157,6 +161,8 @@ impl ProtectionDomain { "period", "passive", "stack_size", + "delegatee", + "allow_delegation", // The SMC field is only available in certain configurations // but we do the error-checking further down. "smc", @@ -175,6 +181,15 @@ impl ProtectionDomain { } ProtectionDomainRole::Normal => {} } + + if allow_delegation && role == ProtectionDomainRole::Normal { + return Err(value_error( + xml_sdf, + node, + "Resource delegation is not allowed to a PD without a parent.".to_string(), + )); + }; + check_attributes(xml_sdf, node, &attrs)?; let name = checked_lookup(xml_sdf, node, "name")?.to_string(); @@ -252,6 +267,33 @@ impl ProtectionDomain { )); } + let delegatee = if let Some(xml_delegatee) = node.attribute("delegatee") { + match str_to_bool(xml_delegatee) { + Some(val) => val, + None => { + return Err(value_error( + xml_sdf, + node, + "delegatee must be 'true' or 'false'".to_string(), + )) + } + } + } else { + false + }; + // + // If a protection domain is a 'delegatee', it will receive the ability + // to access (some) resources of a 'delegator' pd, which should be set + // to be the child/template pds of the delegatee. + // + if delegatee && role != ProtectionDomainRole::Normal { + return Err(value_error( + xml_sdf, + node, + "A child/template PD cannot be a delegatee".to_string(), + )); + } + let stack_size = if let Some(xml_stack_size) = node.attribute("stack_size") { sdf_parse_number(xml_stack_size, node)? } else { @@ -420,8 +462,13 @@ impl ProtectionDomain { child.attribute("path_for_symbols").map(PathBuf::from); } "map" => { + if child.attribute("delegated").is_some() { + ensure_delegation_allowed(allow_delegation, xml_sdf, &*child)?; + }; + let map_max_vaddr = config.pd_map_max_vaddr(stack_size); - let map = SysMap::from_xml(xml_sdf, &*child, true, map_max_vaddr)?; + let map = + SysMap::from_xml(xml_sdf, &*child, true, allow_delegation, map_max_vaddr)?; if let Some(setvar_vaddr) = child.attribute("setvar_vaddr") { ensure_setvar_allowed(role.clone(), sym_emit, xml_sdf, &*child)?; @@ -467,6 +514,24 @@ impl ProtectionDomain { return Err(value_error(xml_sdf, &*child, "id must be >= 0".to_string())); } + if child.attribute("delegated").is_some() { + ensure_delegation_allowed(allow_delegation, xml_sdf, &*child)?; + }; + let delegated = if let Some(xml_delegated) = node.attribute("delegated") { + match str_to_bool(xml_delegated) { + Some(val) => val, + None => { + return Err(value_error( + xml_sdf, + node, + "delegated must be 'true' or 'false'".to_string(), + )) + } + } + } else { + false + }; + if let Some(setvar_id) = child.attribute("setvar_id") { ensure_setvar_allowed(role.clone(), sym_emit, xml_sdf, &*child)?; let setvar = SysSetVar { @@ -507,6 +572,7 @@ impl ProtectionDomain { let irq = SysIrq { id: id as u64, kind: SysIrqKind::Conventional { irq, trigger }, + delegated, }; irqs.push(irq); } else if let Some(pin_str) = child.attribute("pin") { @@ -608,6 +674,7 @@ impl ProtectionDomain { polarity, vector: vector as u64, }, + delegated, }; irqs.push(irq); } else if let Some(pcidev_str) = child.attribute("pcidev") { @@ -658,6 +725,7 @@ impl ProtectionDomain { handle: handle as u64, vector: vector as u64, }, + delegated, }; irqs.push(irq); } else { @@ -679,8 +747,32 @@ impl ProtectionDomain { check_attributes( xml_sdf, &*child, - &["id", "setvar_id", "setvar_addr", "addr", "size"], + &[ + "id", + "setvar_id", + "setvar_addr", + "addr", + "size", + "delegated", + ], )?; + if child.attribute("delegated").is_some() { + ensure_delegation_allowed(allow_delegation, xml_sdf, &*child)?; + }; + let delegated = if let Some(xml_delegated) = node.attribute("delegated") { + match str_to_bool(xml_delegated) { + Some(val) => val, + None => { + return Err(value_error( + xml_sdf, + node, + "delegated must be 'true' or 'false'".to_string(), + )) + } + } + } else { + false + }; let id = checked_lookup(xml_sdf, &*child, "id")? .parse::() @@ -737,6 +829,7 @@ impl ProtectionDomain { addr, size: size as u64, text_pos: node.range().start, + delegated, }) } else { return Err(value_error( @@ -769,11 +862,15 @@ impl ProtectionDomain { )); } + // if the 'delegatee' attribute is set and valid, + // child PDs are allowed to delegate their 'delegated' caps + let delegation: bool = delegatee; let child_pd = ProtectionDomain::from_xml( config, xml_sdf, &*child, ProtectionDomainRole::Child, + delegation, domains, )?; @@ -799,11 +896,15 @@ impl ProtectionDomain { )); } + // if the 'delegatee' attribute is set and valid, + // child PDs are allowed to delegate their 'delegated' caps + let delegation: bool = delegatee; let child_pd = ProtectionDomain::from_xml( config, xml_sdf, &*child, ProtectionDomainRole::Template, + delegation, domains, )?; @@ -855,7 +956,7 @@ impl ProtectionDomain { )); } - cspace = Some(CSpace::from_xml(xml_sdf, &*child)?); + cspace = Some(CSpace::from_xml(xml_sdf, &*child, delegatee)?); } _ => { let pos = child.range().start; @@ -888,6 +989,8 @@ impl ProtectionDomain { }, passive, stack_size, + delegatee, + allow_delegation, smc, cpu, domain, @@ -1111,7 +1214,13 @@ impl VirtualMachine { "map" => { // Virtual machines do not have program images and so we do not allow // setvar_vaddr on SysMap - let map = SysMap::from_xml(xml_sdf, &*child, false, config.vm_map_max_vaddr())?; + let map = SysMap::from_xml( + xml_sdf, + &*child, + false, + false, + config.vm_map_max_vaddr(), + )?; maps.push(map); } _ => { diff --git a/tool/microkit/src/sdf/util.rs b/tool/microkit/src/sdf/util.rs index bd708b90c..bc9e7976c 100644 --- a/tool/microkit/src/sdf/util.rs +++ b/tool/microkit/src/sdf/util.rs @@ -89,6 +89,22 @@ pub fn ensure_setvar_allowed( Ok(()) } +pub fn ensure_delegation_allowed( + allow_delegation: bool, + xml_sdf: &SystemDescriptionFile<'_>, + node: &dyn SdfNode, +) -> Result<(), String> { + if !allow_delegation { + return Err(value_error( + xml_sdf, + node, + "'delegated' is not allowed within this PD".to_string(), + )); + } + + Ok(()) +} + pub fn check_no_text( xml_sdf: &SystemDescriptionFile, node: &roxmltree::Node, diff --git a/tool/microkit/tests/sdf/pd_delegate_child_as_delegatee.system b/tool/microkit/tests/sdf/pd_delegate_child_as_delegatee.system new file mode 100644 index 000000000..bf45b80d0 --- /dev/null +++ b/tool/microkit/tests/sdf/pd_delegate_child_as_delegatee.system @@ -0,0 +1,16 @@ + + + + + + + + + + + + \ No newline at end of file diff --git a/tool/microkit/tests/sdf/pd_delegate_invalid_channel.system b/tool/microkit/tests/sdf/pd_delegate_invalid_channel.system new file mode 100644 index 000000000..5bf8ee8d0 --- /dev/null +++ b/tool/microkit/tests/sdf/pd_delegate_invalid_channel.system @@ -0,0 +1,24 @@ + + + + + + + + + + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_delegate_invalid_ioport.system b/tool/microkit/tests/sdf/pd_delegate_invalid_ioport.system new file mode 100644 index 000000000..a374b80ca --- /dev/null +++ b/tool/microkit/tests/sdf/pd_delegate_invalid_ioport.system @@ -0,0 +1,16 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_delegate_invalid_irq.system b/tool/microkit/tests/sdf/pd_delegate_invalid_irq.system new file mode 100644 index 000000000..16f7c05aa --- /dev/null +++ b/tool/microkit/tests/sdf/pd_delegate_invalid_irq.system @@ -0,0 +1,16 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/sdf/pd_delegate_invalid_map.system b/tool/microkit/tests/sdf/pd_delegate_invalid_map.system new file mode 100644 index 000000000..0aa63cd33 --- /dev/null +++ b/tool/microkit/tests/sdf/pd_delegate_invalid_map.system @@ -0,0 +1,18 @@ + + + + + + + + + + + + \ No newline at end of file diff --git a/tool/microkit/tests/sdf/pd_delegate_without_delegatee.system b/tool/microkit/tests/sdf/pd_delegate_without_delegatee.system new file mode 100644 index 000000000..d4fbec85e --- /dev/null +++ b/tool/microkit/tests/sdf/pd_delegate_without_delegatee.system @@ -0,0 +1,14 @@ + + + + + + + + + + diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 0363d43b5..b78b52faa 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -781,6 +781,60 @@ mod protection_domain { ) } + #[test] + fn test_delegate_without_delegatee() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_delegate_without_delegatee.system", + "Error: 'delegated' is not allowed within this PD on element 'map':", + ) + } + + #[test] + fn test_delegate_invalid_map() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_delegate_invalid_map.system", + "Error: 'delegated' is not allowed within this PD on element 'map':", + ) + } + + #[test] + fn test_delegate_child_as_delegatee() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_delegate_child_as_delegatee.system", + "Error: A child/template PD cannot be a delegatee on element 'protection_domain':", + ) + } + + #[test] + fn test_delegate_invalid_channel() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_delegate_invalid_channel.system", + "Error: 'delegated' is not allowed within this PD on element 'end':", + ) + } + + #[test] + fn test_delegate_invalid_irq() { + check_error( + &DEFAULT_AARCH64_KERNEL_CONFIG, + "pd_delegate_invalid_irq.system", + "Error: 'Delegated' is not allowed within this PD on element 'irq':", + ) + } + + #[test] + fn test_delegate_invalid_ioport() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "pd_delegate_invalid_ioport.system", + "Error: 'delegated' is not allowed within this PD on element 'ioport':", + ) + } + #[test] fn test_template_has_image() { check_error( From 868ca6af06df153ddeb316b9e5c041ec8552261a Mon Sep 17 00:00:00 2001 From: Guangtao Zhu Date: Mon, 10 Aug 2026 01:03:13 +1000 Subject: [PATCH 2/8] cap_delegete: add case for delegated frame mapping Signed-off-by: Guangtao Zhu --- example/cap_delegate/README.md | 6 ++ example/cap_delegate/cap_delegate.system | 2 + example/cap_delegate/delegatee.c | 99 ++++++++++++++++++++++++ example/cap_delegate/delegation.h | 29 +++++++ example/cap_delegate/delegator.c | 21 +++++ 5 files changed, 157 insertions(+) diff --git a/example/cap_delegate/README.md b/example/cap_delegate/README.md index 09709c82b..17ff8afb9 100644 --- a/example/cap_delegate/README.md +++ b/example/cap_delegate/README.md @@ -428,4 +428,10 @@ MON|INFO: Microkit Monitor started! ::notified: received signal from delegatee ::notified: try notifying server <> + access delegated MR +[delegatee] fault from child 0 +[delegatee] VM fault address: 0x0000000000c00000 +[delegatee] map delegated frame +[delegatee] delegated MR mapped + delegated MR mapped, value: 0x0000000012345678 ``` diff --git a/example/cap_delegate/cap_delegate.system b/example/cap_delegate/cap_delegate.system index b155eb4a4..d56672257 100644 --- a/example/cap_delegate/cap_delegate.system +++ b/example/cap_delegate/cap_delegate.system @@ -5,12 +5,14 @@ SPDX-License-Identifier: BSD-2-Clause --> + + diff --git a/example/cap_delegate/delegatee.c b/example/cap_delegate/delegatee.c index 53e04876c..ab752389b 100644 --- a/example/cap_delegate/delegatee.c +++ b/example/cap_delegate/delegatee.c @@ -11,6 +11,43 @@ #define CPTR_DGT_CND \ (microkit_cspace_root_slot_to_cptr(48)) +#define CHILD_DELEGATOR ((microkit_child)0) + +#define DELEGATED_MR_VADDR 0xC00000 +#define DELEGATED_MR_SIZE 0x1000 + +static seL4_Error map_delegated_page(seL4_CPtr frame, seL4_CPtr vspace, seL4_Word vaddr) +{ +#if defined(CONFIG_ARCH_AARCH64) + return seL4_ARM_Page_Map( + frame, + vspace, + vaddr, + seL4_ReadWrite, + seL4_ARM_Default_VMAttributes + ); +#elif defined(CONFIG_ARCH_RISCV) + return seL4_RISCV_Page_Map( + frame, + vspace, + vaddr, + seL4_ReadWrite, + seL4_RISCV_Default_VMAttributes + ); +#elif defined(CONFIG_ARCH_X86_64) + return seL4_X86_Page_Map( + frame, + vspace, + vaddr, + seL4_ReadWrite, + seL4_X86_Default_VMAttributes + ); +#else +#error "Unsupported architecture" +#endif +} + + void init(void) { microkit_dbg_puts("[delegatee] init\n"); @@ -118,3 +155,65 @@ seL4_MessageInfo_t protected(microkit_channel ch, microkit_msginfo msginfo) return microkit_msginfo_new(0, 0); } + +seL4_Bool fault(microkit_child child, microkit_msginfo msginfo, microkit_msginfo *reply_msginfo) +{ + seL4_Word label = microkit_msginfo_get_label(msginfo); + + microkit_dbg_puts("[delegatee] fault from child "); + microkit_dbg_put32(child); + microkit_dbg_puts("\n"); + + if (child != CHILD_DELEGATOR) { + microkit_dbg_puts("[delegatee] unexpected child\n"); + return seL4_False; + } + + if (label != seL4_Fault_VMFault) { + microkit_dbg_puts("[delegatee] unexpected fault type\n"); + return seL4_False; + } + + seL4_Word fault_addr = seL4_GetMR(seL4_VMFault_Addr); + + microkit_dbg_puts("[delegatee] VM fault address: "); + puthex64(fault_addr); + microkit_dbg_puts("\n"); + + if (fault_addr < DELEGATED_MR_VADDR || + fault_addr >= DELEGATED_MR_VADDR + DELEGATED_MR_SIZE) { + microkit_dbg_puts("[delegatee] fault outside delegated MR\n"); + return seL4_False; + } + + // delegation CNode[4] -> delegator VSpace + seL4_CPtr vspace = + DGT_CPTR__DGTR_VSPACE(CPTR_DGT_CND); + + // delegation CNode[138] -> first frame of delegated MR + seL4_CPtr frame = + DGT_CPTR__MR_FRAME(CPTR_DGT_CND, 0); + + microkit_dbg_puts("[delegatee] map delegated frame\n"); + + seL4_Error err = map_delegated_page( + frame, + vspace, + DELEGATED_MR_VADDR + ); + + if (err != seL4_NoError) { + microkit_dbg_puts("[delegatee] Page_Map failed: "); + microkit_dbg_put32(err); + microkit_dbg_puts("\n"); + return seL4_False; + } + + microkit_dbg_puts("[delegatee] delegated MR mapped\n"); + + *reply_msginfo = microkit_msginfo_new(0, 0); + + // Reply to the fault. The delegator resumes from the fault restart PC, + // so the faulting memory access is retried. + return seL4_True; +} diff --git a/example/cap_delegate/delegation.h b/example/cap_delegate/delegation.h index 7f06a986d..b092c95ec 100644 --- a/example/cap_delegate/delegation.h +++ b/example/cap_delegate/delegation.h @@ -28,6 +28,16 @@ #define DELEGATION_SLOT_MICROKIT_CNODE 1 #define DELEGATION_SLOT_ROOT_CNODE 2 #define DELEGATION_SLOT_GRANT_CAP 3 +#define DELEGATION_SLOT_VSPACE 4 + +// Must match DLG_MR_CAP in builder.rs. +#define DELEGATION_BASE_MR_CAP (10 + 64 + 64) + +#define DGT_CPTR__DGTR_VSPACE(CPTR_DGT_CND) \ + ((CPTR_DGT_CND) | DELEGATION_SLOT_VSPACE) + +#define DGT_CPTR__MR_FRAME(CPTR_DGT_CND, IDX) \ + ((CPTR_DGT_CND) | (DELEGATION_BASE_MR_CAP + (IDX))) // Delegator PD's Microkit CNode, accessible through the delegation CNode. #define DGT_CPTR__DGTR_MK_CND(CPTR_DGT_CND) \ @@ -36,3 +46,22 @@ // Delegator PD's root CNode, accessible through the delegation CNode. #define DGT_CPTR__DGTR_ROOT_CND(CPTR_DGT_CND) \ (CPTR_DGT_CND | DELEGATION_SLOT_ROOT_CNODE) + +static inline char hexchar(unsigned int v) +{ + return v < 10 ? '0' + v : ('a' - 10) + v; +} + +/* stolen from monitor/src/util.c */ +static inline void puthex64(seL4_Uint64 val) +{ + char buffer[16 + 3]; + buffer[0] = '0'; + buffer[1] = 'x'; + buffer[16 + 3 - 1] = 0; + for (unsigned i = 16 + 1; i > 1; i--) { + buffer[i] = hexchar(val & 0xf); + val >>= 4; + } + microkit_dbg_puts(buffer); +} diff --git a/example/cap_delegate/delegator.c b/example/cap_delegate/delegator.c index 5b3219393..5cb5ededd 100644 --- a/example/cap_delegate/delegator.c +++ b/example/cap_delegate/delegator.c @@ -14,6 +14,25 @@ typedef void (*entry_t)(void); +#define DELEGATED_MR_VADDR 0xC00000 + +static void delegated_mr_test(void) +{ + volatile seL4_Word *mr = (volatile seL4_Word *)DELEGATED_MR_VADDR; + + microkit_dbg_puts(" access delegated MR\n"); + + // This store should fault the first time. + // + // The delegatee maps the delegated frame and replies to the fault. + // The instruction is then restarted and this store succeeds. + *mr = 0x12345678; + + microkit_dbg_puts(" delegated MR mapped, value: "); + puthex64(*mr); + microkit_dbg_puts("\n"); +} + static void delegation_restore_cap(seL4_Word slot) { microkit_dbg_puts(" restore cap: "); @@ -216,4 +235,6 @@ void notified(microkit_channel ch) microkit_dbg_puts("::notified: received signal from delegatee\n"); microkit_dbg_puts("::notified: try notifying server\n"); microkit_notify(CH_SERVER); + + delegated_mr_test(); } From a8d1740395b161bc8af455ddcd86f55b6ffba455 Mon Sep 17 00:00:00 2001 From: Guangtao Zhu Date: Mon, 10 Aug 2026 10:58:05 +1000 Subject: [PATCH 3/8] sdf: stop supporting delegated IRQs Delegating an IRQ capability to another PD is of limited use because an IRQ handler is configured to signal a notification associated with the original PD. Delegating the IRQ alone would therefore leave an implicit dependency on the notification capability. Supporting this properly would require delegating or otherwise managing that notification as well. For now, reject delegated IRQs rather than introducing this implicit dependency. Signed-off-by: Guangtao Zhu --- tool/microkit/src/sdf/irq.rs | 1 - tool/microkit/src/sdf/pd_vm.rs | 23 +++++------------------ tool/microkit/tests/test.rs | 2 +- 3 files changed, 6 insertions(+), 20 deletions(-) diff --git a/tool/microkit/src/sdf/irq.rs b/tool/microkit/src/sdf/irq.rs index 552261b00..56dc2c7a7 100644 --- a/tool/microkit/src/sdf/irq.rs +++ b/tool/microkit/src/sdf/irq.rs @@ -35,7 +35,6 @@ pub enum SysIrqKind { pub struct SysIrq { pub id: u64, pub kind: SysIrqKind, - pub delegated: bool, } impl SysIrq { diff --git a/tool/microkit/src/sdf/pd_vm.rs b/tool/microkit/src/sdf/pd_vm.rs index 4ae2b3961..358d26699 100644 --- a/tool/microkit/src/sdf/pd_vm.rs +++ b/tool/microkit/src/sdf/pd_vm.rs @@ -515,21 +515,11 @@ impl ProtectionDomain { } if child.attribute("delegated").is_some() { - ensure_delegation_allowed(allow_delegation, xml_sdf, &*child)?; - }; - let delegated = if let Some(xml_delegated) = node.attribute("delegated") { - match str_to_bool(xml_delegated) { - Some(val) => val, - None => { - return Err(value_error( - xml_sdf, - node, - "delegated must be 'true' or 'false'".to_string(), - )) - } - } - } else { - false + return Err(value_error( + xml_sdf, + &*child, + "IRQ delegation is not supported".to_string(), + )); }; if let Some(setvar_id) = child.attribute("setvar_id") { @@ -572,7 +562,6 @@ impl ProtectionDomain { let irq = SysIrq { id: id as u64, kind: SysIrqKind::Conventional { irq, trigger }, - delegated, }; irqs.push(irq); } else if let Some(pin_str) = child.attribute("pin") { @@ -674,7 +663,6 @@ impl ProtectionDomain { polarity, vector: vector as u64, }, - delegated, }; irqs.push(irq); } else if let Some(pcidev_str) = child.attribute("pcidev") { @@ -725,7 +713,6 @@ impl ProtectionDomain { handle: handle as u64, vector: vector as u64, }, - delegated, }; irqs.push(irq); } else { diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index b78b52faa..6b00bae5b 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -822,7 +822,7 @@ mod protection_domain { check_error( &DEFAULT_AARCH64_KERNEL_CONFIG, "pd_delegate_invalid_irq.system", - "Error: 'Delegated' is not allowed within this PD on element 'irq':", + "Error: IRQ delegation is not supported on element 'irq':", ) } From 22849cdce3537eb085f5685b0478dac18e943d40 Mon Sep 17 00:00:00 2001 From: Guangtao Zhu Date: Mon, 10 Aug 2026 11:09:59 +1000 Subject: [PATCH 4/8] sdf: support IOPort delegation This commit redirects delegated IOPort caps to the delegation CNode, while normal non-delegated IOPort caps still stay in the microkit CNode. A range limit is also introduced to prevent the delegated MR caps overlap with the IOPort caps in the delegation CNode. Signed-off-by: Guangtao Zhu --- tool/microkit/src/capdl/builder.rs | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index afc2bbd39..8a432bfa4 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -113,6 +113,7 @@ const DLG_CNODE_DGTR_VSPACE_CAP: u32 = 4; const DLG_PPC_CAP: u32 = PD_BASE_OUTPUT_ENDPOINT_CAP as u32; const DLG_MR_CAP: u32 = DLG_PPC_CAP + 64; +const DLG_MR_CAP_END: u32 = PD_BASE_IOPORT_CAP as u32; pub const SLOT_BITS: u64 = 5; pub const SLOT_SIZE: u64 = 1 << SLOT_BITS; @@ -421,7 +422,10 @@ fn map_memory_region( cnode.push(capdl_util_make_cte(*slot, frame_cap)); *slot += 1; - assert!(*slot <= PD_CAP_SIZE); + assert!( + *slot < DLG_MR_CAP_END, + "delegated MR capabilities exceed reserved delegation CNode range" + ); } } Ok(()) @@ -928,10 +932,13 @@ pub fn build_capdl_spec( let ioport_obj_id = capdl_util_make_ioport_obj(&mut spec_container, &pd.name, ioport.addr, ioport.size); let ioport_cap = capdl_util_make_ioport_cap(ioport_obj_id); - caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( - (PD_BASE_IOPORT_CAP + ioport.id) as u32, - ioport_cap, - )); + let ioport_cap_idx = (PD_BASE_IOPORT_CAP + ioport.id) as u32; + if ioport.delegated { + caps_to_insert_to_pd_delegation_cnode + .push(capdl_util_make_cte(ioport_cap_idx, ioport_cap)); + } else { + caps_to_insert_to_pd_cspace.push(capdl_util_make_cte(ioport_cap_idx, ioport_cap)); + } } // Step 3-11 Create VM Spec. From 786fcbee393df502a5599c24bf9b1426bfb2afa7 Mon Sep 17 00:00:00 2001 From: Guangtao Zhu Date: Mon, 10 Aug 2026 12:44:39 +1000 Subject: [PATCH 5/8] docs: add capability delegation Signed-off-by: Guangtao Zhu --- docs/manual.md | 106 ++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 104 insertions(+), 2 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index 2186004c1..26ef0c2dd 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -109,6 +109,7 @@ This document attempts to clearly describe all of these terms, however as the co * [interrupt](#irq) * [fault](#fault) * [ioport](#ioport) +* [capability delegation](#delegation) * [IO address space](#io_address_space) * [domain scheduling](#domains) @@ -385,6 +386,24 @@ delivered to another PD, the fault being handled depends on when the parent PD i I/O ports are x86 mechanisms to access certain physical devices (e.g. PC serial ports or PCI) using the `in` and `out` CPU instructions. The system description specifies if a protection domain have access to certain port address ranges. These accesses will be executed by seL4 and the result returned to protection domains. +## Capability Delegation {#delegation} + +Capability delegation allows a parent protection domain to control when selected resources of one of its direct child protection domains become available at runtime. + +A parent PD that manages delegated resources is called a *delegatee*. A direct child PD whose resources are managed by that delegatee is called a *delegator*. Together, the two PDs form a *delegatee-delegator pair*. + +Resources selected for delegation are not initially installed in the delegator's CSpace. Instead, the Microkit tool places the corresponding capabilities in a *delegation CNode* associated with the delegatee-delegator pair. The delegatee can then use these capabilities to make the resources available to the delegator at runtime. + +Capability delegation is supported for: + +* channel ends; +* memory-region mappings; +* x86 I/O ports. + +IRQ delegation is not supported. + +See the [`protection_domain`](#sysdesc) and [`channel`](#sysdesc) System Description File sections for the corresponding `delegatee` and `delegated` attributes. The `cap_delegate` example in the SDK demonstrates capability delegation. + ## IO Address Spaces {#io_address_space} IO Address Spaces provide a way to isolate device memory accesses within a fixed virtual address space. The isolation provided by the address space is enforced by the underlying hardware IOMMU or SMMU. @@ -1039,6 +1058,7 @@ It supports the following attributes: * `domain`: (conditionally required) the name of the domain that this PD belongs to. If a domain schedule is specified, this is mandatory, else it is disallowed. * `sym_emit`: (optional) Emit the resolved symbol patches for this PD to `symbols/.mktsym`. Defaults to false. +* `delegatee`: (optional) Indicates that the PD can manage delegated capabilities for its child PDs (delegators). Defaults to false. A delegatee can manage at most 16 delegators. Additionally, it supports the following child elements: @@ -1064,11 +1084,15 @@ The `map` element has the following attributes: * `vaddr`: Identifies the virtual address at which to map the memory region. * `perms`: Identifies the permissions with which to map the memory region. Can be a combination of `r` (read), `w` (write), and `x` (eXecute), with the exception of a write-only mapping (just `w`). Defaults to read-write. +* `delegated`: (optional) Indicates that the memory region mapping is delegated. This is only valid for a map belonging to a child of a PD with `delegatee="true"`. For a delegated map, the frames (of this memory region) are not initially mapped into the delegator's VSpace; the corresponding frame capabilities are instead placed in the delegation CNode so that the delegatee can establish the mapping at runtime. (However, the pagetable structure for establishing the delegated maps is populated, same as non-delegated maps). + Defaults to false. * `cached`: (optional) Determines if mapped with caching enabled or disabled. Defaults to `true`. * `setvar_vaddr`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the virtual address of the memory region. * `setvar_size`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the size of the memory region. * `setvar_prefill_size`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the size of the prefilled data. +The `irq` element does not support capability delegation. Specifying a `delegated` attribute on an `irq` element is an error. + The `irq` element has the following attributes on ARM and RISC-V: * `irq`: The hardware interrupt number. @@ -1101,6 +1125,9 @@ The `ioport` element has the following attributes: * `size`: The size in bytes of the I/O port region. * `setvar_id`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the I/O port identifier. * `setvar_addr`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the base address of the I/O port. +* `delegated`: (optional) Indicates that the I/O port capability is delegated. Defaults to false. + This is only valid for an I/O port belonging to a child of a PD with `delegatee="true"`. + A delegated I/O port capability is initially placed in the delegation CNode instead of the delegator's Microkit CNode. The `setvar` element has the following attributes: @@ -1114,6 +1141,8 @@ The `protection_domain` element has the same attributes as any other protection * `id`: The ID of the child for the parent to refer to. * `setvar_id`: (optional) Specifies a symbol in the parent program image. This symbol will be rewritten with the ID of the child. +A direct child of a PD with `delegatee="true"` is a delegator. The parent and child form a delegatee-delegator pair, and Microkit creates one delegation CNode for each such pair. + On x86-64, a PD with a VCPU cannot have child PDs. The `template` element has the same elements as protection domains but not: @@ -1152,7 +1181,38 @@ The `vcpu` element has the following attributes: core of the PD that the virtual machine belongs to. * `setvar_id`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the vCPU identifier. -The `map` element has the same attributes as the protection domain with the exception of `setvar_vaddr`. +The `map` element has the same attributes as the protection domain with the exception of `setvar_vaddr` and `delegated`. Virtual-machine memory-region maps do not support capability delegation. + +### Capability delegation example + +The following example creates one delegatee-delegator pair and delegates a channel end and a memory-region mapping: + +```xml + + + + + + + + + + + + + + + + + + + + + +``` + +The delegated channel capability and the frame capability for `shared` are initially held in the delegation CNode rather than being directly available to `delegator`. + ## `memory_region` @@ -1293,7 +1353,10 @@ The `end` element has the following attributes: On x86-64, PDs with virtual machines cannot receive protected procedure calls. * `notify`: (optional) Indicates that the protection domain for this end can send a notification to the other end; defaults to true. * `setvar_id`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the channel identifier. - +* `delegated`: (optional) Indicates that the capability associated with this channel end is delegated. Defaults to false. + This is only valid when `pd` names a child of a PD with `delegatee="true"`. + The capability is initially placed in the delegation CNode instead of the delegator's (the child PD's) Microkit CNode. + The `id` is passed to the PD in the `notified` and `protected` entry points. The `id` should be passed to the `microkit_notify` and `microkit_ppcall` functions. @@ -2146,3 +2209,42 @@ produces a valid image, there should be no errors upon initialising the system. If there are any errors with configuring the system (e.g running out of memory), they will be caught at build-time. This can only reasonably be done due to the static-architecture of Microkit systems. + +## Capability Delegation CSpace Layout + +Each PD has a two-level CSpace consisting of a root CNode and a Microkit CNode. The root CNode has 64 slots and the Microkit CNode has 512 slots. Slot 0 of the root CNode refers to the Microkit CNode. + +For each delegatee-delegator pair, Microkit creates one 512-slot delegation CNode. The delegatee's root CNode slots 48 through 63 are reserved for capabilities to delegation CNodes (if delegatee="true"). Consequently, a delegatee can manage at most 16 delegators. + +Conceptually: + +```text +Delegatee root CNode +| ++-- slot 0 -> delegatee Microkit CNode +| ++-- slots 48-63 -> delegation CNodes +``` + +A delegation CNode contains capabilities used to manage the relationship as well as the delegated resource capabilities: + +```text +Delegation CNode +| ++-- slot 0 -> self-reference ++-- slot 1 -> delegator Microkit CNode ++-- slot 2 -> delegator root CNode ++-- slot 3 -> delegation CNode cap suitable for granting to the delegator ++-- slot 4 -> delegator VSpace +| ++-- resource slots + +-- delegated channel capabilities + +-- delegated memory-region frame capabilities + +-- delegated I/O port capabilities +``` + +Where a delegated resource already has a normal Microkit CNode slot, such as a channel or I/O port capability, its capability uses the corresponding slot in the delegation CNode. This allows the capability to be copied to the delegator's normal Microkit CNode without changing its Microkit-visible identifier. + +For a delegated memory region map, the Microkit tool creates the paging structures required to reach the mapped virtual-address range but does not install the frame capabilities at the leaf level. The frame capabilities and the delegator VSpace capability are available through the delegation CNode, allowing the delegatee to establish the leaf mappings dynamically, for example in response to a child virtual-memory fault. + +By default the delegatee can access the delegation CNode while the delegator cannot. A delegatee may choose to perform capability operations itself, or may explicitly grant the delegator temporary access to the delegation CNode. The policy and protocol for granting and revoking such access are implemented by the application. From 846a4b9b1b684ee3b65a7598dc74840523c386a7 Mon Sep 17 00:00:00 2001 From: Guangtao Zhu Date: Mon, 10 Aug 2026 12:55:57 +1000 Subject: [PATCH 6/8] cleanup: remove unused attribute for pd_vm & fix ioport delegation Signed-off-by: Guangtao Zhu --- example/cap_delegate/README.md | 6 +----- tool/microkit/src/sdf/pd_vm.rs | 5 ++--- 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/example/cap_delegate/README.md b/example/cap_delegate/README.md index 17ff8afb9..ec7ba3740 100644 --- a/example/cap_delegate/README.md +++ b/example/cap_delegate/README.md @@ -66,11 +66,7 @@ delegated="true" - + diff --git a/tool/microkit/src/sdf/pd_vm.rs b/tool/microkit/src/sdf/pd_vm.rs index 358d26699..0020b5681 100644 --- a/tool/microkit/src/sdf/pd_vm.rs +++ b/tool/microkit/src/sdf/pd_vm.rs @@ -162,7 +162,6 @@ impl ProtectionDomain { "passive", "stack_size", "delegatee", - "allow_delegation", // The SMC field is only available in certain configurations // but we do the error-checking further down. "smc", @@ -746,13 +745,13 @@ impl ProtectionDomain { if child.attribute("delegated").is_some() { ensure_delegation_allowed(allow_delegation, xml_sdf, &*child)?; }; - let delegated = if let Some(xml_delegated) = node.attribute("delegated") { + let delegated = if let Some(xml_delegated) = child.attribute("delegated") { match str_to_bool(xml_delegated) { Some(val) => val, None => { return Err(value_error( xml_sdf, - node, + &*child, "delegated must be 'true' or 'false'".to_string(), )) } From 68bd8bd93c21b236152ab5c63b8aecf5d1cc8cf7 Mon Sep 17 00:00:00 2001 From: Guangtao Zhu Date: Mon, 10 Aug 2026 12:56:32 +1000 Subject: [PATCH 7/8] fix: avoid frame delegation slot collision Signed-off-by: Guangtao Zhu --- tool/microkit/src/capdl/builder.rs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 8a432bfa4..9a25b35f8 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -419,13 +419,12 @@ fn map_memory_region( cur_vaddr += page_sz; if let Some((cnode, slot)) = delegation.as_mut() { - cnode.push(capdl_util_make_cte(*slot, frame_cap)); - - *slot += 1; assert!( *slot < DLG_MR_CAP_END, "delegated MR capabilities exceed reserved delegation CNode range" ); + cnode.push(capdl_util_make_cte(*slot, frame_cap)); + *slot += 1; } } Ok(()) @@ -713,6 +712,7 @@ pub fn build_capdl_spec( } // Step 3-2: Map in all Memory Regions + let mut next_delegated_mr_cap = DLG_MR_CAP; for map in pd.maps.iter() { let frames = &mr_name_to_frames[&map.mr]; // MRs have frames of equal size so just use the first frame's page size. @@ -745,8 +745,12 @@ pub fn build_capdl_spec( page_size_bytes, &pd_elf_spec.address_space, frames, - Some((&mut caps_to_insert_to_pd_delegation_cnode, DLG_MR_CAP)), + Some(( + &mut caps_to_insert_to_pd_delegation_cnode, + next_delegated_mr_cap, + )), )?; + next_delegated_mr_cap += frames.len() as u32; } else { map_memory_region( &mut spec_container, From 011cf9f24376a665bef6cd4430a271b02cea1c0c Mon Sep 17 00:00:00 2001 From: Guangtao Zhu Date: Mon, 10 Aug 2026 15:36:29 +1000 Subject: [PATCH 8/8] sdf: resolve the hard limit for child number of delegatee PDs Previously, a delegatee PD assumes all child PDs as delegators, which restricts the maximal number of children a delegatee PD can have (16). This commit introduces 'allow_delegation' to the delegator PDs, which distinguish the PDs who needs a delegation CNode from other normal PDs. Signed-off-by: Guangtao Zhu --- docs/manual.md | 11 +++-- example/cap_delegate/README.md | 15 ++++-- example/cap_delegate/cap_delegate.system | 2 +- tool/microkit/src/sdf.rs | 2 +- tool/microkit/src/sdf/pd_vm.rs | 46 ++++++++++++++----- .../sdf/pd_delegate_invalid_channel.system | 4 +- .../sdf/pd_delegate_invalid_delegator.system | 11 +++++ .../sdf/pd_delegate_invalid_ioport.system | 4 +- .../tests/sdf/pd_delegate_invalid_irq.system | 4 +- .../tests/sdf/pd_delegate_invalid_map.system | 4 +- .../sdf/pd_delegate_without_delegatee.system | 2 +- tool/microkit/tests/test.rs | 11 ++++- 12 files changed, 83 insertions(+), 33 deletions(-) create mode 100644 tool/microkit/tests/sdf/pd_delegate_invalid_delegator.system diff --git a/docs/manual.md b/docs/manual.md index 26ef0c2dd..270e7742a 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -1059,6 +1059,7 @@ It supports the following attributes: If a domain schedule is specified, this is mandatory, else it is disallowed. * `sym_emit`: (optional) Emit the resolved symbol patches for this PD to `symbols/.mktsym`. Defaults to false. * `delegatee`: (optional) Indicates that the PD can manage delegated capabilities for its child PDs (delegators). Defaults to false. A delegatee can manage at most 16 delegators. +* `allow_delegation`: (optional) Indicates that the PD participates in capability delegation as a delegator. Defaults to false. When enabled, the parent of this PD must be a delegatee. Additionally, it supports the following child elements: @@ -1084,7 +1085,7 @@ The `map` element has the following attributes: * `vaddr`: Identifies the virtual address at which to map the memory region. * `perms`: Identifies the permissions with which to map the memory region. Can be a combination of `r` (read), `w` (write), and `x` (eXecute), with the exception of a write-only mapping (just `w`). Defaults to read-write. -* `delegated`: (optional) Indicates that the memory region mapping is delegated. This is only valid for a map belonging to a child of a PD with `delegatee="true"`. For a delegated map, the frames (of this memory region) are not initially mapped into the delegator's VSpace; the corresponding frame capabilities are instead placed in the delegation CNode so that the delegatee can establish the mapping at runtime. (However, the pagetable structure for establishing the delegated maps is populated, same as non-delegated maps). +* `delegated`: (optional) Indicates that the memory region mapping is delegated. This is only valid for a map belonging to a PD with `allow_delegation="true"`, who is also a child of a PD with `delegatee="true"`. For a delegated map, the frames (of this memory region) are not initially mapped into the delegator's VSpace; the corresponding frame capabilities are instead placed in the delegation CNode so that the delegatee can establish the mapping at runtime. (However, the pagetable structure for establishing the delegated maps is populated, same as non-delegated maps). Defaults to false. * `cached`: (optional) Determines if mapped with caching enabled or disabled. Defaults to `true`. * `setvar_vaddr`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the virtual address of the memory region. @@ -1126,7 +1127,7 @@ The `ioport` element has the following attributes: * `setvar_id`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the I/O port identifier. * `setvar_addr`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the base address of the I/O port. * `delegated`: (optional) Indicates that the I/O port capability is delegated. Defaults to false. - This is only valid for an I/O port belonging to a child of a PD with `delegatee="true"`. + This is only valid for an I/O port belonging to a PD with `allow_delegation="true"`, who is also a child of a PD with `delegatee="true"`. A delegated I/O port capability is initially placed in the delegation CNode instead of the delegator's Microkit CNode. The `setvar` element has the following attributes: @@ -1141,7 +1142,7 @@ The `protection_domain` element has the same attributes as any other protection * `id`: The ID of the child for the parent to refer to. * `setvar_id`: (optional) Specifies a symbol in the parent program image. This symbol will be rewritten with the ID of the child. -A direct child of a PD with `delegatee="true"` is a delegator. The parent and child form a delegatee-delegator pair, and Microkit creates one delegation CNode for each such pair. +A direct child of a PD with `delegatee="true"` can opt in to capability delegation with `allow_delegation="true"`. Such a child is a delegator, and Microkit creates one delegation CNode for each delegatee-delegator pair. On x86-64, a PD with a VCPU cannot have child PDs. @@ -1194,7 +1195,7 @@ The following example creates one delegatee-delegator pair and delegates a chann - + @@ -1354,7 +1355,7 @@ The `end` element has the following attributes: * `notify`: (optional) Indicates that the protection domain for this end can send a notification to the other end; defaults to true. * `setvar_id`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the channel identifier. * `delegated`: (optional) Indicates that the capability associated with this channel end is delegated. Defaults to false. - This is only valid when `pd` names a child of a PD with `delegatee="true"`. + This is only valid when `pd` names a PD with `allow_delegation="true"`, who is also a child of a PD with `delegatee="true"`. The capability is initially placed in the delegation CNode instead of the delegator's (the child PD's) Microkit CNode. The `id` is passed to the PD in the `notified` and `protected` entry points. diff --git a/example/cap_delegate/README.md b/example/cap_delegate/README.md index ec7ba3740..401d6b3de 100644 --- a/example/cap_delegate/README.md +++ b/example/cap_delegate/README.md @@ -1,6 +1,6 @@ # Capability Delegation -Capability delegation allows a parent protection domain (the **delegatee**) to dynamically control a subset of capabilities associated with one of its child protection domains (the **delegator**). +Capability delegation allows a parent protection domain (the **delegatee**) to dynamically control a subset of capabilities associated with one of its participating child protection domains (the **delegator**). Instead of installing every capability directly into the delegator PD's CSpace, capabilities marked as *delegated="true"* are placed into a separate **delegation CNode**. The delegation CNode is controlled by the delegatee PD and represents the delegation relationship between one delegatee-delegator pair. @@ -54,7 +54,14 @@ A protection domain that manages delegated capabilities is marked with: delegatee="true" ``` -A child PD that is permitted to participate in delegation contains resources that are marked as delegated. For example, a channel end or a memory region can use: +A child PD that participates in capability delegation is marked with: + +```xml +allow_delegation="true" +``` +Resources associated with the delegator can then be marked as delegated. + +For example, a channel end or a memory-region mapping can use: ```xml delegated="true" @@ -66,7 +73,7 @@ delegated="true" - + @@ -353,7 +360,7 @@ server There is a notification channel between `delegator` and `server`. -The delegator's channel end is marked: +The delegator (child) PD is configured with `allow_delegation="true"`, and its channel end is marked: ```xml delegated="true" diff --git a/example/cap_delegate/cap_delegate.system b/example/cap_delegate/cap_delegate.system index d56672257..5844da236 100644 --- a/example/cap_delegate/cap_delegate.system +++ b/example/cap_delegate/cap_delegate.system @@ -10,7 +10,7 @@ - + diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 47283da82..3d7f5031e 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -183,7 +183,7 @@ pub fn parse( &xml_sdf, &*child, ProtectionDomainRole::Normal, - false, /* top-level PDs are not allowed to delegate cap controls */ + false, /* top-level PDs have no delegatee */ &domains, )?), "channel" => channel_nodes.push(child), diff --git a/tool/microkit/src/sdf/pd_vm.rs b/tool/microkit/src/sdf/pd_vm.rs index 0020b5681..177a72558 100644 --- a/tool/microkit/src/sdf/pd_vm.rs +++ b/tool/microkit/src/sdf/pd_vm.rs @@ -151,7 +151,7 @@ impl ProtectionDomain { xml_sdf: &SystemDescriptionFile, node: &dyn SdfNode, role: ProtectionDomainRole, - allow_delegation: bool, + has_delegatee: bool, domains: &Domains, ) -> Result { let mut attrs = vec![ @@ -162,6 +162,7 @@ impl ProtectionDomain { "passive", "stack_size", "delegatee", + "allow_delegation", // The SMC field is only available in certain configurations // but we do the error-checking further down. "smc", @@ -180,16 +181,39 @@ impl ProtectionDomain { } ProtectionDomainRole::Normal => {} } + check_attributes(xml_sdf, node, &attrs)?; - if allow_delegation && role == ProtectionDomainRole::Normal { - return Err(value_error( - xml_sdf, - node, - "Resource delegation is not allowed to a PD without a parent.".to_string(), - )); + let allow_delegation = if let Some(xml_delegation) = node.attribute("allow_delegation") { + match str_to_bool(xml_delegation) { + Some(val) => val, + None => { + return Err(value_error( + xml_sdf, + node, + "allow_delegation must be 'true' or 'false'".to_string(), + )) + } + } + } else { + false }; - check_attributes(xml_sdf, node, &attrs)?; + if allow_delegation { + if role == ProtectionDomainRole::Normal { + return Err(value_error( + xml_sdf, + node, + "Resource delegation is not allowed to a PD without a parent.".to_string(), + )); + } else if !has_delegatee { + return Err(value_error( + xml_sdf, + node, + "Resource delegation is not allowed to the child of a non-delegatee PD" + .to_string(), + )); + } + }; let name = checked_lookup(xml_sdf, node, "name")?.to_string(); @@ -850,13 +874,12 @@ impl ProtectionDomain { // if the 'delegatee' attribute is set and valid, // child PDs are allowed to delegate their 'delegated' caps - let delegation: bool = delegatee; let child_pd = ProtectionDomain::from_xml( config, xml_sdf, &*child, ProtectionDomainRole::Child, - delegation, + delegatee, domains, )?; @@ -884,13 +907,12 @@ impl ProtectionDomain { // if the 'delegatee' attribute is set and valid, // child PDs are allowed to delegate their 'delegated' caps - let delegation: bool = delegatee; let child_pd = ProtectionDomain::from_xml( config, xml_sdf, &*child, ProtectionDomainRole::Template, - delegation, + delegatee, domains, )?; diff --git a/tool/microkit/tests/sdf/pd_delegate_invalid_channel.system b/tool/microkit/tests/sdf/pd_delegate_invalid_channel.system index 5bf8ee8d0..9f61bf1a0 100644 --- a/tool/microkit/tests/sdf/pd_delegate_invalid_channel.system +++ b/tool/microkit/tests/sdf/pd_delegate_invalid_channel.system @@ -6,9 +6,9 @@ --> - + -