Add support for XN vm attributes

[nspin]

This includes removing the use of the grant permission to encode executable permissions for frames. The kernel does not use the grant permission to determine whether a frame is executable, so this encoding was not doing anything.

Motivated by seL4/rust-sel4#280 (comment)

[lsf37]

The kernel does not use the grant permission to determine whether a frame is executable, so this encoding was not doing anything.

Hm, I need to look into what the capDL formalisation does with this. It's possible that the Haskell version here was an early attempt to model NX that never got carried through to the rest of the model and implementation.

[kent-mcleod]

How would this impact the C capdl loader app? It does respect the lack of grant right to set execute never on the ARM page mappings here I think: https://github.com/seL4/capdl/blob/master/capdl-loader-app/src/main.c#L1496-L1500

[nspin]

How would this impact the C capdl loader app? It does respect the lack of grant right to set execute never on the ARM page mappings here I think: https://github.com/seL4/capdl/blob/master/capdl-loader-app/src/main.c#L1496-L1500

Good catch. The way forward with this PR as it is would be to remove the line you linked and instead add logic to incorporate XN into the vm_attrs at

capdl/capDL-tool/CapDL/PrintC.hs

Lines 145 to 146 in 01b3bd4

	", .vm_attribs = " ++
	(if cached then "seL4_ARCH_Default_VMAttributes" else "CDL_VM_CacheDisabled") ++

(and at

capdl/capdl-loader-app/include/capdl.h

Lines 19 to 32 in 01b3bd4

	#define CDL_VM_CacheEnabled seL4_ARCH_Default_VMAttributes
	#define CDL_VM_CacheDisabled seL4_ARCH_Uncached_VMAttributes
	#if defined(CONFIG_ARCH_ARM)
	/* ARM does not support write through */
	#define CDL_VM_WriteThrough CDL_VM_CacheDisabled
	/* Note that this is the number of bits translated by the PT
	* not the size of the actual PT object */
	#elif defined(CONFIG_ARCH_X86)
	#define CDL_VM_WriteThrough seL4_X86_WriteThrough
	#endif

).