-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Labeled IO Information Flow Control Library
--
-- The Labeled IO (LIO) library provides information flow control
-- for incorporating untrusted code within Haskell applications. Most
-- code should import module LIO.LIO and whichever label type the
-- application is using (e.g., LIO.DCLabel). The core
-- functionality of the library is documented in LIO.TCB. LIO was
-- implemented by David Mazieres
-- (http://www.scs.stanford.edu/~dm/), Deian Stefan
-- (http://www.scs.stanford.edu/~deian/), Alejandro Russo
-- (http://www.cse.chalmers.se/~russo/) and John C. Mitchell
-- (http://www.stanford.edu/~jcm/). The extended version of our
-- paper, that includes the proofs is available here:
-- http://www.scs.stanford.edu/~deian/pubs/stefan:2011:flexible-ext.pdf.
-- The library depends on the DCLabel module. You can read more
-- on DC Labels here:
-- http://www.scs.stanford.edu/~deian/dclabels/.
@package lio
@version 0.0.2
-- | This module generalizes throw and catch (from
-- Control.Exception) to methods that can be defined on multiple
-- Monads.
module LIO.MonadCatch
-- | MonadCatch is the class used to generalize the standard IO
-- catch and throwIO functions to methods that can be
-- defined in multiple monads.
class Monad m => MonadCatch m
block :: MonadCatch m => m a -> m a
unblock :: MonadCatch m => m a -> m a
throwIO :: (MonadCatch m, Exception e) => e -> m a
catch :: (MonadCatch m, Exception e) => m a -> (e -> m a) -> m a
handle :: (MonadCatch m, Exception e) => (e -> m a) -> m a -> m a
onException :: MonadCatch m => m a -> m b -> m a
bracket :: MonadCatch m => m b -> (b -> m c) -> (b -> m a) -> m a
genericBracket :: MonadCatch m => (m b -> m c -> m b) -> m a -> (a -> m c) -> (a -> m b) -> m b
instance [safe] MonadCatch IO
-- | This module implements the core of the Labeled IO library for
-- information flow control in Haskell. It provides a monad, LIO,
-- that is intended to be used as a replacement for the IO monad in
-- untrusted code. The idea is for untrusted code to provide a
-- computation in the LIO monad, which trusted code can then
-- safely execute through the evalLIO function. (Though usually a
-- wrapper function is employed depending on the type of labels used by
-- an application. For example, with LIO.DCLabel, you would use
-- evalDC to execute an untrusted computation, and with
-- LIO.HiStar labels, the function is evalHS. There are
-- also abbreviations for the LIO monad type of a particular
-- label--for instance DC or HS.)
--
-- A data structure Labeled (labeled value) protects access to
-- pure values. Without the appropriate privileges, one cannot produce a
-- pure value that depends on a secret Labeled, or conversely
-- produce a high-integrity Labeled based on pure data. The
-- function toLabeled allows one to seal off the results of an LIO
-- computation inside an Labeled without tainting the current flow
-- of execution. unlabel conversely allows one to use the value
-- stored within a Labeled.
--
-- Any code that imports this module is part of the Trusted Computing
-- Base (TCB) of the system. Hence, untrusted code must be prevented
-- from importing this module. The exported symbols ending
-- ...TCB can be used to violate label protections even from
-- within pure code or the LIO Monad. A safe subset of these symbols is
-- exported by the LIO.Base module, which is how untrusted code
-- should access the core label functionality. (LIO.Base is also
-- re-exported by LIO.LIO, the main gateway to this library.)
module LIO.TCB
data POrdering
-- | Equal
PEQ :: POrdering
-- | Less than
PLT :: POrdering
-- | Greater than
PGT :: POrdering
-- | Incomparable (neither less than nor greater than)
PNE :: POrdering
class Eq a => POrd a
pcompare :: POrd a => a -> a -> POrdering
leq :: POrd a => a -> a -> Bool
o2po :: Ordering -> POrdering
class (POrd a, Show a, Read a, Typeable a) => Label a
lbot :: Label a => a
ltop :: Label a => a
lub :: Label a => a -> a -> a
glb :: Label a => a -> a -> a
class (Label l, Monoid p, PrivTCB p) => Priv l p
leqp :: Priv l p => p -> l -> l -> Bool
lostar :: Priv l p => p -> l -> l -> l
-- | A generic Priv instance that works for all Labels and
-- confers no downgrading privileges.
data NoPrivs
NoPrivs :: NoPrivs
data Label l => LIO l s a
-- | Returns the current value of the thread's label.
getLabel :: Label l => LIO l s l
-- | If the current label is oldLabel and the current clearance is
-- clearance, this function allows code to raise the label to
-- any value newLabel such that oldLabel `leq`
-- newLabel && newLabel `leq` clearance. Note that
-- there is no setLabel variant without the ...P
-- because the taint function provides essentially the same
-- functionality that setLabel would.
setLabelP :: Priv l p => p -> l -> LIO l s ()
-- | Returns the current value of the thread's clearance.
getClearance :: Label l => LIO l s l
-- | Reduce the current clearance. One cannot raise the current label or
-- create object with labels higher than the current clearance.
lowerClr :: Label l => l -> LIO l s ()
-- | Raise the current clearance (undoing the effects of lowerClr).
-- This requires privileges.
lowerClrP :: Priv l p => p -> l -> LIO l s ()
-- | Lowers the clearance of a computation, then restores the clearance to
-- its previous value. Useful to wrap around a computation if you want to
-- be sure you can catch exceptions thrown by it. Also useful to wrap
-- around toLabeled to ensure that the computation does not access
-- data exceeding a particular label. If withClearance is given
-- a label that can't flow to the current clearance, then the clearance
-- is lowered to the greatest lower bound of the label supplied and the
-- current clearance.
--
-- Note that if the computation inside withClearance acquires
-- any Privs, it may still be able to raise its clearance above
-- the supplied argument using lowerClrP.
withClearance :: Label l => l -> LIO l s a -> LIO l s a
-- | Use taint l in trusted code before observing an object
-- labeled l. This will raise the current label to a value
-- l' such that l `leq` l', or throw
-- LerrClearance if l' would have to be higher
-- than the current clearance.
taint :: Label l => l -> LIO l s ()
-- | Like taint, but use privileges to reduce the amount of taint
-- required. Note that unlike setLabelP, taintP will
-- never lower the current label. It simply uses privileges to avoid
-- raising the label as high as taint would raise it.
taintP :: Priv l p => p -> l -> LIO l s ()
-- | Use wguard l in trusted code before modifying an object
-- labeled l. If l' is the current label, then this
-- function ensures that l' `leq` l before doing the same
-- thing as taint l. Throws LerrHigh if
-- the current label l' is too high.
wguard :: Label l => l -> LIO l s ()
-- | Like wguard, but takes privilege argument to be more
-- permissive.
wguardP :: Priv l p => p -> l -> LIO l s ()
-- | Ensures the label argument is between the current IO label and current
-- IO clearance. Use this function in code that allocates
-- objects--untrusted code shouldn't be able to create an object labeled
-- l unless aguard l does not throw an exception.
aguard :: Label l => l -> LIO l s ()
-- | Like aguardP, but takes privilege argument to be more
-- permissive.
aguardP :: Priv l p => p -> l -> LIO l s ()
-- | Labeled is a type representing labeled data.
data Label l => Labeled l t
-- | Function to construct an Labeled from a label and pure value.
-- If the current label is lcurrent and the current clearance is
-- ccurrent, then the label l specified must satisfy
-- lcurrent `leq` l && l `leq` ccurrent.
label :: Label l => l -> a -> LIO l s (Labeled l a)
-- | Constructs an Labeled using privilege to allow the
-- Labeled's label to be below the current label. If the current
-- label is lcurrent and the current clearance is
-- ccurrent, then the privilege p and label l
-- specified must satisfy (leqp p lcurrent l) && l
-- `leq` ccurrent. Note that privilege is not used to bypass
-- the clearance. You must use lowerClrP to raise the clearance
-- first if you wish to create an Labeled at a higher label than
-- the current clearance.
labelP :: Priv l p => p -> l -> a -> LIO l s (Labeled l a)
-- | Within the LIO monad, this function takes an Labeled and
-- returns the value. Thus, in the LIO monad one can say:
--
--
-- x <- unlabel (xv :: Labeled SomeLabelType Int)
--
--
-- And now it is possible to use the value of x, which is the
-- pure value of what was stored in xv. Of course,
-- unlabel also raises the current label. If raising the label
-- would exceed the current clearance, then unlabel throws
-- LerrClearance. However, you can use labelOf to check if
-- unlabel will suceed without throwing an exception.
unlabel :: Label l => Labeled l a -> LIO l s a
-- | Extracts the value of an Labeled just like unlabel, but
-- takes a privilege argument to minimize the amount the current label
-- must be raised. Will still throw LerrClearance under the same
-- circumstances as unlabel.
unlabelP :: Priv l p => p -> Labeled l a -> LIO l s a
-- | toLabeled is the dual of unlabel. It allows one to
-- invoke computations that would raise the current label, but without
-- actually raising the label. Instead, the result of the computation is
-- packaged into a Labeled with a supplied label. Thus, to get at
-- the result of the computation one will have to call unlabel and
-- raise the label, but this can be postponed, or done inside some other
-- call to toLabeled. This suggestst that the provided label must
-- be above the current label and below the current clearance.
--
-- Note that toLabeled always restores the clearance to whatever
-- it was when it was invoked, regardless of what occured in the
-- computation producing the value of the Labeled. This higlights
-- one main use of clearance: to ensure that a Labeled computed
-- does not exceed a particular label.
toLabeled :: Label l => l -> LIO l s a -> LIO l s (Labeled l a)
toLabeledP :: Priv l p => p -> l -> LIO l s a -> LIO l s (Labeled l a)
-- | Executes a computation that would raise the current label, but
-- discards the result so as to keep the label the same. Used when one
-- only cares about the side effects of a computation. For instance, if
-- log_handle is an LHandle with a high label, one can
-- execute
--
--
-- discard ltop $ hputStrLn log_handle "Log message"
--
--
-- to create a log message without affecting the current label. (Of
-- course, if log_handle is closed and this throws an exception,
-- it may not be possible to catch the exception within the LIO
-- monad without sufficient privileges--see catchP.)
discard :: Label l => l -> LIO l s a -> LIO l s ()
-- | Returns label of a Label type.
labelOf :: Label l => Labeled l a -> l
-- | Raises the label of a Labeled to the lub of it's current
-- label and the value supplied. The label supplied must be less than the
-- current clarance, though the resulting label may not be if the
-- Labeled is already above the current thread's clearance.
taintLabeled :: Label l => l -> Labeled l a -> LIO l s (Labeled l a)
data LabelFault
-- | Requested label too low
LerrLow :: LabelFault
-- | Current label too high
LerrHigh :: LabelFault
-- | Label would exceed clearance
LerrClearance :: LabelFault
-- | Insufficient privileges
LerrPriv :: LabelFault
-- | Invalid request
LerrInval :: LabelFault
-- | MonadCatch is the class used to generalize the standard IO
-- catch and throwIO functions to methods that can be
-- defined in multiple monads.
class Monad m => MonadCatch m
block :: MonadCatch m => m a -> m a
unblock :: MonadCatch m => m a -> m a
throwIO :: (MonadCatch m, Exception e) => e -> m a
catch :: (MonadCatch m, Exception e) => m a -> (e -> m a) -> m a
handle :: (MonadCatch m, Exception e) => (e -> m a) -> m a -> m a
onException :: MonadCatch m => m a -> m b -> m a
bracket :: MonadCatch m => m b -> (b -> m c) -> (b -> m a) -> m a
-- | Catches an exception, so long as the label at the point where the
-- exception was thrown can flow to the label at which catchP is invoked,
-- modulo the privileges specified. Note that the handler receives an an
-- extra first argument (before the exception), which is the label when
-- the exception was thrown.
catchP :: (Label l, Exception e, Priv l p) => p -> LIO l s a -> (l -> e -> LIO l s a) -> LIO l s a
-- | Version of catchP with arguments swapped.
handleP :: (Label l, Exception e, Priv l p) => p -> (l -> e -> LIO l s a) -> LIO l s a -> LIO l s a
-- | onException cannot run its handler if the label was raised in
-- the computation that threw the exception. This variant allows
-- privileges to be supplied, so as to catch exceptions thrown with a
-- raised label.
onExceptionP :: Priv l p => p -> LIO l s a -> LIO l s b -> LIO l s a
-- | Like standard bracket, but with privileges to downgrade
-- exception.
bracketP :: Priv l p => p -> LIO l s a -> (a -> LIO l s c) -> (a -> LIO l s b) -> LIO l s b
-- | Evaluate in LIO.
evaluate :: Label l => a -> LIO l s a
-- | Produces an IO computation that will execute a particular
-- LIO computation. Because untrusted code cannot execute
-- IO computations, this function should only be useful within
-- trusted code. No harm is done from exposing the evalLIO
-- symbol to untrusted code. (In general, untrusted code is free to
-- produce IO computations--it just can't execute them without
-- access to ioTCB.)
evalLIO :: Label l => LIO l s a -> s -> IO (a, l)
data Label l => LIOstate l s
LIOstate :: s -> l -> l -> LIOstate l s
labelState :: LIOstate l s -> s
lioL :: LIOstate l s -> l
lioC :: LIOstate l s -> l
-- | Execute an LIO action.
runLIO :: Label l => LIO l s a -> LIOstate l s -> IO (a, LIOstate l s)
-- | It would be a security issue to make certain objects a member of the
-- Show class, but nonetheless it is useful to be able to examine
-- such objects from within the debugger. The showTCB method can
-- be used to examine such objects.
class ShowTCB a
showTCB :: ShowTCB a => a -> String
-- | It is useful to have the dual of ShowTCB, ReadTCB,
-- that allows for the reading of Labeleds that were written using
-- showTCB. Only readTCB (corresponding to read)
-- and readsPrecTCB (corresponding to readsPrec) are
-- implemented.
class ReadTCB a
readsPrecTCB :: ReadTCB a => Int -> ReadS a
readTCB :: ReadTCB a => String -> a
labelTCB :: Label l => l -> a -> Labeled l a
-- | PrivTCB is a method-less class whose only purpose is to be
-- unavailable to unprivileged code. Since (PrivTCB t) => is
-- in the context of class Priv and unprivileged code cannot
-- create new instances of the PrivTCB class, this ensures
-- unprivileged code cannot create new instances of the Priv class
-- either, even though the symbol Priv is exported by
-- LIO.Base and visible to untrusted code.
class PrivTCB t
class MintTCB t i
mintTCB :: MintTCB t i => i -> t
-- | Extracts the value from an Labeled, discarding the label and
-- any protection.
unlabelTCB :: Label l => Labeled l a -> a
-- | Set the current label to anything, with no security check.
setLabelTCB :: Label l => l -> LIO l s ()
-- | Set the current clearance to anything, with no security check.
lowerClrTCB :: Label l => l -> LIO l s ()
-- | Returns label-specific state of the LIO monad. This is the data
-- specified as the second argument of evalLIO, whose type is
-- s in the monad LIO l s.
getTCB :: Label l => LIO l s s
-- | Sets the label-specific state of the LIO monad. See
-- getTCB.
putTCB :: Label l => s -> LIO l s ()
-- | Lifts an IO computation into the LIO monad. Note that
-- exceptions thrown within the IO computation cannot directly be
-- caught within the LIO computation. Thus, if you are not inside
-- a rethrowTCB block, you will generally want to use
-- rtioTCB instead of ioTCB.
ioTCB :: Label l => IO a -> LIO l s a
-- | Lifts an IO computation into the LIO monad. If the
-- IO computation throws an exception, it labels the exception
-- with the current label so that the exception can be caught with
-- catch or catchP. This function's name stands for
-- "re-throw io", because the functionality is a combination of
-- rethrowTCB and ioTCB. Effectively
--
--
-- rtioTCB = rethrowTCB . ioTCB
--
rtioTCB :: Label l => IO a -> LIO l s a
-- | Privileged code that does IO operations may cause exceptions that
-- should be caught by untrusted code in the LIO monad. Such
-- operations should be wrapped by rethrowTCB (or
-- rtioTCB, which uses rethrowTCB) to ensure the
-- exception is labeled. Note that it is very important that the
-- computation executed inside rethrowTCB not in any way change
-- the label, as otherwise rethrowTCB would put the wrong label
-- on the exception.
rethrowTCB :: Label l => LIO l s a -> LIO l s a
-- | For privileged code that needs to catch all exceptions in some cleanup
-- function. Note that for the LIO monad, these methods do
-- not call rethrowTCB to label the exceptions. It is
-- assumed that you will use rtioTCB instead of ioTCB for
-- IO within the computation arguments of these methods.
class MonadCatch m => OnExceptionTCB m
onExceptionTCB :: OnExceptionTCB m => m a -> m b -> m a
bracketTCB :: OnExceptionTCB m => m a -> (a -> m c) -> (a -> m b) -> m b
-- | Generate a fresh state to pass runLIO when invoking it for the
-- first time.
newstate :: Label l => s -> LIOstate l s
instance Typeable LabelFault
instance Typeable1 LabeledExceptionTCB
instance Eq POrdering
instance Ord POrdering
instance Show POrdering
instance Functor (LIO l s)
instance Monad (LIO l s)
instance MonadFix (LIO l s)
instance Show LabelFault
instance Label l => MonadError IOException (LIO l s)
instance Label l => OnExceptionTCB (LIO l s)
instance OnExceptionTCB IO
instance Label l => MonadCatch (LIO l s)
instance Label l => Exception (LabeledExceptionTCB l)
instance Label l => Show (LabeledExceptionTCB l)
instance Exception LabelFault
instance Label l => Priv l NoPrivs
instance Monoid NoPrivs
instance PrivTCB NoPrivs
instance (Label l, Read l, Read a) => ReadTCB (Labeled l a)
instance (Label l, Show a) => ShowTCB (Labeled l a)
instance Label l => Functor (Labeled l)
instance Monoid POrdering
-- | This module provides bindings for the DCLabel module, with
-- some renaming to resolve name clashes. The delegation of privilege and
-- other trusted code is not exported by this module and code wishing to
-- use this should import DCLabel.TCB.
module LIO.DCLabel
-- | A DCLabel category set.
type DCCatSet = Label
-- | A DCLabel (untrusted) privilege.
type DCPriv = Priv
-- | A DCLabel privilege.
type DCPrivTCB = TCBPriv
-- | The type for Labeled values uinsg DCLabel as the label.
type DCLabeled a = Labeled DCLabel a
-- | The monad for LIO computations using DCLabel as the label.
type DC = LIO DCLabel ()
-- | Runs a computation in the LIO Monad, returning both the computation's
-- result and the label of the result.
evalDC :: DC a -> IO (a, DCLabel)
instance Typeable DCLabel
instance Typeable Label
instance Typeable Conj
instance Typeable Disj
instance Priv DCLabel TCBPriv
instance MintTCB TCBPriv Principal
instance MintTCB TCBPriv Priv
instance PrivTCB TCBPriv
instance Label DCLabel
instance POrd DCLabel
-- | This module provides a function liftLIO for executing
-- LIO computations from transformed versions of the LIO
-- monad. There is also a method liftIO, which is a synonym for
-- liftLIO, to help with porting code that expects to run in the
-- IO monad.
module LIO.MonadLIO
class (Monad m, Label l) => MonadLIO m l s | m -> l s
liftLIO :: MonadLIO m l s => LIO l s a -> m a
liftIO :: MonadLIO m l s => LIO l s a -> m a
instance [overlap ok] (MonadLIO m l s, MonadTrans t, Monad (t m)) => MonadLIO (t m) l s
instance [overlap ok] Label l => MonadLIO (LIO l s) l s
-- | This module implements labeled IORefs. The interface is analogous to
-- Data.IORef, but the operations take place in the LIO monad.
-- Moreover, reading the LIORef calls taint, while writing it calls
-- wguard.
module LIO.LIORef.TCB
data LIORef l a
newLIORef :: Label l => l -> a -> LIO l s (LIORef l a)
labelOfLIORef :: Label l => LIORef l a -> l
readLIORef :: Label l => LIORef l a -> LIO l s a
writeLIORef :: Label l => LIORef l a -> a -> LIO l s ()
atomicModifyLIORef :: Label l => LIORef l a -> (a -> (a, b)) -> LIO l s b
newLIORefP :: Priv l p => p -> l -> a -> LIO l s (LIORef l a)
readLIORefP :: Priv l p => p -> LIORef l a -> LIO l s a
writeLIORefP :: Priv l p => p -> LIORef l a -> a -> LIO l s ()
atomicModifyLIORefP :: Priv l p => p -> LIORef l a -> (a -> (a, b)) -> LIO l s b
newLIORefTCB :: Label l => l -> a -> LIO l s (LIORef l a)
readLIORefTCB :: Label l => LIORef l a -> LIO l s a
writeLIORefTCB :: Label l => LIORef l a -> a -> LIO l s ()
atomicModifyLIORefTCB :: Label l => LIORef l a -> (a -> (a, b)) -> LIO l s b
-- | This module exports the safe subset of the LIO.LIORef.TCB
-- module. It is important that untrusted code be limited to this subset;
-- information flow can easily be violated if the TCB functions are
-- exported.
module LIO.LIORef.Safe
-- | This module implements labeled IORefs. The interface is analogous to
-- Data.IORef, but the operations take place in the LIO monad.
-- Moreover, reading the LIORef calls taint, while writing it calls
-- wguard. This module exports only the safe subset (non TCB) of the
-- LIORef module -- trusted code can import LIO.LIORef.TCB.
module LIO.LIORef
-- | This file exports the subset of symbols in the LIO.TCB module
-- that are safe for untrusted code to access. See the LIO.TCB
-- module for documentation.
module LIO.Base
data POrdering
-- | Equal
PEQ :: POrdering
-- | Less than
PLT :: POrdering
-- | Greater than
PGT :: POrdering
-- | Incomparable (neither less than nor greater than)
PNE :: POrdering
class Eq a => POrd a
pcompare :: POrd a => a -> a -> POrdering
leq :: POrd a => a -> a -> Bool
o2po :: Ordering -> POrdering
class (POrd a, Show a, Read a, Typeable a) => Label a
lbot :: Label a => a
ltop :: Label a => a
lub :: Label a => a -> a -> a
glb :: Label a => a -> a -> a
class (Label l, Monoid p, PrivTCB p) => Priv l p
leqp :: Priv l p => p -> l -> l -> Bool
lostar :: Priv l p => p -> l -> l -> l
-- | A generic Priv instance that works for all Labels and
-- confers no downgrading privileges.
data NoPrivs
NoPrivs :: NoPrivs
data Label l => LIO l s a
-- | Returns the current value of the thread's label.
getLabel :: Label l => LIO l s l
-- | If the current label is oldLabel and the current clearance is
-- clearance, this function allows code to raise the label to
-- any value newLabel such that oldLabel `leq`
-- newLabel && newLabel `leq` clearance. Note that
-- there is no setLabel variant without the ...P
-- because the taint function provides essentially the same
-- functionality that setLabel would.
setLabelP :: Priv l p => p -> l -> LIO l s ()
-- | Returns the current value of the thread's clearance.
getClearance :: Label l => LIO l s l
-- | Reduce the current clearance. One cannot raise the current label or
-- create object with labels higher than the current clearance.
lowerClr :: Label l => l -> LIO l s ()
-- | Raise the current clearance (undoing the effects of lowerClr).
-- This requires privileges.
lowerClrP :: Priv l p => p -> l -> LIO l s ()
-- | Lowers the clearance of a computation, then restores the clearance to
-- its previous value. Useful to wrap around a computation if you want to
-- be sure you can catch exceptions thrown by it. Also useful to wrap
-- around toLabeled to ensure that the computation does not access
-- data exceeding a particular label. If withClearance is given
-- a label that can't flow to the current clearance, then the clearance
-- is lowered to the greatest lower bound of the label supplied and the
-- current clearance.
--
-- Note that if the computation inside withClearance acquires
-- any Privs, it may still be able to raise its clearance above
-- the supplied argument using lowerClrP.
withClearance :: Label l => l -> LIO l s a -> LIO l s a
-- | Use taint l in trusted code before observing an object
-- labeled l. This will raise the current label to a value
-- l' such that l `leq` l', or throw
-- LerrClearance if l' would have to be higher
-- than the current clearance.
taint :: Label l => l -> LIO l s ()
-- | Like taint, but use privileges to reduce the amount of taint
-- required. Note that unlike setLabelP, taintP will
-- never lower the current label. It simply uses privileges to avoid
-- raising the label as high as taint would raise it.
taintP :: Priv l p => p -> l -> LIO l s ()
-- | Use wguard l in trusted code before modifying an object
-- labeled l. If l' is the current label, then this
-- function ensures that l' `leq` l before doing the same
-- thing as taint l. Throws LerrHigh if
-- the current label l' is too high.
wguard :: Label l => l -> LIO l s ()
-- | Like wguard, but takes privilege argument to be more
-- permissive.
wguardP :: Priv l p => p -> l -> LIO l s ()
-- | Ensures the label argument is between the current IO label and current
-- IO clearance. Use this function in code that allocates
-- objects--untrusted code shouldn't be able to create an object labeled
-- l unless aguard l does not throw an exception.
aguard :: Label l => l -> LIO l s ()
-- | Like aguardP, but takes privilege argument to be more
-- permissive.
aguardP :: Priv l p => p -> l -> LIO l s ()
-- | Labeled is a type representing labeled data.
data Label l => Labeled l t
-- | Function to construct an Labeled from a label and pure value.
-- If the current label is lcurrent and the current clearance is
-- ccurrent, then the label l specified must satisfy
-- lcurrent `leq` l && l `leq` ccurrent.
label :: Label l => l -> a -> LIO l s (Labeled l a)
-- | Constructs an Labeled using privilege to allow the
-- Labeled's label to be below the current label. If the current
-- label is lcurrent and the current clearance is
-- ccurrent, then the privilege p and label l
-- specified must satisfy (leqp p lcurrent l) && l
-- `leq` ccurrent. Note that privilege is not used to bypass
-- the clearance. You must use lowerClrP to raise the clearance
-- first if you wish to create an Labeled at a higher label than
-- the current clearance.
labelP :: Priv l p => p -> l -> a -> LIO l s (Labeled l a)
-- | Within the LIO monad, this function takes an Labeled and
-- returns the value. Thus, in the LIO monad one can say:
--
--
-- x <- unlabel (xv :: Labeled SomeLabelType Int)
--
--
-- And now it is possible to use the value of x, which is the
-- pure value of what was stored in xv. Of course,
-- unlabel also raises the current label. If raising the label
-- would exceed the current clearance, then unlabel throws
-- LerrClearance. However, you can use labelOf to check if
-- unlabel will suceed without throwing an exception.
unlabel :: Label l => Labeled l a -> LIO l s a
-- | Extracts the value of an Labeled just like unlabel, but
-- takes a privilege argument to minimize the amount the current label
-- must be raised. Will still throw LerrClearance under the same
-- circumstances as unlabel.
unlabelP :: Priv l p => p -> Labeled l a -> LIO l s a
-- | toLabeled is the dual of unlabel. It allows one to
-- invoke computations that would raise the current label, but without
-- actually raising the label. Instead, the result of the computation is
-- packaged into a Labeled with a supplied label. Thus, to get at
-- the result of the computation one will have to call unlabel and
-- raise the label, but this can be postponed, or done inside some other
-- call to toLabeled. This suggestst that the provided label must
-- be above the current label and below the current clearance.
--
-- Note that toLabeled always restores the clearance to whatever
-- it was when it was invoked, regardless of what occured in the
-- computation producing the value of the Labeled. This higlights
-- one main use of clearance: to ensure that a Labeled computed
-- does not exceed a particular label.
toLabeled :: Label l => l -> LIO l s a -> LIO l s (Labeled l a)
toLabeledP :: Priv l p => p -> l -> LIO l s a -> LIO l s (Labeled l a)
-- | Executes a computation that would raise the current label, but
-- discards the result so as to keep the label the same. Used when one
-- only cares about the side effects of a computation. For instance, if
-- log_handle is an LHandle with a high label, one can
-- execute
--
--
-- discard ltop $ hputStrLn log_handle "Log message"
--
--
-- to create a log message without affecting the current label. (Of
-- course, if log_handle is closed and this throws an exception,
-- it may not be possible to catch the exception within the LIO
-- monad without sufficient privileges--see catchP.)
discard :: Label l => l -> LIO l s a -> LIO l s ()
-- | Returns label of a Label type.
labelOf :: Label l => Labeled l a -> l
-- | Raises the label of a Labeled to the lub of it's current
-- label and the value supplied. The label supplied must be less than the
-- current clarance, though the resulting label may not be if the
-- Labeled is already above the current thread's clearance.
taintLabeled :: Label l => l -> Labeled l a -> LIO l s (Labeled l a)
data LabelFault
-- | Requested label too low
LerrLow :: LabelFault
-- | Current label too high
LerrHigh :: LabelFault
-- | Label would exceed clearance
LerrClearance :: LabelFault
-- | Insufficient privileges
LerrPriv :: LabelFault
-- | Invalid request
LerrInval :: LabelFault
-- | Catches an exception, so long as the label at the point where the
-- exception was thrown can flow to the label at which catchP is invoked,
-- modulo the privileges specified. Note that the handler receives an an
-- extra first argument (before the exception), which is the label when
-- the exception was thrown.
catchP :: (Label l, Exception e, Priv l p) => p -> LIO l s a -> (l -> e -> LIO l s a) -> LIO l s a
-- | onException cannot run its handler if the label was raised in
-- the computation that threw the exception. This variant allows
-- privileges to be supplied, so as to catch exceptions thrown with a
-- raised label.
onExceptionP :: Priv l p => p -> LIO l s a -> LIO l s b -> LIO l s a
-- | Like standard bracket, but with privileges to downgrade
-- exception.
bracketP :: Priv l p => p -> LIO l s a -> (a -> LIO l s c) -> (a -> LIO l s b) -> LIO l s b
-- | Version of catchP with arguments swapped.
handleP :: (Label l, Exception e, Priv l p) => p -> (l -> e -> LIO l s a) -> LIO l s a -> LIO l s a
-- | Evaluate in LIO.
evaluate :: Label l => a -> LIO l s a
-- | Produces an IO computation that will execute a particular
-- LIO computation. Because untrusted code cannot execute
-- IO computations, this function should only be useful within
-- trusted code. No harm is done from exposing the evalLIO
-- symbol to untrusted code. (In general, untrusted code is free to
-- produce IO computations--it just can't execute them without
-- access to ioTCB.)
evalLIO :: Label l => LIO l s a -> s -> IO (a, l)
module LIO.HiStar
withDefaults :: a -> a -> (a -> a -> b) -> Maybe a -> Maybe a -> b
assocs2 :: Ord k => (Map k v1) -> (Map k v2) -> [(k, Maybe v1, Maybe v2)]
mergeWith :: Ord k => (Maybe a -> Maybe b -> Maybe c) -> Map k a -> Map k b -> Map k c
newtype HSCategory
HSC :: Integer -> HSCategory
data HSLevel
L0 :: HSLevel
L1 :: HSLevel
L2 :: HSLevel
L3 :: HSLevel
data HSLabel
HSL :: (Map HSCategory HSLevel) -> HSLevel -> HSLabel
combineLabel :: (HSLevel -> HSLevel -> HSLevel) -> HSLabel -> HSLabel -> HSLabel
lupdate :: HSLabel -> HSCategory -> HSLevel -> HSLabel
lupdates :: HSLabel -> [HSCategory] -> HSLevel -> HSLabel
lapply :: HSLabel -> HSCategory -> HSLevel
newtype HSPrivs
HSPrivs :: [HSCategory] -> HSPrivs
data HSState
HSState :: IORef HSCategory -> HSState
nextCat :: HSState -> IORef HSCategory
type HS a = LIO HSLabel HSState a
newcat :: HSLevel -> HS (HSPrivs, HSLabel)
evalHS :: HS t -> IO (t, HSLabel)
instance Typeable HSLabel
instance Typeable HSState
instance Eq HSCategory
instance Ord HSCategory
instance Read HSCategory
instance Show HSCategory
instance Eq HSLevel
instance Ord HSLevel
instance Enum HSLevel
instance Read HSLevel
instance Show HSLevel
instance Read HSLabel
instance Show HSLabel
instance Priv HSLabel HSPrivs
instance PrivTCB HSPrivs
instance Monoid HSPrivs
instance Label HSLabel
instance POrd HSLabel
instance Eq HSLabel
instance POrd HSLevel
-- | These functions support a simple base-32 encoding of binary data, in
-- which 5 bytes of binary data are mapped onto 8 characters from the set
-- {a, ..., k, m, n, p, ..., z, 2, ..., 9} (i.e., all lower-case letters
-- and digits except for l, o, 0, and 9).
--
-- The armor32 function encodes binary using this base-32
-- encoding, while dearmor32 reverses the encoding.
--
-- Binary data is assumed to come from the Data.ByteString.Lazy
-- type.
module LIO.Armor
armor32 :: ByteString -> String
dearmor32 :: String -> ByteString
a2b :: UArray Word8 Char
b2a :: UArray Char Word8
-- | Return True iff the caracter could have been in the output of
-- armor32.
a32Valid :: Char -> Bool
-- | This module creates new files and directories with unique names. Its
-- functionality is similary to C's mkstemp() and mkdtemp() functions.
module LIO.TmpFile
-- | Creates a new file with a unique name in a particular directory
mkTmpFile :: IOMode -> FilePath -> String -> IO (Handle, FilePath)
-- | Creates a new subdirectory with uniqe file name. Returns the pathname
-- of the new directory as the second element of a pair, just for
-- consistency with the interface to mkTmpFile. See
-- mkTmpDir' if you don't want this behavior.
mkTmpDir :: FilePath -> String -> IO ((), FilePath)
-- | Like mkTmpDir, but just returns the pathname of the new
-- directory.
mkTmpDir' :: FilePath -> String -> IO FilePath
-- | Executes a function on temporary file names until the function does
-- not throw AlreadyExistsError. For example, mkTmpFile is defined
-- as:
--
--
-- mkTmpFile m d s = mkTmp (openFileExclusive m) d s
--
mkTmp :: (FilePath -> IO a) -> FilePath -> String -> IO (a, FilePath)
-- | Opens a file in exclusive mode, throwing AlreadyExistsError if the
-- file name is already in use.
openFileExclusive :: IOMode -> FilePath -> IO Handle
-- | Return a temorary file name, based on the value of the current time of
-- day clock.
tmpName :: IO String
-- | When the file name returned by tmpName already exists,
-- nextTmpName modifies the file name to generate a new one.
nextTmpName :: String -> String
-- | Serialize an Integer into an array of bytes, in little-endian order.
serializele :: Int -> Integer -> [Word8]
-- | Take an array of bytes containing an Integer serialized in
-- little-endian order, and return the Integer.
unserializele :: [Word8] -> Integer
-- | Flushes a Handle to disk with fsync()
hSync :: Handle -> IO ()
-- | This module manages a file store in which a label is associated with
-- every file and directory. The file store is grouped into directories
-- by label. Files are stored under names like:
--
--
-- LabelHash/OpaqueName
--
--
-- where LabelHash is a SHA-224 hash of the label, and OpaqueName is
-- either a regular file (containing contents) or a directory populated
-- exclusively by symbolic links pointing back into LabelHash
-- directories. Each LabelHash directory also has a file called
--
--
-- LabelHash/LABEL
--
--
-- which actually contains the label of all the files in that directory.
--
-- There is also a symbolic link root, pointing to the root
-- directory. For efficiency, LabelHash actually consists of
-- multiple directories.
--
-- There are two externally-visible abstractions. The first is
-- Name, which refers to a file name in a user directory, of the
-- form:
--
--
-- LabelHash/OpaqueName/UserName
--
--
-- There is also a special Name, rootDir, which refers to
-- the root directory. Untrusted user code has access to the
-- rootDir Name, and can walk the tree from there using the
-- lookupName function. The LIO.Handle module contains
-- functions mkDir and mkLHandle which permit untrusted
-- code to make new Names as well as to do handle-based IO on
-- protected files.
--
-- The second is Node, which refers to one of the
-- OpaqueNames that Names point to. Currently, any
-- functions that operate on Nodes are in the IO Monad so as not
-- to be executable by untrusted code. This is important because in order
-- to use a file, someone must have the right to know know that the file
-- exists, and this requires read permission on the file's Name.
-- It would be insecure if untrusted code could execute openNode in the
-- LIO Monad.
--
-- Note that if a machine crashes, the code in this module could leave
-- the filesystem in an inconsistent state. However, the code tries to
-- maitain the invariant that any inconsistencies will either be:
--
--
-- - temporary files or directories whose names end with the
-- "~" character, or
-- - dangling symbolic links.
--
--
-- Both of these inconsistencies can be checked and cleaned up locally
-- without examining the whole file system. The code tries to fix up
-- these inconsistencies on-the-fly as it encounters them. However, it
-- could possibly lieave some stranded temporary LABEL...~
-- files. You could also end up with some weirdness like a file that
-- shows up in getDirectoryContents, but that you can't open for reading.
--
-- To keep from having to examine the whole file system to fix errors,
-- the code tries to maintain the invariant that if a 'Node'\'s file name
-- doesn't end with ~, then there must be a link pointing to it
-- somewhere. This is why the code uses a separate NewNode type to
-- represent a Node whose name ends ~. The function
-- linkNode renames the NewNode to a name without a
-- trailing ~ only after creating a Name that points to
-- the permenent Node path.
--
-- Assuming a file system that preserves the order of metadata
-- operations, the code should mostly be okay to recover from any
-- crashes. If using soft updates, which can re-order metadata
-- operations, you could end up with symbolic links that point nowhere.
--
-- In the worst case scenario if inconsistencies develop, you can
-- manually fix up the file system by deleting all danglinng symbolic
-- links and all files and directories ending ~. Make sure no
-- application is concurrently accessing the file system, however.
module LIO.FS
-- | The Name type represents user-chosen (non-opaque) filenames
-- of symbolic links, either "root" or pathnames of the form
-- LabelHash/OpaqueName/filename. Intermediary components of the
-- file name must not be symbolic links.
data Name l
-- | Return the root directory for the default root label. (There is a root
-- directory for each label, but only one label is the default.)
rootDir :: Label l => LIO l s (Name l)
-- | Get the root directory for a particular label.
getRootDir :: Label l => l -> Name l
-- | Creates a root directory for a particular label.
mkRootDir :: Priv l p => p -> l -> LIO l s (Name l)
-- | Looks up a FilePath, turning it into a Name, and raising to
-- current label to reflect all directories traversed. Note that this
-- only looks up a Name; it does not ensure the Name
-- actually exists. The intent is that you call lookupName
-- before creating or opening files.
--
-- Note that this function will touch bad parts of the file system if it
-- is supplied with a malicous Name. Thus, it is important to keep
-- the constructor of Name private, so that the only way for user
-- code to generate names is to start with rootDir and call
-- lookupName.
lookupName :: Priv l p => p -> Name l -> FilePath -> LIO l s (Name l)
-- | Creates a temporary directory in an existing directory (or
-- label-specific root directory, if the Name argument comes from
-- getRootDir).
mkTmpDirL :: Priv l p => p -> l -> Name l -> String -> LIO l s (FilePath, Name l)
initFS :: Label l => l -> IO ()
-- | The Node type represents filenames of the form
-- LabelHash/OpaqueName. These names must always point to
-- regular files or directories (not symbolic links). There must always
-- exist a file LabalHash/LABEL specifying the label of a
-- Node.
data Node
-- | Label protecting the name of a file. Note that this is the label of
-- the directory containing the file name, not the label of the Node that
-- the file name designates.
labelOfName :: Label l => Name l -> IO l
-- | Label protecting the contents of a node.
labelOfNode :: Label l => Node -> IO l
-- | Node that a Name is pointing to.
nodeOfName :: Label l => Name l -> IO Node
-- | Create new Node in the appropriate directory for a given label. The
-- node gets created with an extra ~ appended, and wrapped in the type
-- NewNode to reflect this fact.
mkNode :: Label l => l -> (FilePath -> String -> IO (a, FilePath)) -> IO (a, NewNode)
-- | Wrapper around mkNode to create a directory.
mkNodeDir :: Label l => l -> IO NewNode
-- | Wrapper around mkNode to create a regular file.
mkNodeReg :: Label l => IOMode -> l -> IO (Handle, NewNode)
-- | Assign a Name to a NewNode, turning it into a
-- Node. Note that unlike the Unix file system, only a single link
-- may be created to each node.
linkNode :: Label l => NewNode -> Name l -> IO Node
lookupNode :: Priv l p => p -> Name l -> FilePath -> Bool -> LIO l s Node
-- | Thie function just calls openFile on the filename in a
-- Node. However, on the off chance that the file system is in an
-- inconsistent state (e.g., because of a crash during a call to
-- linkNode), it tries to finish creating a partially created
-- Node.
openNode :: Node -> IOMode -> IO Handle
-- | Thie function is a wrapper around getDirectoryContents that
-- tries to fixup errors analogously to openNode.
getDirectoryContentsNode :: Node -> IO [FilePath]
tryPred :: Exception e => (e -> Bool) -> IO a -> IO (Either e a)
instance Typeable FSErr
instance Show FSErr
instance Show LDir
instance Show Node
instance Show NewNode
instance Show l => Show (Name l)
instance Exception FSErr
-- | This module abstracts the basic FileHandle methods provided
-- by the system library, and provides an LHandle (Labeled Handle)
-- type that can be manipulated from within the LIO Monad. Two
-- lower level functions, mkDir and mkLHandle may be useful
-- for functions that wish to open file names that are not relative to
-- rootDir. (There is no notion of changeable current working
-- directory in the LIO Monad.)
--
-- The actual storage of labeled files is handled by the LIO.FS
-- module.
module LIO.Handle
class Monad m => DirectoryOps h m | m -> h
getDirectoryContents :: DirectoryOps h m => FilePath -> m [FilePath]
createDirectory :: DirectoryOps h m => FilePath -> m ()
openFile :: DirectoryOps h m => FilePath -> IOMode -> m h
class Monad m => CloseOps h m
hClose :: CloseOps h m => h -> m ()
hFlush :: CloseOps h m => h -> m ()
class CloseOps h m => HandleOps h b m
hGet :: HandleOps h b m => h -> Int -> m b
hGetNonBlocking :: HandleOps h b m => h -> Int -> m b
hGetContents :: HandleOps h b m => h -> m b
hPut :: HandleOps h b m => h -> b -> m ()
hPutStrLn :: HandleOps h b m => h -> b -> m ()
data LHandle l h
hlabelOf :: Label l => LHandle l h -> l
mkDir :: Priv l p => p -> l -> Name l -> FilePath -> LIO l s ()
mkLHandle :: Priv l p => p -> l -> Name l -> FilePath -> IOMode -> LIO l s (LHandle l Handle)
readFile :: (DirectoryOps h m, HandleOps h b m) => FilePath -> m b
writeFile :: (DirectoryOps h m, HandleOps h b m, OnExceptionTCB m) => FilePath -> b -> m ()
createDirectoryPR :: Priv l p => p -> Name l -> FilePath -> LIO l s ()
openFilePR :: Priv l p => p -> Name l -> FilePath -> IOMode -> LIO l s (LHandle l Handle)
writeFilePR :: (Priv l p, HandleOps Handle b IO) => p -> Name l -> FilePath -> b -> LIO l s ()
createDirectoryP :: Priv l p => p -> FilePath -> LIO l s ()
openFileP :: Priv l p => p -> FilePath -> IOMode -> LIO l s (LHandle l Handle)
writeFileP :: (Priv l p, HandleOps Handle b IO) => p -> FilePath -> b -> LIO l s ()
-- | See System.IO.openFile
data IOMode :: *
ReadMode :: IOMode
WriteMode :: IOMode
AppendMode :: IOMode
ReadWriteMode :: IOMode
instance (Label l, CloseOps (LHandle l h) (LIO l s), HandleOps h b IO) => HandleOps (LHandle l h) b (LIO l s)
instance Label l => CloseOps (LHandle l Handle) (LIO l s)
instance Label l => DirectoryOps (LHandle l Handle) (LIO l s)
instance Label l => MintTCB (LHandle l Handle) (Handle, l)
instance HandleOps Handle ByteString IO
instance CloseOps Handle IO
instance DirectoryOps Handle IO
-- | This is the main module to be included by code using the Labeled IO
-- (LIO) library. The core of the library is documented in the
-- LIO.TCB module. Note, however, that unprivileged code must not
-- be allowed to import LIO.TCB--instead, a module LIO.Base
-- exports just the safe symbols from LIO.TCB. This module,
-- LIO.LIO, re-exports LIO.Base as well as a few other
-- handy modules. For many modules it should be the only import
-- necessary.
--
-- Certain symbols in the LIO library supersede variants in the standard
-- Haskell libraries. Thus, depending on the modules imported and
-- functions used, you may wish to import LIO with commands like these:
--
--
-- import Prelude hiding (readFile, writeFile, catch)
-- import Control.Exception hiding (throwIO, catch, handle, onException
-- , bracket, block, unblock)
-- import LIO.LIO
--
--
-- The LIO variants of the system functions hidden in the above import
-- commands are designed to work in both the IO and LIO monads, making it
-- easier to have both types of code in the same module.
--
-- Warning: For security, at a minimum untrusted code must not be allowed
-- to do any of the following:
--
--
-- - Import LIO.TCB,
-- - Use any symbols with names ending ...TCB,
-- - Use the foreign keyword,
-- - Use functions such as unsafePerformIO,
-- unsafeInterleaveIO, inlinePerformIO,
-- - Use language extensions such as Generalized Newtype Deriving and
-- Stand-alone Deriving to extend LIO types (such as by deriving an
-- instance of Show for Lref, or deriving an
-- instance of the MonadTrans class for LIO,
-- which would allow untrusted code to bypass all security with
-- lift),
-- - Manually define typeOf methods (as this would cause the
-- supposedly safe cast method to make usafe casts);
-- automatically deriving Typeable should be safe.
-- - Define new Ix instances (which could produce out of
-- bounds array references).
--
--
-- In general, pragmas and imports should be highly scrutinized. For
-- example, most of the Foreign class of modules are probably
-- dangerous. With GHC 7.2, we use the SafeHaskell extension to enforce
-- these.
module LIO.LIO