LatticeSecurity.hs

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}

module LatticeSecurity where

data H -- High
data L -- Low

class Flow l l'              where
class Flow l l' => Less l l' where

instance Flow L L where
instance Flow L H where
instance Flow H H where

instance Less L L where
instance Less L H where
instance Less H H where

-- | This monad labels the results of the computation (of type @a@) with label @l@.
newtype MAC l a = MkMAC (IO a)

-- | Labeling expressions of type @a@ with label @l@.
newtype Res l a = MkRes {unRes :: a}

-- | Label of resources
labelOf :: Res l a -> l
labelOf _res = undefined

instance Functor (MAC l) where
    fmap f (MkMAC io) = MkMAC (fmap f io)

instance Applicative (MAC l) where
    pure = MkMAC . return
    (<*>) (MkMAC f) (MkMAC a) = MkMAC (f <*> a)

instance Monad (MAC l) where
   return = pure
   MkMAC m >>= k = unsafeLift (m >>= runMAC . k)

-- | Should not be exported!
unsafeLift :: IO a -> MAC l a
unsafeLift = MkMAC

-- | Execute secure computations.
runMAC :: MAC l a -> IO a
runMAC (MkMAC m) = m

-- | Lifts action in @IO@ to action in @MAC@
create :: Less l l' => IO (d a) -> MAC l (Res l' (d a))
create io = unsafeLift io >>= return . MkRes

-- | Lifts function in @IO@ to function in @MAC@
writeup :: Less l l' => (d a -> IO ()) -> Res l' (d a) -> MAC l ()
writeup io (MkRes a) = unsafeLift $ io a

-- | Lifts @IO@ action that reads from resource to function in @MAC@ that reads from labeled resource.
readdown :: Less l' l => (d a -> IO a) -> Res l' (d a) -> MAC l a
readdown io (MkRes da) = unsafeLift $ io da

-- | Type denoting values of type @a@
newtype Id a = MkId { unId :: a }

-- | Labeled expressions
type Labeled l a = Res l (Id a)

-- | Creation of labeled expressions
label :: Less l l' => a -> MAC l (Labeled l' a)
label = create . return . MkId

-- | Observing labeled expressions
unlabel :: Less l' l => Labeled l' a -> MAC l a
unlabel = readdown (return . unId)