diff --git a/include/arch/arm/arch/object/structures.bf b/include/arch/arm/arch/object/structures.bf
index 26a3adc633cff02abe7acb33ff2f61c5e028a611..c3e178de807215337e6935f24568416ccbdbd53a 100644
--- a/include/arch/arm/arch/object/structures.bf
+++ b/include/arch/arm/arch/object/structures.bf
@@ -451,11 +451,6 @@ tagged_union pde pdeType {
}
-- Page table entries
-block pte_invalid {
- padding 30
- field pteType 2
-}
-
block pte_large {
field_high address 16
field XN 1
@@ -467,7 +462,8 @@ block pte_large {
field AP 2
field C 1
field B 1
- field pteType 2
+ field pteSize 1
+ field reserved 1 -- must be set
}
block pte_small {
@@ -479,21 +475,20 @@ block pte_small {
field AP 2
field C 1
field B 1
- -- The lower bit of pteType is used to store the XN bit for small pages
- -- We ignore this here, and use tag 2 for small pages which sets XN always to 0.
- field pteType 2
+ field pteSize 1
+ field XN 1
}
-tagged_union pte pteType {
- tag pte_invalid 0
- tag pte_large 1
- tag pte_small 2
+tagged_union pte pteSize {
+ tag pte_large 0
+ tag pte_small 1
}
-- VM attributes
block vm_attributes {
- padding 30
+ padding 29
+ field armExecuteNever 1
field armParityEnabled 1
field armPageCacheable 1
}
diff --git a/include/arch/arm/arch/object/structures.h b/include/arch/arm/arch/object/structures.h
index cf695db1b3df676383731965dce22c068e15849b..09046ca3271a45a7851af1a32664aefea50bc1ce 100644
--- a/include/arch/arm/arch/object/structures.h
+++ b/include/arch/arm/arch/object/structures.h
@@ -570,4 +570,33 @@ isArchCap(cap_t cap)
return (cap_get_capType(cap) % 2);
}
+/* We need to supply different type getters for the bitfield generated PTE type
+ * because there is an implicit third type that PTEs can be. If the type bit is
+ * set but the reserved bit is not set, the type of the PTE is invalid, not a
+ * large PTE.
+ */
+enum { pte_pte_invalid = 2 };
+
+static inline uint32_t __attribute__((__const__))
+pte_get_pteType(pte_t pte) {
+ if (pte_get_pteSize(pte) == pte_pte_small) {
+ return pte_pte_small;
+ } else if (pte_pte_large_get_reserved(pte) == 1) {
+ return pte_pte_large;
+ } else {
+ return pte_pte_invalid;
+ }
+}
+
+static inline uint32_t __attribute__((__pure__))
+pte_ptr_get_pteType(pte_t *pte_ptr) {
+ if (pte_ptr_get_pteSize(pte_ptr) == pte_pte_small) {
+ return pte_pte_small;
+ } else if (pte_pte_large_ptr_get_reserved(pte_ptr) == 1) {
+ return pte_pte_large;
+ } else {
+ return pte_pte_invalid;
+ }
+}
+
#endif
diff --git a/libsel4/arch_include/arm/sel4/arch/types.h b/libsel4/arch_include/arm/sel4/arch/types.h
index 1f396fda2a653887eeadae4110599262d01c8557..13c6750c78f98923f40de9c88874343c4dbf9570 100644
--- a/libsel4/arch_include/arm/sel4/arch/types.h
+++ b/libsel4/arch_include/arm/sel4/arch/types.h
@@ -48,6 +48,7 @@ typedef enum {
seL4_ARM_PageCacheable = 0x01,
seL4_ARM_ParityEnabled = 0x02,
seL4_ARM_Default_VMAttributes = 0x03,
+ seL4_ARM_ExecuteNever = 0x04,
/* seL4_ARM_PageCacheable | seL4_ARM_ParityEnabled */
SEL4_FORCE_LONG_ENUM(seL4_ARM_VMAttributes),
} seL4_ARM_VMAttributes;
diff --git a/manual/parts/vspace.tex b/manual/parts/vspace.tex
index 841ba75577328e08e06a93b54a2ed1b5a2cf73d8..8aa489cb6be939af87d2d86f4d490fc898fc3647 100644
--- a/manual/parts/vspace.tex
+++ b/manual/parts/vspace.tex
@@ -181,6 +181,7 @@ page being mapped; possible values for ARM are shown in \autoref{tbl:vmattr_arm}
to be cached \\
\texttt{seL4\_ARM\_ParityEnabled} & Enable parity checking for
this mapping\\
+ \texttt{seL4\_ARM\_ExecuteNever} & Map this memory as non-executable \\
\bottomrule
\end{tabularx}
\caption{\label{tbl:vmattr_arm} Virtual memory attributes for ARM page
diff --git a/src/arch/arm/kernel/vspace.c b/src/arch/arm/kernel/vspace.c
index f9e49bcb0ed3060aeecd41cc58a52f90e3ab0647..1b1d931a1d7de1f5af0109e5f35856951a2da7b4 100644
--- a/src/arch/arm/kernel/vspace.c
+++ b/src/arch/arm/kernel/vspace.c
@@ -130,7 +130,8 @@ map_it_frame_cap(cap_t pd_cap, cap_t frame_cap)
0, /* TEX = 0 */
APFromVMRights(VMReadWrite),
1, /* cacheable */
- 1 /* write-back caching */
+ 1, /* write-back caching */
+ 0 /* executable */
);
}
@@ -150,7 +151,8 @@ map_kernel_frame(paddr_t paddr, pptr_t vaddr, vm_rights_t vm_rights, vm_attribut
0, /* TEX = 0 */
APFromVMRights(vm_rights),
vm_attributes_get_armPageCacheable(attributes),
- 1 /* Write-back caching */
+ 1, /* Write-back caching */
+ 0 /* executable */
);
}
@@ -266,7 +268,8 @@ map_kernel_window(void)
VMKernelOnly,
vm_attributes_new(
true, /* armParityEnabled */
- true /* armPageCacheable */
+ true, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -277,7 +280,8 @@ map_kernel_window(void)
VMReadOnly,
vm_attributes_new(
true, /* armParityEnabled */
- true /* armPageCacheable */
+ true, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -288,7 +292,8 @@ map_kernel_window(void)
VMKernelOnly,
vm_attributes_new(
true, /* armParityEnabled */
- true /* armPageCacheable */
+ true, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -568,6 +573,13 @@ unmapPageTable(asid_t asid, vptr_t vaddr, pte_t* pt)
}
}
+static pte_t pte_pte_invalid_new(void) {
+ /* Invalid as every PTE must have bit 0 set (large PTE) or bit 1 set (small
+ * PTE). 0 == 'translation fault' in ARM parlance.
+ */
+ return (pte_t){{ 0 }};
+}
+
void
unmapPage(vm_page_size_t page_size, asid_t asid, vptr_t vptr, void *pptr)
{
@@ -959,7 +971,7 @@ invalidateTLBByASID(asid_t asid)
static pte_t CONST
makeUserPTE(vm_page_size_t page_size, paddr_t paddr,
- bool_t cacheable, vm_rights_t vm_rights)
+ bool_t cacheable, bool_t nonexecutable, vm_rights_t vm_rights)
{
pte_t pte;
word_t ap;
@@ -975,7 +987,8 @@ makeUserPTE(vm_page_size_t page_size, paddr_t paddr,
0, /* APX = 0, privileged full access */
5, /* TEX = 0b101, outer write-back, write-allocate */
ap,
- 0, 1 /* Inner write-back, write-allocate (except on ARM11) */);
+ 0, 1, /* Inner write-back, write-allocate (except on ARM11) */
+ nonexecutable);
} else {
pte = pte_pte_small_new(paddr,
1, /* not global */
@@ -983,7 +996,8 @@ makeUserPTE(vm_page_size_t page_size, paddr_t paddr,
0, /* APX = 0, privileged full access */
0, /* TEX = 0b000, strongly-ordered. */
ap,
- 0, 0);
+ 0, 0,
+ nonexecutable);
}
break;
}
@@ -991,22 +1005,24 @@ makeUserPTE(vm_page_size_t page_size, paddr_t paddr,
case ARMLargePage: {
if (cacheable) {
pte = pte_pte_large_new(paddr,
- 0, /* XN not set */
+ nonexecutable,
5, /* TEX = 0b101, outer write-back, write-allocate */
1, /* not global */
0, /* not shared */
0, /* APX = 0, privileged full access */
ap,
- 0, 1 /* Inner write-back, write-allocate (except on ARM11) */);
+ 0, 1, /* Inner write-back, write-allocate (except on ARM11) */
+ 1 /* reserved */);
} else {
pte = pte_pte_large_new(paddr,
- 0, /* XN not set */
+ nonexecutable,
0, /* TEX = 0b000, strongly-ordered */
1, /* not global */
1, /* shared */
0, /* APX = 0, privileged full access */
ap,
- 0, 0);
+ 0, 0,
+ 1 /* reserved */);
}
break;
}
@@ -1020,7 +1036,8 @@ makeUserPTE(vm_page_size_t page_size, paddr_t paddr,
static pde_t CONST
makeUserPDE(vm_page_size_t page_size, paddr_t paddr, bool_t parity,
- bool_t cacheable, word_t domain, vm_rights_t vm_rights)
+ bool_t cacheable, bool_t nonexecutable, word_t domain,
+ vm_rights_t vm_rights)
{
word_t ap, size2;
@@ -1045,8 +1062,7 @@ makeUserPDE(vm_page_size_t page_size, paddr_t paddr, bool_t parity,
0, /* not shared */
0, /* APX = 0, privileged full access */
5, /* TEX = 0b101, outer write-back, write-allocate */
- ap, parity, domain,
- 0, /* XN not set */
+ ap, parity, domain, nonexecutable,
0, 1 /* Inner write-back, write-allocate (except on ARM11) */);
} else {
return pde_pde_section_new(paddr, size2,
@@ -1054,8 +1070,7 @@ makeUserPDE(vm_page_size_t page_size, paddr_t paddr, bool_t parity,
1, /* shared */
0, /* APX = 0, privileged full access */
0, /* TEX = 0b000, strongly-ordered */
- ap, parity, domain,
- 0, /* XN not set */
+ ap, parity, domain, nonexecutable,
0, 0);
}
}
@@ -1205,6 +1220,7 @@ createSafeMappingEntries_PTE
ret.pte = makeUserPTE(ARMSmallPage, base,
vm_attributes_get_armPageCacheable(attr),
+ vm_attributes_get_armExecuteNever(attr),
vmRights);
lu_ret = lookupPTSlot(pd, vaddr);
@@ -1240,6 +1256,7 @@ createSafeMappingEntries_PTE
ret.pte = makeUserPTE(ARMLargePage, base,
vm_attributes_get_armPageCacheable(attr),
+ vm_attributes_get_armExecuteNever(attr),
vmRights);
lu_ret = lookupPTSlot(pd, vaddr);
@@ -1298,7 +1315,9 @@ createSafeMappingEntries_PDE
ret.pde = makeUserPDE(ARMSection, base,
vm_attributes_get_armParityEnabled(attr),
vm_attributes_get_armPageCacheable(attr),
- 0, vmRights);
+ vm_attributes_get_armExecuteNever(attr),
+ 0,
+ vmRights);
currentPDEType =
pde_ptr_get_pdeType(ret.pde_entries.base);
@@ -1322,7 +1341,9 @@ createSafeMappingEntries_PDE
ret.pde = makeUserPDE(ARMSuperSection, base,
vm_attributes_get_armParityEnabled(attr),
vm_attributes_get_armPageCacheable(attr),
- 0, vmRights);
+ vm_attributes_get_armExecuteNever(attr),
+ 0,
+ vmRights);
for (i = 0; i < SECTIONS_PER_SUPER_SECTION; i++) {
currentPDEType =
diff --git a/src/plat/am335x/machine/hardware.c b/src/plat/am335x/machine/hardware.c
index 2fc71d137351ee2ca840025b615df4b08b4609b8..9a2ef37d0bcdc368b58ed5812741bfca5f137cd8 100644
--- a/src/plat/am335x/machine/hardware.c
+++ b/src/plat/am335x/machine/hardware.c
@@ -76,7 +76,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -87,7 +88,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -99,7 +101,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
#endif
diff --git a/src/plat/exynos4/machine/hardware.c b/src/plat/exynos4/machine/hardware.c
index 553e6d7b839af0afec4e61a06b89cb4ec757ff1d..a8ebc96d1ffb34270c4a143b0bda064f44103f96 100644
--- a/src/plat/exynos4/machine/hardware.c
+++ b/src/plat/exynos4/machine/hardware.c
@@ -236,7 +236,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -247,7 +248,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
map_kernel_frame(
@@ -256,7 +258,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -267,7 +270,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -279,7 +283,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
#endif /* DEBUG */
diff --git a/src/plat/exynos5/machine/hardware.c b/src/plat/exynos5/machine/hardware.c
index 4027f119d3490259f32459ee45ae024d376616b1..23ed4c518f9ffcccb341a1f6dad7ec93413e8f3c 100644
--- a/src/plat/exynos5/machine/hardware.c
+++ b/src/plat/exynos5/machine/hardware.c
@@ -295,7 +295,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -306,7 +307,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
map_kernel_frame(
@@ -315,7 +317,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -327,7 +330,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
#endif /* DEBUG */
diff --git a/src/plat/imx31/machine/hardware.c b/src/plat/imx31/machine/hardware.c
index dc248887b1c3c4bdbb22b22d44802a8b616c8c85..bad6c8a94398edb8745399d8d10c3e0fc63fe621 100644
--- a/src/plat/imx31/machine/hardware.c
+++ b/src/plat/imx31/machine/hardware.c
@@ -229,7 +229,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -240,7 +241,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -251,7 +253,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -263,7 +266,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
#endif
diff --git a/src/plat/imx6/machine/hardware.c b/src/plat/imx6/machine/hardware.c
index 883e9c1cca2aba604f24df72dbacd1a769e2c56c..75745017a5f6fc0cf6f0a349159baf81ed41f0cb 100644
--- a/src/plat/imx6/machine/hardware.c
+++ b/src/plat/imx6/machine/hardware.c
@@ -206,7 +206,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -217,7 +218,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -228,7 +230,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -241,7 +244,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
#endif /* DEBUG */
diff --git a/src/plat/omap3/machine/hardware.c b/src/plat/omap3/machine/hardware.c
index 9c18883ac4829cea2d8602ba1f107931551d560a..c3ea996d4bceefd39c5f31878e029e74b50e147c 100644
--- a/src/plat/omap3/machine/hardware.c
+++ b/src/plat/omap3/machine/hardware.c
@@ -179,7 +179,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -190,7 +191,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
@@ -202,7 +204,8 @@ map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(
false, /* armParityEnabled */
- false /* armPageCacheable */
+ false, /* armPageCacheable */
+ false /* armExecuteNever */
)
);
#endif