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

).

[lsf37]

Have you had a look if this would be a breaking change for CAmkES?

It does look to me like it is specifically generating RWX (this file is from CAmkES) and the intention for the capDL text spec was that RWX vs RW etc can be specified. Whether that then results in being communicated to the C loader via presence or absence of Grant which is unused for frames is a different question.

I agree that it'd be better to be closer to the kernel interface for that, but the user-facing text spec doesn't need to change. It'd be Ok to have both, though, i.e. adding an explicit execute_never VM attribute in the text spec in addition to RW being equivalent to RW + execute_never and RWX being RW + execute_never=0.

Maybe the confusion is between actual caps in CNodes and mapping caps. The former have no vm attributes and RWX there would not makes, the latter do and the X would translate into a vm attribute of the mapping we want.