{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Unsafe #-}

-- | Provide security for computations involving side-effects.
module SecLib.TCB.SecIO where

import Control.Applicative

import SecLib.Lattice
import SecLib.TCB.Sec

--
-- The SecIO Monad
--

{-| This monad represents side-effectful computations with observable effects, and return
    values, at security level, at least, @l@.
-}
newtype SecIO l a = MkSecIO (IO (Sec l a))

instance Monad (SecIO l) where
  return a =
    MkSecIO (return (return a))

  MkSecIO m >>= k =
    MkSecIO (do sec_a <- m
                let MkSecIO m' = k (unsec sec_a)
                m')

{- |
   'SecIO' cannot be a functor for security reasons. The member `fmap` is
declared as @undefined@ due to the Applicative-Monad Haskell 2014 proposal.
-}
instance Functor (SecIO l) where
    fmap = undefined

{- |
   For the same reason as above, '(<*>)' is undefined.
-}
instance Applicative (SecIO l) where
    pure  = return
    (<*>) = undefined

--
-- Lifting secure values
--

-- | Lift pure sensitive values into secure side-effectful computations.
toSecIO :: Sec l a -> SecIO l a
toSecIO sa = MkSecIO (return sa)

--
-- Running computations
--


{- | Execute secure computations.

This function can be safely given to untrusted code. However, trusted code
should not run an 'IO' computation returned by untrusted code. After all, its
origin cannot be determined, i.e., it could come from 'run' or any other IO
operation which could compromise confidentiality or integrity of data.

-}
run :: SecIO l a -> IO (Sec l a)
run (MkSecIO m) = m

--
-- Secure composition
--

{- |
   Secure coupling of side-effectul computations.
-}
plug :: forall l l' a . Less l l' => SecIO l' a -> SecIO l (Sec l' a)
plug (MkSecIO m) = MkSecIO (do sh_a <- m
                               return (return sh_a))  :: SecIO l (Sec l' a)

ioTCB :: IO a -> SecIO l a
ioTCB io = MkSecIO $ io >>= return . return