diff --git a/apps/sel4test-tests/src/tests/pagetables.c b/apps/sel4test-tests/src/tests/pagetables.c
index 8b1fae3a7..8b94f16f5 100644
--- a/apps/sel4test-tests/src/tests/pagetables.c
+++ b/apps/sel4test-tests/src/tests/pagetables.c
@@ -86,6 +86,9 @@ static int do_test_pagetable_tlbflush_on_vaddr_reuse(env_t env, seL4_CPtr cap1,
     test_error_eq(error, 0);
     test_check(vptr[0] == 1);
 
+    error = seL4_ARM_Page_Unmap(cap1);
+    test_error_eq(error, 0);
+
     error = seL4_ARM_Page_Map(cap2, env->page_directory,
                               vaddr, seL4_AllRights,
                               seL4_ARM_Default_VMAttributes);
@@ -508,3 +511,474 @@ test_pagetable_arm(env_t env)
 DEFINE_TEST(PT0001, "Fun with page tables on ARM", test_pagetable_arm, true)
 #endif /* CONFIG_ARCH_AARCHxx */
 #endif /* CONFIG_ARCH_ARM */
+
+
+#if defined(CONFIG_ARCH_AARCH32)
+static int test_overmap_small(env_t env)
+{
+    seL4_Word map_addr = 0x10000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr pd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageDirectoryObject, 0);
+    seL4_CPtr pt = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageTableObject, 0);
+    seL4_CPtr frame = vka_alloc_object_leaky(&env->vka, seL4_ARM_SmallPageObject, 0);
+    seL4_CPtr frame2 = vka_alloc_object_leaky(&env->vka, seL4_ARM_SmallPageObject, 0);
+    test_assert(pd != 0);
+    test_assert(pt != 0);
+    test_assert(frame != 0);
+    test_assert(frame2 != 0);
+
+    seL4_ARM_ASIDPool_Assign(env->asid_pool, pd);
+
+    /* map page table into page directory */
+    error = seL4_ARM_PageTable_Map(pt, pd, map_addr, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map frame into the page table */
+    error = seL4_ARM_Page_Map(frame, pd, map_addr, seL4_AllRights, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_ARM_Page_Map(frame, pd, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_ARM_Page_Map(frame2, pd, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0011, "Test that overmapping small pages is not permitted", test_overmap_small, true)
+
+static int test_overmap_large(env_t env)
+{
+    seL4_Word map_addr = 0x10000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr pd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageDirectoryObject, 0);
+    seL4_CPtr pt = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageTableObject, 0);
+    seL4_CPtr frame = vka_alloc_object_leaky(&env->vka, seL4_ARM_LargePageObject, 0);
+    seL4_CPtr frame2 = vka_alloc_object_leaky(&env->vka, seL4_ARM_LargePageObject, 0);
+    test_assert(pd != 0);
+    test_assert(pt != 0);
+    test_assert(frame != 0);
+    test_assert(frame2 != 0);
+
+    seL4_ARM_ASIDPool_Assign(env->asid_pool, pd);
+
+    /* map page table into page directory */
+    error = seL4_ARM_PageTable_Map(pt, pd, map_addr, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map frame into the page table */
+    error = seL4_ARM_Page_Map(frame, pd, map_addr, seL4_AllRights, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_ARM_Page_Map(frame, pd, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_ARM_Page_Map(frame2, pd, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0012, "Test that overmapping large pages is not permitted", test_overmap_large, true)
+
+static int test_overmap_section(env_t env)
+{
+    seL4_Word map_addr = 0x10000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr pd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageDirectoryObject, 0);
+    seL4_CPtr section = vka_alloc_object_leaky(&env->vka, seL4_ARM_SectionObject, 0);
+    seL4_CPtr section2 = vka_alloc_object_leaky(&env->vka, seL4_ARM_SectionObject, 0);
+    test_assert(pd != 0);
+    test_assert(section != 0);
+    test_assert(section2 != 0);
+
+    seL4_ARM_ASIDPool_Assign(env->asid_pool, pd);
+
+    /* map frame into the page table */
+    error = seL4_ARM_Page_Map(section, pd, map_addr, seL4_AllRights, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_ARM_Page_Map(section, pd, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_ARM_Page_Map(section2, pd, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0013, "Test that overmapping sections is not permitted", test_overmap_section, true)
+
+static int test_overmap_supersection(env_t env)
+{
+    seL4_Word map_addr = 0x10000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr pd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageDirectoryObject, 0);
+    seL4_CPtr supersection = vka_alloc_object_leaky(&env->vka, seL4_ARM_SuperSectionObject, 0);
+    seL4_CPtr supersection2 = vka_alloc_object_leaky(&env->vka, seL4_ARM_SuperSectionObject, 0);
+    test_assert(pd != 0);
+    test_assert(supersection != 0);
+    test_assert(supersection2 != 0);
+
+    seL4_ARM_ASIDPool_Assign(env->asid_pool, pd);
+
+    /* map frame into the page table */
+    error = seL4_ARM_Page_Map(supersection, pd, map_addr, seL4_AllRights, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_ARM_Page_Map(supersection, pd, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_ARM_Page_Map(supersection2, pd, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0014, "Test that overmapping super sections is not permitted", test_overmap_supersection, true)
+
+#elif defined(CONFIG_ARCH_AARCH64)
+static int test_overmap_small(env_t env)
+{
+    seL4_Word map_addr = 0x10000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr pgd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageGlobalDirectoryObject, 0);
+    seL4_CPtr pud = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageUpperDirectoryObject, 0);
+    seL4_CPtr pd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageDirectoryObject, 0);
+    seL4_CPtr pt = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageTableObject, 0);
+    seL4_CPtr frame = vka_alloc_object_leaky(&env->vka, seL4_ARM_SmallPageObject, 0);
+    seL4_CPtr frame2 = vka_alloc_object_leaky(&env->vka, seL4_ARM_SmallPageObject, 0);
+    /* Under an Arm Hyp configuration where the CPU only supports 40bit physical addressing, we
+     * only have 3 level page tables and no PGD.
+     */
+    test_assert((seL4_PGDBits == 0) || pgd != 0);
+    test_assert(pud != 0);
+    test_assert(pd != 0);
+    test_assert(pt != 0);
+    test_assert(frame != 0);
+    test_assert(frame2 != 0);
+
+
+    seL4_CPtr vspace = (seL4_PGDBits == 0) ? pud : pgd;
+    seL4_ARM_ASIDPool_Assign(env->asid_pool, vspace);
+#if seL4_PGDBits > 0
+    /* map pud into page global directory */
+    error = seL4_ARM_PageUpperDirectory_Map(pud, vspace, map_addr, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+#endif
+
+    /* map pd into page upper directory */
+    error = seL4_ARM_PageDirectory_Map(pd, vspace, map_addr, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map page table into page directory */
+    error = seL4_ARM_PageTable_Map(pt, vspace, map_addr, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map frame into the page table */
+    error = seL4_ARM_Page_Map(frame, vspace, map_addr, seL4_AllRights, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_ARM_Page_Map(frame, vspace, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_ARM_Page_Map(frame2, vspace, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0011, "Test that overmapping small pages is not permitted", test_overmap_small, true)
+
+static int test_overmap_large(env_t env)
+{
+    seL4_Word map_addr = 0x10000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr pgd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageGlobalDirectoryObject, 0);
+    seL4_CPtr pud = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageUpperDirectoryObject, 0);
+    seL4_CPtr pd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageDirectoryObject, 0);
+    seL4_CPtr frame = vka_alloc_object_leaky(&env->vka, seL4_ARM_LargePageObject, 0);
+    seL4_CPtr frame2 = vka_alloc_object_leaky(&env->vka, seL4_ARM_LargePageObject, 0);
+    /* Under an Arm Hyp configuration where the CPU only supports 40bit physical addressing, we
+     * only have 3 level page tables and no PGD.
+     */
+    test_assert((seL4_PGDBits == 0) || pgd != 0);
+    test_assert(pud != 0);
+    test_assert(pd != 0);
+    test_assert(frame != 0);
+    test_assert(frame2 != 0);
+
+
+    seL4_CPtr vspace = (seL4_PGDBits == 0) ? pud : pgd;
+    seL4_ARM_ASIDPool_Assign(env->asid_pool, vspace);
+#if seL4_PGDBits > 0
+    /* map pud into page global directory */
+    error = seL4_ARM_PageUpperDirectory_Map(pud, vspace, map_addr, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+#endif
+
+    /* map pd into page upper directory */
+    error = seL4_ARM_PageDirectory_Map(pd, vspace, map_addr, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map frame into the page table */
+    error = seL4_ARM_Page_Map(frame, vspace, map_addr, seL4_AllRights, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_ARM_Page_Map(frame, vspace, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_ARM_Page_Map(frame2, vspace, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0012, "Test that overmapping large pages is not permitted", test_overmap_large, true)
+
+static int test_overmap_huge(env_t env)
+{
+    seL4_Word map_addr = 0x10000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr pgd = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageGlobalDirectoryObject, 0);
+    seL4_CPtr pud = vka_alloc_object_leaky(&env->vka, seL4_ARM_PageUpperDirectoryObject, 0);
+    seL4_CPtr frame = vka_alloc_object_leaky(&env->vka, seL4_ARM_HugePageObject, 0);
+    seL4_CPtr frame2 = vka_alloc_object_leaky(&env->vka, seL4_ARM_HugePageObject, 0);
+    /* Under an Arm Hyp configuration where the CPU only supports 40bit physical addressing, we
+     * only have 3 level page tables and no PGD.
+     */
+    test_assert((seL4_PGDBits == 0) || pgd != 0);
+    test_assert(pud != 0);
+    test_assert(frame != 0);
+    test_assert(frame2 != 0);
+
+
+    seL4_CPtr vspace = (seL4_PGDBits == 0) ? pud : pgd;
+    seL4_ARM_ASIDPool_Assign(env->asid_pool, vspace);
+#if seL4_PGDBits > 0
+    /* map pud into page global directory */
+    error = seL4_ARM_PageUpperDirectory_Map(pud, vspace, map_addr, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+#endif
+
+    /* map frame into the page table */
+    error = seL4_ARM_Page_Map(frame, vspace, map_addr, seL4_AllRights, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_ARM_Page_Map(frame, vspace, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_ARM_Page_Map(frame2, vspace, map_addr, seL4_NoWrite, seL4_ARM_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0013, "Test that overmapping huge pages is not permitted", test_overmap_huge,
+            config_set(CONFIG_SIMULATION))
+#elif defined(CONFIG_ARCH_RISCV)
+
+static int test_overmap_small(env_t env)
+{
+    seL4_Word map_addr = 0x10000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr vspace = vka_alloc_object_leaky(&env->vka, seL4_RISCV_PageTableObject, 0);
+    seL4_CPtr level2 = vka_alloc_object_leaky(&env->vka, seL4_RISCV_PageTableObject, 0);
+#if defined(CONFIG_ARCH_RISCV64)
+    seL4_CPtr level3 = vka_alloc_object_leaky(&env->vka, seL4_RISCV_PageTableObject, 0);
+#endif
+    seL4_CPtr frame = vka_alloc_object_leaky(&env->vka, seL4_RISCV_4K_Page, 0);
+    seL4_CPtr frame2  = vka_alloc_object_leaky(&env->vka, seL4_RISCV_4K_Page, 0);
+    test_assert(vspace != 0);
+    test_assert(level2 != 0);
+#if defined(CONFIG_ARCH_RISCV64)
+    test_assert(level3 != 0);
+#endif
+    test_assert(frame != 0);
+    test_assert(frame2 != 0);
+
+
+    seL4_RISCV_ASIDPool_Assign(env->asid_pool, vspace);
+
+    /* map lvl2 into vspace */
+    error = seL4_RISCV_PageTable_Map(level2, vspace, map_addr, seL4_RISCV_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+#if defined(CONFIG_ARCH_RISCV64)
+    /* map lvl3 into vspace */
+    error = seL4_RISCV_PageTable_Map(level3, vspace, map_addr, seL4_RISCV_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+#endif
+
+    /* map frame into the page table */
+    error = seL4_RISCV_Page_Map(frame, vspace, map_addr, seL4_AllRights, seL4_RISCV_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_RISCV_Page_Map(frame, vspace, map_addr, seL4_NoWrite, seL4_RISCV_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_RISCV_Page_Map(frame2, vspace, map_addr, seL4_NoWrite, seL4_RISCV_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0011, "Test that overmapping small pages is not permitted", test_overmap_small, true)
+#elif defined(CONFIG_ARCH_X86_64)
+
+
+static int test_overmap_small(env_t env)
+{
+    seL4_Word map_addr = 0x10000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr vspace = vka_alloc_object_leaky(&env->vka, seL4_X64_PML4Object, 0);
+    seL4_CPtr pdpt = vka_alloc_object_leaky(&env->vka, seL4_X86_PDPTObject, 0);
+    seL4_CPtr pd = vka_alloc_object_leaky(&env->vka, seL4_X86_PageDirectoryObject, 0);
+    seL4_CPtr pt = vka_alloc_object_leaky(&env->vka, seL4_X86_PageTableObject, 0);
+    seL4_CPtr frame = vka_alloc_object_leaky(&env->vka, seL4_X86_4K, 0);
+    seL4_CPtr frame2  = vka_alloc_object_leaky(&env->vka, seL4_X86_4K, 0);
+    test_assert(vspace != 0);
+    test_assert(pdpt != 0);
+    test_assert(pd != 0);
+    test_assert(pt != 0);
+    test_assert(frame != 0);
+    test_assert(frame2 != 0);
+
+    seL4_X86_ASIDPool_Assign(env->asid_pool, vspace);
+
+    /* map pdpt into vspace */
+    error = seL4_X86_PDPT_Map(pdpt, vspace, map_addr, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map pd into vspace */
+    error = seL4_X86_PageDirectory_Map(pd, vspace, map_addr, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map pt into vspace */
+    error = seL4_X86_PageTable_Map(pt, vspace, map_addr, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map frame into the page table */
+    error = seL4_X86_Page_Map(frame, vspace, map_addr, seL4_AllRights, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_X86_Page_Map(frame, vspace, map_addr, seL4_NoWrite, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_X86_Page_Map(frame2, vspace, map_addr, seL4_NoWrite, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0011, "Test that overmapping small pages is not permitted", test_overmap_small, true)
+
+static int test_overmap_large(env_t env)
+{
+    seL4_Word map_addr = 0x10000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr vspace = vka_alloc_object_leaky(&env->vka, seL4_X64_PML4Object, 0);
+    seL4_CPtr pdpt = vka_alloc_object_leaky(&env->vka, seL4_X86_PDPTObject, 0);
+    seL4_CPtr pd = vka_alloc_object_leaky(&env->vka, seL4_X86_PageDirectoryObject, 0);
+    seL4_CPtr frame = vka_alloc_object_leaky(&env->vka, seL4_X86_LargePageObject, 0);
+    seL4_CPtr frame2  = vka_alloc_object_leaky(&env->vka, seL4_X86_LargePageObject, 0);
+    test_assert(vspace != 0);
+    test_assert(pdpt != 0);
+    test_assert(pd != 0);
+    test_assert(frame != 0);
+    test_assert(frame2 != 0);
+
+    seL4_X86_ASIDPool_Assign(env->asid_pool, vspace);
+
+    /* map pdpt into vspace */
+    error = seL4_X86_PDPT_Map(pdpt, vspace, map_addr, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map pd into vspace */
+    error = seL4_X86_PageDirectory_Map(pd, vspace, map_addr, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map frame into the page table */
+    error = seL4_X86_Page_Map(frame, vspace, map_addr, seL4_AllRights, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_X86_Page_Map(frame, vspace, map_addr, seL4_NoWrite, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_X86_Page_Map(frame2, vspace, map_addr, seL4_NoWrite, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0012, "Test that overmapping large pages is not permitted", test_overmap_large, true)
+
+static int test_overmap_huge(env_t env)
+{
+    seL4_Word map_addr = 0x40000000;
+    cspacepath_t path;
+    int error;
+
+    seL4_CPtr vspace = vka_alloc_object_leaky(&env->vka, seL4_X64_PML4Object, 0);
+    seL4_CPtr pdpt = vka_alloc_object_leaky(&env->vka, seL4_X86_PDPTObject, 0);
+    seL4_CPtr frame = vka_alloc_object_leaky(&env->vka, seL4_X64_HugePageObject, 0);
+    seL4_CPtr frame2  = vka_alloc_object_leaky(&env->vka, seL4_X64_HugePageObject, 0);
+    test_assert(vspace != 0);
+    test_assert(pdpt != 0);
+    test_assert(frame != 0);
+    test_assert(frame2 != 0);
+
+    seL4_X86_ASIDPool_Assign(env->asid_pool, vspace);
+
+    /* map pdpt into vspace */
+    error = seL4_X86_PDPT_Map(pdpt, vspace, map_addr, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* map frame into the page table */
+    error = seL4_X86_Page_Map(frame, vspace, map_addr, seL4_AllRights, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Remap the frame with readonly permissions */
+    error = seL4_X86_Page_Map(frame, vspace, map_addr, seL4_NoWrite, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_NoError);
+
+    /* Try to overmap the existing mapping*/
+    error = seL4_X86_Page_Map(frame2, vspace, map_addr, seL4_NoWrite, seL4_X86_Default_VMAttributes);
+    test_error_eq(error, seL4_DeleteFirst);
+
+    return sel4test_get_result();
+}
+DEFINE_TEST(PT0013, "Test that overmapping huge pages is not permitted", test_overmap_huge,
+            config_set(CONFIG_SIMULATION))
+#endif