LIO.TCB.MLObj

Helper routines for exposing IO operations on objects with mutable labels. The mutable labels are implemented by type MLabel, and have an immutable meta-label (or "label label") protecting the mutable label.

It is reasonable to allow untrusted code to modify labels by exporting a type-restricted version of modifyMLObjLabelP. When this happens, asynchronous exceptions are sent to any other threads inside mblessTCB or mblessPTCB if the new label revokes their access.

Objects with mutable labels

data MLObj policy l object

IO Object with a mutable label. By contrast with LObj, the label on an MLObj can change over time. If this happens, the internal MLabel ensures that threads accessing the object receive an asynchronous exception.

Constructors

MLObjTCB !(MLabel policy l) !object

Instances

MLabelOf MLObj

Methods

mLabelOf :: MLObj policy l a -> MLabel policy l

mlObjTCB :: MLabelPolicyDefault policy => l -> l -> a -> LIO l (MLObj policy l a)

mlObjTCB ll l a creates an MLObj wrapping some IO object a. Here ll is the label on the label, which remains immutable over the lifetime of the MLObj. l is the initial value of the mutable lable.

mlPolicyObjTCB :: policy -> l -> l -> a -> LIO l (MLObj policy l a)

Like mlObjTCB, but create an MLObj with a particular policy value. Note that you don't need to use this for ExternalML and InternalML, as these don't have anything interesting in the policy value, only the type matters. This might be useful if, for instance, you wished to design a new policy type that embeds a clearance.

modifyMLObjLabelP :: (PrivDesc l p, MLabelPolicy policy l) => Priv p -> MLObj policy l a -> (l -> LIO l l) -> LIO l ()

Modify the MLabel within an MLObj.

mblessTCB :: (LabelIO l io lio, Label l) => String -> (a -> io) -> MLObj policy l a -> lio

The MLObj equivalent of blessTCB in LIO.TCB.LObj. Use this for conveniently providing LIO versions of standard IO functions.

mblessPTCB :: (LabelIO l io lio, Label l, PrivDesc l p) => String -> (a -> io) -> Priv p -> MLObj policy l a -> lio

The MLObj equivalent of blessPTCB in LIO.TCB.LObj. Use this for conveniently providing LIO versions of standard IO functions.

Internal details

Mutable labels

data MLabel policy l

A mutable label. Consists of a static label on the label, a mutable label, and a list of threads currently accessing the label. This is intended to be used by privileged code implementing IO abstractions with mutable labels. Routines for accessing such an IO abstraction should perform tne IO from within a call to withMLabelP, to ensure an exception is raised if another thread revokes access with modifyMLabelP.

Constructors

MLabelTCB

Fields

• mlLabelLabel :: !l
• mlLabel :: !(IORef l)
• mlUsers :: !(MVar (Map Unique (l -> IO Bool)))
• mlPolicy :: policy

newMLabelP :: PrivDesc l p => Priv p -> policy -> l -> l -> LIO l (MLabel policy l)

Create an MLabel, performing access control checks to ensure that the labels are within the range allowed given the current label and clearance, and the supplied privileges.

labelOfMlabel :: MLabel policy l -> l

Returns the immutable label that controls access to the mutable label value of an MLabel.

readMLabelP :: PrivDesc l p => Priv p -> MLabel policy l -> LIO l l

Retreive a snapshot of the value of a mutable label. Of course, it may already have changed by the time you process it.

withMLabelP :: PrivDesc l p => Priv p -> MLabel policy l -> LIO l a -> LIO l a

Run an action that should be protected by a mutable label. An exception is thrown if the invoking thread cannot write to the mutable label given the privileges. No attempt is made to adjust the current label, even if doing so would make the permissions acceptable.

Note that if the label changes after this function has been invoked, an exception may be raised in the middle of the protected action.

modifyMLabelP :: (PrivDesc l p, MLabelPolicy policy l) => Priv p -> MLabel policy l -> (l -> LIO l l) -> LIO l ()

