lio-0.10.0.0: LIO/TCB.hs

{-# LANGUAGE Unsafe #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}

{- | 

This module exports 

* The definition of the 'LIO' monad and relevant trusted state
  access/modifying functions.

* Various other types whose constructors are privileged and must be
  hidden from untrusted code.

* Uncatchable exceptions used to pop threads out of the 'LIO' monad
  unconditionally.

* Combinators for executing 'IO' actions within the 'LIO' monad.

The documentation and external, safe 'LIO' interface is provided in
"LIO.Core".

-}

module LIO.TCB (
  -- * LIO monad
    LIOState(..), LIO(..)
  -- ** Accessing internal state
  , getLIOStateTCB, putLIOStateTCB, modifyLIOStateTCB, updateLIOStateTCB 
  -- * Executing IO actions
  , ioTCB
  -- * Privileged constructors
  , Priv(..), Labeled(..)
  -- * Uncatchable exception type
  , UncatchableTCB(..), makeCatchable
  -- * Trusted 'Show' and 'Read'
  , ShowTCB(..), ReadTCB(..)
  ) where

import Control.Applicative
import Control.Exception (Exception(..), SomeException(..))
import Control.Monad
import Data.Monoid
import Data.IORef
import Data.Typeable
import Text.Read (minPrec)

import LIO.Label

--
-- LIO Monad
--

-- | Internal state of an 'LIO' computation.
data LIOState l = LIOState { lioLabel     :: !l -- ^ Current label.
                           , lioClearance :: !l -- ^ Current clearance.
                           } deriving (Eq, Show, Read)

-- | The @LIO@ monad is a state monad, with 'IO' as the underlying monad,
-- that carries along a /current label/ ('lioLabel') and /current clearance/
-- ('lioClearance'). The current label imposes restrictions on
-- what the current computation may read and write (e.g., no writes to
-- public channels after reading sensitive data).  Since the current
-- label can be raised to be permissive in what a computation observes,
-- we need a way to prevent certain computations from reading overly
-- sensitive data. This is the role of the current clearance: it imposes
-- an upper bound on the current label.
newtype LIO l a = LIOTCB {
    unLIOTCB :: IORef (LIOState l) -> IO a
  } deriving (Typeable)

instance Monad (LIO l) where
  {-# INLINE return #-}
  return = LIOTCB . const . return
  {-# INLINE (>>=) #-}
  m >>= k = LIOTCB $ \s -> do
    a <- unLIOTCB m s
    unLIOTCB (k a) s
  fail = LIOTCB . const . fail

instance Functor (LIO l) where
  {-# INLINE fmap #-}
  fmap f ma = LIOTCB $ \s -> unLIOTCB ma s >>= return . f

instance Applicative (LIO l) where
  {-# INLINE pure #-}
  pure = return
  {-# INLINE (<*>) #-}
  (<*>) = ap

--
-- Internal state
--

-- | Get internal state. This function is not actually unsafe, but
-- to avoid future security bugs we leave all direct access to the
-- internal state to trusted code.
getLIOStateTCB :: LIO l (LIOState l)
{-# INLINE getLIOStateTCB #-}
getLIOStateTCB = LIOTCB readIORef

-- | Set internal state.
putLIOStateTCB :: LIOState l -> LIO l ()
{-# INLINE putLIOStateTCB #-}
putLIOStateTCB s = LIOTCB $ \sp -> writeIORef sp $! s

-- | Update the internal state given some function.
modifyLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()
{-# INLINE modifyLIOStateTCB #-}
modifyLIOStateTCB f = do
  s <- getLIOStateTCB
  putLIOStateTCB (f s)

{-# DEPRECATED updateLIOStateTCB "Use modifyLIOStateTCB instead" #-}
updateLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()
updateLIOStateTCB = modifyLIOStateTCB

--
-- Executing IO actions
--

-- | 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, you will generally want to
-- use 'rethrowIoTCB'.
ioTCB :: IO a -> LIO l a
{-# INLINE ioTCB #-}
ioTCB = LIOTCB . const

--
-- Exception handling
--

-- | An uncatchable exception hierarchy use to terminate an untrusted
-- thread.  Wrap the uncatchable exception in 'UncatchableTCB' before
-- throwing it to the thread.  'runLIO' will subsequently unwrap the
-- 'UncatchableTCB' constructor.
--
-- Note this can be circumvented by 'IO.mapException', which should be
-- made unsafe.
data UncatchableTCB = forall e. (Exception e) =>
                      UncatchableTCB e deriving (Typeable)

instance Show UncatchableTCB where
  showsPrec p (UncatchableTCB e) = showsPrec p e

instance Exception UncatchableTCB where
  toException = SomeException
  fromException (SomeException e) = cast e

-- | Simple utility function that strips 'UncatchableTCB' from around an
-- exception.
makeCatchable :: SomeException -> SomeException
makeCatchable e@(SomeException einner) =
  case cast einner of Just (UncatchableTCB enew) -> SomeException enew
                      Nothing                    -> e

--
-- Privileges
--

-- | A newtype wrapper that can be used by trusted code to bless
-- privileges.  Privilege-related functions are defined in
-- "LIO.Privs", but the constructor, 'PrivTCB', allows one to mint
-- arbitrary privileges and hence must be located in this file.
newtype Priv a = PrivTCB a deriving (Show, Eq, Typeable)

instance Monoid p => Monoid (Priv p) where
  mempty = PrivTCB mempty
  {-# INLINE mappend #-}
  mappend (PrivTCB m1) (PrivTCB m2) = PrivTCB $ m1 `mappend` m2
  {-# INLINE mconcat #-}
  mconcat ps = PrivTCB $ mconcat $ map (\(PrivTCB p) -> p) ps

--
-- Pure labeled values
--

-- | @Labeled l a@ is a value that associates a label of type @l@ with
-- a value of type @a@. Labeled values allow users to label data with
-- a label other than the current label. In an embedded setting this
-- is akin to having first class labeled values. Note that 'Labeled'
-- is an instance of 'LabelOf', which effectively means that the label
-- of a 'Labeled' value is usually just protected by the current
-- label. (Of course if you have a nested labeled value then the label
-- on the inner labeled value's label is the outer label.)
data Labeled l t = LabeledTCB !l t deriving Typeable
-- Note: t cannot be strict if we want things like lFmap.

instance LabelOf Labeled where
  labelOf (LabeledTCB l _) = l

-- | Trusted 'Show' instance.
instance (Label l, Show a) => ShowTCB (Labeled l a) where
    showTCB (LabeledTCB l t) = show t ++ " {" ++ show l ++ "}"

-- | Trusted 'Read' instance.
instance (Label l, Read l, Read a) => ReadTCB (Labeled l a) where
  readsPrecTCB _ str = do (val, str1) <- reads str
                          ("{", str2) <- lex str1
                          (lab, str3) <- reads str2
                          ("}", rest) <- lex str3
                          return (LabeledTCB lab val, rest)

--
-- Trusted 'Show' and 'Read'
--

-- | 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 when debugging.  The 'showTCB' method can be used
-- to examine such objects.
class ShowTCB a where
    showTCB :: a -> String

-- | It is useful to have the dual of 'ShowTCB', @ReadTCB@, that allows
-- for the reading of strings that were created using 'showTCB'. Only
-- @readTCB@ (corresponding to 'read') and @readsPrecTCB@ (corresponding
-- to 'readsPrec') are implemented.
class ReadTCB a where
  -- | Trusted 'readsPrec'
  readsPrecTCB :: Int -> ReadS a
  -- | Trusted 'read'
  readTCB :: String -> a
  readTCB str = check $ readsPrecTCB minPrec str
    where check []                          = error "readTCB: no parse"
          check [(x,rst)] | all (==' ') rst = x
                         | otherwise        = error "readTCB: no parse"
          check _                           = error "readTCB: ambiguous parse"