I think the confusion arises from your current understanding of how accessible "kernel objects" are to userspace. Specifically:

> The user level resource managers can access both the kernel memory and other memory as well because they have capabilities to both.

The thing is, kernel objects are not accessible to userspace. Userspace can *refer* to them via the numerical indexes of their capability token. We call these numerical indexes "capability-pointers" (CPtrs), which are not to be confused with "capabilities", which are themselves also kernel-objects (and therefore, inaccessible to userspace). Userspace can ask the kernel to perform operations on a kernel object by invoking a capability to that kernel object (and the capability is specified to the kernel as a CPtr).

A simple way to think about how the kernel prevents userspace from accessible kernel objects, is to realize that after a chunk of untyped memory has been retyped into an object, say, a Frame or TCB, that new object (the Frame or TCB) cannot be retyped further. The untyped memory has been made into a kernel object, and userspace cannot access kernel memory. In order to transform that object into something else, you'd need to destroy the TCB, and then re-retype the original untyped into something new.

In the case of Frame objects however, the special operation of combining a Frame object with a PageTable object using the "PageMap()" invocation causes the Frame to become visible to userspace as a result of the fact that the PageMap operation manipulates the hardware MMU to make the Frame visible to within the virtual address space. You cannot however, do a "PageMap" that maps a TCB into a VSpace. Only Frames can be mapped into VSpaces, so they are the only kernel objects that can be viewed by userspace.

Fortunately, the kernel doesn't access Frame objects for any reason other than to zero them when they are being created, or in the case of the IPC buffer, to read and write the IPC buffer fields. For every other kind of kernel object, there's no way to map the kernel objects to be viewable by userspace.

From: Devel <devel-bounces@sel4.systems> on behalf of Mark Reus <markreusva@gmail.com>
Sent: 01 December 2016 13:29
To: devel@sel4.systems
Subject: [seL4] seL4 Memory Management

I have been going through some of the research papers about seL4. I wanted to understand the security features in the memory management. I am a little confused, hope someone can I help me.

Quote from the paper

"Finally, the kernel ensures that each physical frame mapped by the MMU at a useraccessible address is of the Frame object type. These Frame objects contain no kernel data and since they cannot overlap with other typed objects, direct user access to kernel data is not possible"

I understand that seL4 promotes isolation between processes and no allocation is done by the kernel itself rather it is done by user level manager. Since we use untyped memory and we retype them, there is no overlap of objects. The user level resource managers can access both the kernel memory and other memory as well because they have capabilities to both. What exactly in the above quote causes the isolation of user level memory with kernel memory. I am of the notion that the kernel allocated objects are still accessible and can be modified to point to some other memory? Am I misunderstanding something?

Regards

Mark