CapRef

Overview

The Grasshopper kernel enforces the protection of system services through the use of a segregated capability system. Services are only performed if the calling locus has access to a capability which permits the request. A locus is defined to have access to all capabilities owned by itself and its host container. Since these capabilities are intangible, a locus is only able to refer to them via a special type called a CapRef.

A CapRef consists of two parts. One part is a flag that controls whether the CapRef refers to a capability owned by the locus or by its host container. The other part is an index into a table of capabilities. When the kernel sees a CapRef, it uses the flag to decide which table the capability is in, and the index to extract the capability from the table.

It is not possible for a locus to present the kernel with arbitrary bit patterns under the guise of a CapRef and gain access to capabilities that it doesn't own since the kernel's interpretation of a CapRef does not permit otherwise. The worst that could happen is that a locus could construct a CapRef with an index that refers to an invalid table entry. The kernel detects this case and aborts the requested operation.

Signatures

#include <libc.h>
CAPREF_LOCUS
CAPREF_CONT
capref(type,index)
capref_type(capref)
capref_index(capref)

Semantics

C programs wishing to make use of CapRefs should include the standard header file libc.h. This file defines several macros useful for constructing and manipulating capabilities. These macros are listed above and are used as follows.

CAPREF_LOCUS and CAPREF_CONT are manifest constants and represent the type of a CapRef. The first is for referring to capabilities owned by a locus. The second is for referring to capabilities owned by a locus' host container.

The macro capref is used to construct CapRefs. The first argument must be either CAPREF_LOCUS or CAPREF_CONT and determines the type of the CapRef that is constructed. The second argument must be a non-negative integer and specifies an index into the table of capabilities determined (indirectly) by the first argument.

The macro capref_type is used to determine the type of the CapRef that is its argument. The resulting expression will be equal to either CAPREF_LOCUS or CAPREF_CONT.

The macro capref_index is used to determine the index of the capability referred to by the CapRef that is its argument. The resulting expression will be a non-negative integer value.