User-level kernel heap introspection

seL4 kernel
1

Would it be possible to allow for any untyped memory to be mapped into a VSpace as read-only before it is the retyped into other kinds of memory? It seems it would be useful if a user-level memory manager could introspect the state of the kernel objects for the purposes of debugging or for avoiding duplication of things like VSpace layout.

A possible way I could think of doing this would to introduce some concept of an ‘observer frame’ that can be retyped from an untyped object with no children that aren’t also observer frames. These frames would have to align to frame sizes available on the given platform and would have to be read-only when mapped. An untyped with only observer frames as children could then be retyped in all the ways that an untyped with no children can currently be retyped (i.e. used for kernel objects or smaller untypeds).

Doing so would allow a user-level mapping of the physical address space (to the regions where user-level has capabilities to the untypeds) and could allow a user not only to traverse virtual address translation tables, but also to introspect and traverse CSpaces and the CDT.

@gerwin.klein, do you think such a system could be permissable in a verified configuration?

Drawbacks of this idea would be that any untypes smaller than the smallest frame size or any kernel objects in memory to which untypeds aren’t provided (such as the objects for the initial task) can’t be mapped.

2

I don’t think this would work in a verified configuration, and it might have problems in unverified ones as well. One of the key invariants we have is that objects don’t overlap, which would be majorly violated in this scenario. That’d definitely kill the proofs, but even in unverified versions all kinds of things rely on that, so it’s hard to see which obscure corner might break even for a read-only version of objects. E.g. what happens when you delete the untyped, how do you track those frames etc.

It’d also have direct infoflow implications, because you can now observe everything inside kernel objects, not just what the kernel lets you see. There might be information about other objects in the encoding (not sure, haven’t fully checked through that, but proving it would now fully depend on the data representation, i.e. not allow refinement any more).

3

One such example of this would be the MDB nodes inside capabilities which could point to memory outside the mapped regions.

4

Yes. Also thread states linking to endpoints they are blocked on, which could be in another security domain.