model kernel ELF window for AArch64

[lsf37]

Up until #1031 and seL4/seL4#1516 it was fine for the formalisation to ignore the kernel ELF, because it overlapped with the normal kernel window, so the formalisation could treat objects such as the (empty) global user page table as residing in the kernel window. The objects that reside in the kernel ELF window are the global variables.

seL4/seL4#1516 makes the kernel ELF window and the kernel window distinct. Because we need to require that the physical address of the global user page table fits into 48 bits and this physical address is computed via the kernel ELF window translation, this distinctness becomes directly visible in the formalisation and leads to a contradiction with the separate invariant that all objects live in the kernel window.

The problem currently only leads to a problem in the example state for information flow at the design spec level, and could be circumvented by picking an address in the kernel window that happens to have the right properties under the kernel ELF window translation, but this would not properly model the kernel setup.

The proper fix for this is:

• introduce the kernel ELF window to the formal model
• require that global_refs are within the kernel ELF window, and that only objects at global_refs addresses are within the kernel ELF window
• relax the pspace_in_kernel_window invariant to say that an object must be either fully within the kernel window or fully within the kernel ELF window

[Indanz]

How is this solved on RISCV?

If it's only the empty global user page table (armKSGlobalUserVSpace), that could be replaced with disabling page table walks instead (assuming there is a way to make the proofs understand that concept). This can be done by setting EPD0 and/or EPD1 to 1 in TCR_EL1 (HYP would set both, non-HYP only EPD0).

and could be circumvented by picking an address in the kernel window that happens to have the right properties under the kernel ELF window translation, but this would not properly model the kernel setup.

True, but any address in the ELF region will be within 48 bits, as the kernel can't be loaded to non-existing memory. Putting a lot of effort into proving this isn't very useful, anything that works is good enough.

[lsf37]

How is this solved on RISCV?

RISCV doesn't have the 48-bit requirement for ttbr0 in the C bitfield, so the C proof obligation doesn't occur and doesn't force its way up the stack. RISCV should probably get the same model, but so far at least nothing forces a contradiction.

If it's only the empty global user page table (armKSGlobalUserVSpace), that could be replaced with disabling page table walks instead (assuming there is a way to make the proofs understand that concept). This can be done by setting EPD0 and/or EPD1 to 1 in TCR_EL1 (HYP would set both, non-HYP only EPD0).

We'll need to model the ELF region anyway for multikernel so that we can state that those are distinct as well. It should not be very high effort to add (famous last words), so hopefully no C side changes necessary.

and could be circumvented by picking an address in the kernel window that happens to have the right properties under the kernel ELF window translation, but this would not properly model the kernel setup.

True, but any address in the ELF region will be within 48 bits, as the kernel can't be loaded to non-existing memory. Putting a lot of effort into proving this isn't very useful, anything that works is good enough.

That's basically the approach we've been taking so far, but the in terms of assurance it's better to just model it properly instead of handwaving it away. I agree that there is nothing interesting here to prove, though. It's just straightening out a small wrinkle.

[Indanz]

We'll need to model the ELF region anyway for multikernel so that we can state that those are distinct as well.

For multikernel we need distinct normal memory regions and ELF regions (at least the data part. The RO/X part could be shared). I don't know how to enforce that other than having one kernel load the others (or at least do the memory partitioning and verify that part). Otherwise it's just blindly trusting some external input, either compile time or runtime.

It should not be very high effort to add (famous last words), so hopefully no C side changes necessary.

But the C changes are easy compared to the proof changes. If there is anything on the C side that can be done to ease verification, please say so.