Bug with capDL initialiser untyped allocation for high-address regions

[Ivan-Velickovic]

When trying to allocate from untypeds close to the top of physical memory, we run into problems with the capDL initialiser's untyped allocation strategy. This specifically occurred with Microkit on QEMU x86-64 but the issue applies to all platforms/architectures.

The issue is that the kernel calculates untyped alignment based on the kernel virtual addresses rather than the physical addresses of the memory being allocated. The initialiser does not consider this, which means in certain cases there is a mismatch between the kernel's untyped watermark and the initialiser's when the kernel virtual address overflows, causing a difference between the max size bits of the next untyped allocation.

This was encountered when we were trying to use device memory at a high-address such as 0xe0000000000. This address is in the middle of an untyped which causes the initialiser to use UntypeRetype to keep splitting the large untyped until it can make the intended allocation at 0xe0000000000. During this process, the mismatch between the kernel book-keeping and the initialiser's book-keeping happens which causes the initialiser to think it is allocating from 0xe0000000000 when in reality it is some different physical memory.

We have some logs from when we encountered this to help show what the problem is:

TRACE [sel4_capdl_initializer::initialize] Allocating from untyped: 0x4000000000..0x8000000000 (size_bits = 38, device = true)
TRACE [sel4_capdl_initializer::initialize] Allocating from untyped: 0x8000000000..0x408000000000 (size_bits = 46, device = true)
TRACE [sel4_sys::invocations] seL4_CNode_Delete(_service=2, index=39138, depth=64)
TRACE [sel4_capdl_initializer::initialize] Creating dummy: paddr=0x8000000000, size_bits=39
TRACE [sel4_sys::invocations] seL4_Untyped_Retype(_service=3057, type=0, size_bits=39, root=2, node_index=0, node_depth=0, node_offset=39138, num_objects=1)
alignedFreeRef = 0x0, freeRef = 0x0
invokeUntyped_Retype(): reset = 1, retypeBase = 0x8000000000, newType = 0x0, userSize = 0x27, destOffset = 0x98e2, destLength = 0x1, deviceMemory = 1, totalObjectSize = 0x8000000000
TRACE [sel4_sys::invocations] seL4_CNode_Delete(_service=2, index=39139, depth=64)
TRACE [sel4_capdl_initializer::initialize] Creating dummy: paddr=0x10000000000, size_bits=40
TRACE [sel4_sys::invocations] seL4_Untyped_Retype(_service=3057, type=0, size_bits=40, root=2, node_index=0, node_depth=0, node_offset=39139, num_objects=1)
alignedFreeRef = 0x10000000000, freeRef = 0x8000000000

Here, the capDL initialiser believes 0x8000000000 + (1 << 39) is 0x10000000000 which has
an alignment of 40-bits. However, due to the physical to kernel virtual address translation, the kernel sees 0x0 + (1 << 39) which is 0x8000000000 which has an alignment of 39-bits. The capDL initialiser then tries to allocate a 40-bit aligned untype but because the actual watermark (in seL4's tracking) is 39-bit aligned, there's a mismatch between
the initialiser and seL4, which messes up the initialiser's book-keeping and it ends up mapping the
incorrect device memory.

The solution(s) are:

1. Adopt what the Microkit does by considering the kernel virtual addresses.
2. Change the strategy to instead do a binary search based approach when splitting the untyped.
   This is akin to the util_libs 'utspace_split'.

We've quickly done solution 1 to make progress but we think it would be better if the initialiser was changed to solution 2 but that is more invasive.

We have run into this exact same issue before with Microkit, and the fix was done in ab560e15b1facaf2c78a53cf1415ea451f569a4c.

There's a bit of past discussion in seL4/seL4#1004 about this issue in general.

[lsf37]

Something is not quite right in that analysis yet. The kernel virtual address in the untyped can't overflow: all untypeds, including device untypeds, are aligned to their size, which means overflow in the kernel virtual address space inside the untyped is impossible. (This is in fact one of the reasons for those alignment requirements).

What could over/underflow is the physical address, though, depending on the layout. The physical address of the untyped has smaller alignment requirements and is at a fixed offset to the virtual address.

[midnightveil]

The kernel virtual address in the untyped can't overflow: all untypeds, including device untypeds, are aligned to their size, which means overflow in the kernel virtual address space inside the untyped is impossible. (This is in fact one of the reasons for those alignment requirements).

Yes, there's no overflow in the untyped itself; just one that starts at a pptr of 0x0 because the code making them has overflowed because of paddr_to_pptr (which is fine, as previously discussed). When "the kernel virtual address overflows" we mean the base does, but not within a single untyped.

What could over/underflow is the physical address, though, depending on the layout. The physical address of the untyped has smaller alignment requirements and is at a fixed offset to the virtual address.

This is what is happening (but it's not actually the issue)

[Indanz]

The solution(s) are:

1. Adopt what the Microkit does by considering the kernel virtual addresses.

2. Change the strategy to instead do a binary search based approach when splitting the untyped.
   This is akin to the util_libs 'utspace_split'.

3. Limit allocated UTs sizes to 39 bits or smaller (for AArch64, different value for other platforms).