LIO.TCB.LObj

This module provides routines for safely exposing IO functions in the LIO monad. At a high level, certain IO objects such as handles can be associated with a label via LObj, while certain operations can then be blessed (via blessTCB) to operate on such LObj objects.

For example, trusted code might define the following:

 import qualified System.IO as IO
 
 type Handle = LObj DCLabel IO.Handle
 
 hPutStrLn :: LObj DCLabel IO.Handle -> String -> LIO DCLabel ()
 hPutStrLn h = blessTCB "hPutStrLn" IO.hPutStrLn h

 hPutStrLnP :: DCPriv -> LObj DCLabel IO.Handle -> String -> LIO DCLabel ()
 hPutStrLnP h = blessPTCB "hPutStrLnP" IO.hPutStrLn h
 
 hGetLine :: LObj DCLabel IO.Handle -> LIO DCLabel String
 hGetLine h = blessTCB "hGetLine" IO.hGetLine h

Then application-specific trusted code can wrap a specific label around each Handle using the LObjTCB constructor.

Documentation

data LObj label object

A "LObj label object" is a wrapper around an IO abstraction of type object (such as a file handle or socket) on which it is safe to do IO operations in the LIO monad when the caller can read and write a the label label. It is the job of the trusted code constructing such a LObj object to ensure both that the same IO object is only ever associated with a single label, and that the abstraction combined with its blessed IO operations (see blessTCB) cannot be used to communicate with code running at different labels.

Constructors

LObjTCB !label !object

Instances

Typeable2 LObj

LabelOf LObj

(Label l, Show t) => ShowTCB (LObj l t)

blessTCB :: (GuardIO l io lio, Label l) => String -> (a -> io) -> LObj l a -> lio

This function can be used to turn an IO function into an LIO one. The LIO version expects a LObj argument, and before performing any IO uses guardWrite to check that the current label can write the label in the LObj object.

The first argument should be the name of the function being defined with blessTCB. Its purpose is to enhance error reporting.

Note that io and lio are function types (of up to nine arguments), which must be the same in all types except the monad. For example, if io is Int -> String -> IO (), then lio must be Int -> String -> LIO l ().

blessPTCB :: (GuardIO l io lio, PrivDesc l p) => String -> (a -> io) -> Priv p -> LObj l a -> lio

A variant of blessTCB that produces an LIO function taking a privilege argument.

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

Class for lifting IO actions.

Methods

guardIOTCB :: LIO l () -> io -> lio

Lifts an IO action in the LIO monad, executing a guard before calling the function.

Instances

GuardIO l (IO r) (LIO l r)

GuardIO 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)

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

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

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

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

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

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

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

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

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