portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

manual: more precision on retype and revoke

Browse source 
The concept of untyped object was confusing the description here, esp
when it comes to the CDT and what is derived from what. Also explain
when memory is actually zeroed, because that is important for where you
want to make sure that no confidential data remains in memory, for
instance.

This commit only affects the retype/revoke explanation and does not
attempt to clear up the concept of untyped object more generally.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-10-19 10:44:57 +11:00 committed by Gerwin Klein
parent be34e323e5
commit 3a7764c033
1 changed files with 21 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
manual/parts/objects.tex
View file

@ -419,28 +419,31 @@ creates new kernel objects by retyping untyped memory, the newly created
capabilities would be inserted into the CDT as children of the untyped
memory capability.
For each \obj{Untyped Memory} region, the kernel keeps
a \emph{watermark} recording how much of the region has previously been
allocated. Whenever a user requests the kernel to create new objects in
an untyped memory region, the kernel will carry out one of two actions:
if there are already existing objects allocated in the region, the
For each \obj{Untyped} capability pointing to an \obj{Untyped Memory} region,
the kernel keeps a \emph{watermark} recording how much of the region has
previously been allocated. Whenever a user requests the kernel to create new
objects in an untyped memory region, the kernel will carry out one of two
actions: if there are already existing objects allocated in the region, the
kernel will allocate the new objects at the current watermark level, and
increase the watermark. If all objects previously allocated in the
region have been deleted, the kernel will reset the watermark and start
increase the watermark. If all capabilities to objects previously allocated in
the region have been deleted, the kernel will reset the watermark and start
allocating new objects from the beginning of the region again.
Finally, the \apifunc{seL4\_CNode\_Revoke}{cnode_revoke} method provided by \obj{CNode} objects
destroys all capabilities derived from the argument capability. Revoking
the last capability to a kernel object triggers the \emph{destroy}
operation on the now unreferenced object. This simply cleans up any in-kernel dependencies between
it, other objects and the kernel.
Finally, the \apifunc{seL4\_CNode\_Revoke}{cnode_revoke} method provided by
the \obj{CNode} objects deletes all capabilities derived from the argument
capability. Revoking the last capability to a kernel object triggers the
\emph{destroy} operation on the now unreferenced object. This cleans up any
in-kernel dependencies between it, other objects and the kernel. It does not
necessarily zero all memory state associated with the object yet. Memory zeroing
will happen for the entire region when an untyped capability is \emph{reset} as
part of the first retype operation after all child capabilities have been
revoked.
By calling \apifunc{seL4\_CNode\_Revoke}{cnode_revoke} on the original capability to an untyped memory
object, the user removes all of the untyped memory object's
children---that is, all capabilities pointing to objects in the untyped
memory region. Thus, after this invocation there are no valid references
to any object within the untyped region, and the region may be safely
retyped and reused.
To reuse a region of memory, user code can call
\apifunc{seL4\_CNode\_Revoke}{cnode_revoke} on the original untyped capability
for that region, thereby removing all children of that capability. After this
invocation, no references remain to any object within the untyped region, and
the region may be safely retyped again.
\subsection{Summary of Object Sizes}
\label{sec:object_sizes}