This module exports the class
PrivTCB which all privilege types must
be an instance of. This class is in the TCB since privileges can be
used to bypass label restrictions and untrusted code should not be
allowed to do do arbitrarily. See LIO.Privs for an additional
description of privileges and their role within LIO.
In addition to
PrivTCB this module exports the class
which provides a function from privileges to privilege descriptions.
A privilege description is a meaningful and safe interpretation of a
coresponding privilege (note that the function must be one-to-on).
Privilege descriptions are used in LIO.Gate as "proof" of
privilege ownership. Additionally, privilege descriptions can be used
by TCB code to mint new privileges using the
Zero-method class that imposes a restriction on what code (namely trusted) can make a "privilege type".
Class used to convert a privilege to a privilege description. This is particularly useful when one piece of code wishes to prove ownership of certain privileges without granting the privilege. NOTE: it (almost) always a security violation if the privilege is also the privilege description.
Although this class is not part of the TCB there are some security
implications that should be considered when making a type an
instance of this class. Specifically, if the value constructor for
the privilege description type
d is exported then some
trusted code must be used when "proving" ownership of a certain
privilege. This is generally a good idea even if the constructor is
not made available, since code can (usually) cache such privilege
descriptions. An alternative is to use phantom types to enforce a
The dual of
PrivDesc. This class provides
mintTCB which may
be used to convert, or mint, a privilege descriptions into a
privilege. Of course,
mintTCB must be restricted to the TCB.