MonadicFlow.hs

{-# LANGUAGE DataKinds, 
             TypeFamilies, 
             PolyKinds, 
             GADTs, 
             ConstraintKinds #-}

module MonadicFlow (
    Sec,
    Less,
    open,
    up,
    TwoLevels (..),
    proofLow,
    declassifyWith,
   ) where

import GHC.Exts (Constraint)
import Control.Monad.Identity
import Control.Applicative

-- | Implementation based on Russo et al., 2008


-- | Sec: the Identity monad tagged with a proposition allowing to access its value.
data Sec s a = MkSec { runSec :: a } | Denied

instance Functor (Sec s) where
    fmap f (MkSec x) = MkSec $ f x
    fmap _ Denied = Denied

instance Applicative (Sec s) where
    pure x = MkSec x
    (MkSec f) <*> (MkSec x) = MkSec $ f x
    _ <*> _ = Denied

instance Monad (Sec s) where
    return x = MkSec x
    (MkSec a) >>= f = f a
    Denied >>= _ = Denied
    fail _ = Denied


-- | API for handling Sec values. Raising the security level of a value with @up@ 
-- is possible for everybody. A Sec value can be unwrapped given a proof that 
-- accessing the security level of it was allowed.

-- | A predicate on types, to be implemented by the provider of a security level type.
-- Actually, means ""less or equal"".
type family Less x y :: Constraint

-- | Proxy/proof, that one actually owns a value of type s.
data Ticket s = Ticket

-- | Needs to be strict in `s` to disallow passing @undefined@ as proof for @s@.
open :: Ticket s -> Sec s a -> Maybe a
open Ticket (MkSec a) = Just a
open Ticket Denied = Nothing

up :: Less s s' => Sec s a -> Sec s' a
up (MkSec a) = MkSec a
up Denied = Denied


-- only for trusted code !
reveal :: Sec s a -> a
reveal (MkSec a) = a

unsafeCoerceLevels :: Sec s a -> Sec s' a
unsafeCoerceLevels (MkSec x) = MkSec x
unsafeCoerceLevels Denied = Denied



-- | Declassification
declassifyWith :: (Less s k, Less s' s) => Sec k (a -> Maybe b) -> Sec s a -> Sec s' b
declassifyWith (MkSec f) s = unsafeCoerceLevels $ do
    x <- s
    case f x of
        Just x' -> return x'
        Nothing -> fail """"
declassifyWith Denied _ = Denied




-- | These types and instances are exported for testing.

data TwoLevels = H | L

type instance (Less L H) = ()
type instance (Less l1 l2) = l1 ~ l2

proofLow :: Ticket L
proofLow = Ticket

proofHigh :: Ticket H
proofHigh = Ticket