diff --git a/repos/base-sel4/src/core/include/cnode.h b/repos/base-sel4/src/core/include/cnode.h
index 27a4db2f4e..ee113a6a66 100644
--- a/repos/base-sel4/src/core/include/cnode.h
+++ b/repos/base-sel4/src/core/include/cnode.h
@@ -164,7 +164,7 @@ class Genode::Cnode : public Cnode_base, Noncopyable
 			create<Cnode_kobj>(untyped_pool, parent_sel, dst_idx, size_log2);
 		}
 
-		void destruct(Range_allocator &phys_alloc)
+		void destruct(Range_allocator &phys_alloc, bool revoke = false)
 		{
 			/* revert phys allocation */
 
@@ -173,6 +173,14 @@ class Genode::Cnode : public Cnode_base, Noncopyable
 				return;
 			}
 
+			if (revoke) {
+				int ret = seL4_CNode_Revoke(seL4_CapInitThreadCNode,
+				                            sel().value(), 32);
+				if (ret)
+					error(__PRETTY_FUNCTION__, ": seL4_CNode_Revoke (",
+					      Hex(sel().value()), ") returned ", ret);
+			}
+
 			int ret = seL4_CNode_Delete(seL4_CapInitThreadCNode,
 			                            sel().value(), 32);
 			if (ret != seL4_NoError)
diff --git a/repos/base-sel4/src/core/platform_pd.cc b/repos/base-sel4/src/core/platform_pd.cc
index e73d8535e3..37648b1bb6 100644
--- a/repos/base-sel4/src/core/platform_pd.cc
+++ b/repos/base-sel4/src/core/platform_pd.cc
@@ -196,11 +196,12 @@ Platform_pd::~Platform_pd()
 {
 	for (unsigned i = 0; i < sizeof(_cspace_cnode_2nd) /
 	                         sizeof(_cspace_cnode_2nd[0]); i++) {
-		_cspace_cnode_2nd[i]->destruct(*platform()->ram_alloc());
+		_cspace_cnode_1st.remove(Cnode_index(i));
+		_cspace_cnode_2nd[i]->destruct(*platform()->ram_alloc(), true);
 		platform_specific()->core_sel_alloc().free(_cspace_cnode_2nd[i]->sel());
 	}
 
-	_cspace_cnode_1st.destruct(*platform()->ram_alloc());
+	_cspace_cnode_1st.destruct(*platform()->ram_alloc(), true);
 	platform_specific()->core_sel_alloc().free(_cspace_cnode_1st.sel());
 
 	/* invalidate weak pointers to this object */