diff --git a/libsel4utils/include/sel4utils/vspace_internal.h b/libsel4utils/include/sel4utils/vspace_internal.h
index f1a391b..47c961f 100644
--- a/libsel4utils/include/sel4utils/vspace_internal.h
+++ b/libsel4utils/include/sel4utils/vspace_internal.h
@@ -434,6 +434,9 @@
                           int cacheable);
 int sel4utils_map_pages_at_vaddr(vspace_t *vspace, seL4_CPtr caps[], uintptr_t cookies[], void *vaddr,
                                  size_t num_pages, size_t size_bits, reservation_t reservation);
+int sel4utils_deferred_rights_map_pages_at_vaddr(vspace_t *vspace, seL4_CPtr caps[], uintptr_t cookies[], void *vaddr,
+                                                 size_t num_pages, size_t size_bits, seL4_CapRights_t rights,
+                                                 reservation_t reservation);
 void sel4utils_unmap_pages(vspace_t *vspace, void *vaddr, size_t num_pages, size_t size_bits, vka_t *vka);
 
 void *sel4utils_new_pages(vspace_t *vspace, seL4_CapRights_t rights,
diff --git a/libsel4utils/src/vspace/bootstrap.c b/libsel4utils/src/vspace/bootstrap.c
index ad06562..99bf5d9 100644
--- a/libsel4utils/src/vspace/bootstrap.c
+++ b/libsel4utils/src/vspace/bootstrap.c
@@ -71,6 +71,7 @@
     vspace->map_pages = sel4utils_map_pages;
     vspace->new_pages_at_vaddr = sel4utils_new_pages_at_vaddr;
     vspace->map_pages_at_vaddr = sel4utils_map_pages_at_vaddr;
+    vspace->deferred_rights_map_pages_at_vaddr = sel4utils_deferred_rights_map_pages_at_vaddr;
     vspace->unmap_pages = sel4utils_unmap_pages;
 
     vspace->reserve_range_aligned = sel4utils_reserve_range_aligned;
diff --git a/libsel4utils/src/vspace/vspace.c b/libsel4utils/src/vspace/vspace.c
index 01254d0..af21c24 100644
--- a/libsel4utils/src/vspace/vspace.c
+++ b/libsel4utils/src/vspace/vspace.c
@@ -357,10 +357,41 @@
         return -1;
     }
 
+    if (res->rights_deferred) {
+        ZF_LOGE("Reservation has no rights associated with it");
+        return -1;
+    }
+
     return map_pages_at_vaddr(vspace, caps, cookies, vaddr, num_pages, size_bits,
                               res->rights, res->cacheable);
 }
 
+int sel4utils_deferred_rights_map_pages_at_vaddr(vspace_t *vspace, seL4_CPtr caps[], uintptr_t cookies[], void *vaddr,
+                                                 size_t num_pages, size_t size_bits,
+                                                 seL4_CapRights_t rights, reservation_t reservation)
+{
+    sel4utils_alloc_data_t *data = get_alloc_data(vspace);
+    sel4utils_res_t *res = reservation_to_res(reservation);
+
+    if (!sel4_valid_size_bits(size_bits)) {
+        ZF_LOGE("Invalid size_bits %zu", size_bits);
+        return -1;
+    }
+
+    if (!check_reservation(data->top_level, res, (uintptr_t) vaddr, (uintptr_t)vaddr + num_pages * BIT(size_bits))) {
+        ZF_LOGE("Invalid reservation");
+        return -1;
+    }
+
+    if (!res->rights_deferred) {
+        ZF_LOGE("Invalid rights: rights already given to reservation");
+        return -1;
+    }
+
+    return map_pages_at_vaddr(vspace, caps, cookies, vaddr, num_pages, size_bits,
+                              rights, res->cacheable);
+}
+
 void *sel4utils_map_pages(vspace_t *vspace, seL4_CPtr caps[], uintptr_t cookies[],
                           seL4_CapRights_t rights, size_t num_pages, size_t size_bits,
                           int cacheable)