Change the mutable label in an MLabel. Raises asynchronous exceptions in other threads that are inside withMLabelP if the new label revokes their access.

class MLabelOf t where

Class of objects with mutable labels.

Minimal complete definition

mLabelOf

Methods

mLabelOf :: t policy l a -> MLabel policy l

Instances

MLabelOf MLObj

Methods

mLabelOf :: MLObj policy l a -> MLabel policy l

MLabel modificaton policies

class MLabelPolicyDefault policy where

Class for MLabelPolicys that don't encode any interesting values. This allows mlObjTCB to create an MLObj without requiring a policy argument.

Minimal complete definition

mlabelPolicyDefault

Methods

mlabelPolicyDefault :: policy

Instances

MLabelPolicyDefault ExternalML

Methods

mlabelPolicyDefault :: ExternalML

MLabelPolicyDefault InternalML

Methods

mlabelPolicyDefault :: InternalML

class MLabelPolicy policy l where

Class of policies for when it is permissible to update an MLabel.

Minimal complete definition

mlabelPolicy

Methods

mlabelPolicy :: PrivDesc l p => policy -> p -> l -> l -> LIO l ()

Instances

MLabelPolicy ExternalML l

Methods

mlabelPolicy :: PrivDesc l p => ExternalML -> p -> l -> l -> LIO l ()

MLabelPolicy InternalML l

Methods

mlabelPolicy :: PrivDesc l p => InternalML -> p -> l -> l -> LIO l ()

data InternalML

InternalML is for objects contained entirely within Haskell, such as a variable. Raising the label can't cause data to leak.

Constructors

InternalML

Instances

Show InternalML

Methods

showsPrec :: Int -> InternalML -> ShowS

show :: InternalML -> String

showList :: [InternalML] -> ShowS

MLabelPolicyDefault InternalML

Methods

mlabelPolicyDefault :: InternalML

MLabelPolicy InternalML l

Methods

mlabelPolicy :: PrivDesc l p => InternalML -> p -> l -> l -> LIO l ()

data ExternalML

ExternalML is for objects that communicate to the outside world, where extra privileges are required since once data gets out, so as to vouch for the fact that the other end of a socket won't arbitrarily downgrade data.

Constructors

ExternalML

Instances

Show ExternalML

Methods

showsPrec :: Int -> ExternalML -> ShowS

show :: ExternalML -> String

showList :: [ExternalML] -> ShowS

MLabelPolicyDefault ExternalML

Methods

mlabelPolicyDefault :: ExternalML

MLabelPolicy ExternalML l

Methods

mlabelPolicy :: PrivDesc l p => ExternalML -> p -> l -> l -> LIO l ()

Helper class for variadic lifting

class LabelIO l io lio | l io -> lio where

Takes a liftIO-like function and an IO function of an arbitrary number of arguments (up to 10). Applies the arguments to the IO function, then passed the result to its argument funciton to transform it into an LIO function.

Minimal complete definition

labelIO

Methods

labelIO :: (forall r. IO r -> LIO l r) -> io -> lio

Instances

LabelIO l (IO r) (LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> IO r -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> (a1 -> a2 -> a3 -> a4 -> a5 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> IO r) (a1 -> a2 -> a3 -> a4 -> LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> (a1 -> a2 -> a3 -> a4 -> IO r) -> a1 -> a2 -> a3 -> a4 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> IO r) (a1 -> a2 -> a3 -> LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> (a1 -> a2 -> a3 -> IO r) -> a1 -> a2 -> a3 -> LIO l r

LabelIO l (a1 -> a2 -> IO r) (a1 -> a2 -> LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> (a1 -> a2 -> IO r) -> a1 -> a2 -> LIO l r

LabelIO l (a1 -> IO r) (a1 -> LIO l r)

Methods

labelIO :: (forall a. IO a -> LIO l a) -> (a1 -> IO r) -> a1 -> LIO l r