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 IO.hPutStrLn noPrivs h
 
 hGetLine :: LObj DCLabel IO.Handle -> LIO DCLabel String
 hGetLine h = blessTCB IO.hGetLine noPrivs h

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

Documentation

data LObj label object

Constructors

LObjTCB !label !object

Instances

Typeable2 LObj

LabelOf LObj

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

blessTCB :: (GuardIO l io lio, Label l) => (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.

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) => (a -> io) -> Priv p -> LObj l a -> lio

A variant of blessTCB that takes a privilege argument.

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

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)