diff --git a/repos/base-sel4/src/core/include/platform_pd.h b/repos/base-sel4/src/core/include/platform_pd.h
index 7e8696f50..dd77a78a7 100644
--- a/repos/base-sel4/src/core/include/platform_pd.h
+++ b/repos/base-sel4/src/core/include/platform_pd.h
@@ -37,8 +37,7 @@ class Genode::Platform_pd : public Address_space
 		Page_table_registry _page_table_registry;
 
 		Cap_sel const _page_directory_sel;
-		addr_t        _init_page_directory();
-		addr_t  const _page_directory = _init_page_directory();
+		addr_t  const _page_directory;
 
 		Vm_space _vm_space;
 
@@ -64,6 +63,9 @@ class Genode::Platform_pd : public Address_space
 		Cap_sel alloc_sel();
 		void free_sel(Cap_sel sel);
 
+		addr_t _init_page_directory() const;
+		void   _deinit_page_directory(addr_t) const;
+
 	public:
 
 		/**
diff --git a/repos/base-sel4/src/core/platform_pd.cc b/repos/base-sel4/src/core/platform_pd.cc
index 9d7eb1fb5..5d354b97b 100644
--- a/repos/base-sel4/src/core/platform_pd.cc
+++ b/repos/base-sel4/src/core/platform_pd.cc
@@ -251,4 +251,7 @@ Platform_pd::~Platform_pd()
 
 	_cspace_cnode_1st.destruct(*platform()->ram_alloc(), true);
 	platform_specific()->core_sel_alloc().free(_cspace_cnode_1st.sel());
+
+	_deinit_page_directory(_page_directory);
+	platform_specific()->core_sel_alloc().free(_page_directory_sel);
 }
diff --git a/repos/base-sel4/src/core/spec/arm/platform.cc b/repos/base-sel4/src/core/spec/arm/platform.cc
index 2034cba0a..65a956d6c 100644
--- a/repos/base-sel4/src/core/spec/arm/platform.cc
+++ b/repos/base-sel4/src/core/spec/arm/platform.cc
@@ -74,7 +74,7 @@ void Genode::Platform::_init_core_page_table_registry()
 	log(":phys_mem_16k:     ",  phys_alloc_16k());
 }
 
-Genode::addr_t Genode::Platform_pd::_init_page_directory()
+Genode::addr_t Genode::Platform_pd::_init_page_directory() const
 {
 	/* page directory table contains 4096 elements of 32bits -> 16k required */
 	enum { PAGES_16K = (1UL << Page_directory_kobj::SIZE_LOG2) / 4096 };
@@ -94,3 +94,16 @@ Genode::addr_t Genode::Platform_pd::_init_page_directory()
 
 	return phys_addr;
 }
+
+void Genode::Platform_pd::_deinit_page_directory(addr_t phys_addr) const
+{
+	int ret = seL4_CNode_Delete(seL4_CapInitThreadCNode,
+	                            _page_directory_sel.value(), 32);
+	if (ret != seL4_NoError) {
+		error(__FUNCTION__, ": could not free ASID entry, "
+		      "leaking physical memory ", ret);
+		return;
+	}
+
+	Untyped_memory::free_page(phys_alloc_16k(), phys_addr);
+}
diff --git a/repos/base-sel4/src/core/spec/x86_32/platform_pd.cc b/repos/base-sel4/src/core/spec/x86_32/platform_pd.cc
index 346592450..64a6adb9a 100644
--- a/repos/base-sel4/src/core/spec/x86_32/platform_pd.cc
+++ b/repos/base-sel4/src/core/spec/x86_32/platform_pd.cc
@@ -16,7 +16,7 @@
 
 #include "arch_kernel_object.h"
 
-Genode::addr_t Genode::Platform_pd::_init_page_directory()
+Genode::addr_t Genode::Platform_pd::_init_page_directory() const
 {
 	addr_t const phys_addr = Untyped_memory::alloc_page(*platform()->ram_alloc());
 	seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value();
@@ -33,3 +33,16 @@ Genode::addr_t Genode::Platform_pd::_init_page_directory()
 
 	return phys_addr;
 }
+
+void Genode::Platform_pd::_deinit_page_directory(addr_t phys_addr) const
+{
+	int ret = seL4_CNode_Delete(seL4_CapInitThreadCNode,
+	                            _page_directory_sel.value(), 32);
+	if (ret != seL4_NoError) {
+		error(__FUNCTION__, ": could not free ASID entry, "
+		      "leaking physical memory ", ret);
+		return;
+	}
+
+	Untyped_memory::free_page(*platform()->ram_alloc(), phys_addr);
+}
diff --git a/repos/base-sel4/src/core/spec/x86_64/platform_pd.cc b/repos/base-sel4/src/core/spec/x86_64/platform_pd.cc
index d5b189ab1..b7f9104a5 100644
--- a/repos/base-sel4/src/core/spec/x86_64/platform_pd.cc
+++ b/repos/base-sel4/src/core/spec/x86_64/platform_pd.cc
@@ -16,7 +16,7 @@
 
 #include "arch_kernel_object.h"
 
-Genode::addr_t Genode::Platform_pd::_init_page_directory()
+Genode::addr_t Genode::Platform_pd::_init_page_directory() const
 {
 	addr_t const phys_addr = Untyped_memory::alloc_page(*platform()->ram_alloc());
 	seL4_Untyped const service = Untyped_memory::untyped_sel(phys_addr).value();
@@ -32,3 +32,16 @@ Genode::addr_t Genode::Platform_pd::_init_page_directory()
 
 	return phys_addr;
 }
+
+void Genode::Platform_pd::_deinit_page_directory(addr_t phys_addr) const
+{
+	int ret = seL4_CNode_Delete(seL4_CapInitThreadCNode,
+	                            _page_directory_sel.value(), 32);
+	if (ret != seL4_NoError) {
+		error(__FUNCTION__, ": could not free ASID entry, "
+		      "leaking physical memory ", ret);
+		return;
+	}
+
+	Untyped_memory::free_page(*platform()->ram_alloc(), phys_addr);
+}