{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module DCLabel.Core ( -- * Constructors
                      Disj(..), Conj(..), Label(..)
                      -- * DC Labels
                    , Lattice(..), DCLabel(..)
                    , emptyLabel, allLabel
                      -- * Principals
                    , Principal(..), principal
                      -- * Priviliges
                    , TCBPriv(..), Priv
                    , RelaxedLattice(..)
                    , noPriv, rootPrivTCB
                    , delegatePriv, createPrivTCB
                    , CanActFor(..)
                      -- * Label/internal operations
                    , and_label, or_label, ToLNF(..), cleanLabel, implies
                    ) where


import Data.List (nub, sort, (\\))
import Data.Maybe (fromJust)

--
-- Categories
--

-- | A disjunction of ordered elements.
-- The empty list '[]' corresponds to the disjunction of all principals.
-- In other words, conceptually, @[] =  [P_1 \/ P_2 \/ ...]@
newtype Disj = MkDisj { disj :: [Principal] }
        deriving (Eq, Ord, Show, Read)


-- | A conjunction of ordered elements.
-- The empty list '[]' corresponds to the single disjunction of all principals.
-- In other words, conceptually, @[] =  {[P_1 \/ P_2 \/ ...]}@
newtype Conj = MkConj { conj :: [Disj] }
        deriving (Eq, Ord, Show, Read)

--
-- Labels
--

-- | (Bounded) Lattice definition 
class Eq a => Lattice a where
  bottom    :: a  -- ^ Bottom of lattice
  top       :: a  -- ^ Top of lattice
  join      :: a -> a -> a  -- ^ Join of two elements
  meet      :: a -> a -> a  -- ^ Meet of two elements
  canflowto :: a -> a -> Bool -- ^ Partial order relation


-- | A label is a conjunction of disjunctions, where @MkLabelAll@ is 
-- the constructor that is associated with the conjunction of all
-- possible disjunctions.
data Label = MkLabelAll
           | MkLabel { label :: Conj }
     deriving (Show, Read)

instance Eq Label where
  (==) MkLabelAll MkLabelAll = True
  (==) MkLabelAll _ = False
  (==) _ MkLabelAll = False
  (==) l1 l2 = (label . toLNF $ l1) == (label . toLNF $ l2)

-- | A label without any disjunctions or conjunctions. This label, conceptually
-- corresponds to the label consisting of a single category containing all
-- principals.
-- In other words, conceptually, @emptyLabel = <{[P_1 \/ P_2 \/ ...]}>@
emptyLabel :: Label
emptyLabel = MkLabel (MkConj [])

-- | The dual of 'emptyLabel', 'allLabel' consists of the conjunction of
-- all possible disjunctions, i.e., it is the label that implies all
-- other labels.
-- In other words, conceptually, @allLabel = <{[P_1] /\ [P_2] /\ ...}>@
allLabel :: Label
allLabel = MkLabelAll

-- | Predicate function that returns @True@ if the label corresponds to
-- the 'emptyLabel'.
isEmptyLabel :: Label -> Bool
isEmptyLabel MkLabelAll = False
isEmptyLabel l = and [ null (disj d) | d <- conj (label l) ]

-- | Predicate function that retuns @True@ if the label corresponds to
-- the 'allLabel'.
isAllLabel :: Label -> Bool
isAllLabel MkLabelAll = True
isAllLabel _ = False


--
-- Helper functions
--


-- | Given two labels, take the union of the disjunctions, i.e., simply 
-- perform an \"and\". Note the new label is not necessarily in LNF.
and_label :: Label -> Label -> Label
and_label l1 l2 | isAllLabel l1 || isAllLabel l2 = allLabel
                | otherwise = MkLabel
                        {label = MkConj $ conj (label l1) ++ conj (label l2)}

-- | Given two labels, perform an \"or\".
-- Note that the new label is not necessarily in LNF.
or_label :: Label -> Label -> Label 
or_label l1 l2 | isEmptyLabel l1 || isEmptyLabel l2 = emptyLabel
               | isAllLabel l2 = l1 
               | isAllLabel l1 = l2 
               | otherwise = MkLabel . MkConj $ [ MkDisj (disj d1 ++ disj d2)
                                                | d1 <- (conj (label l1)) 
                                                , d2 <- (conj (label l2))
                                                , not . null . disj $ d1
                                                , not . null . disj $ d2] 

-- | Determines if a conjunction of disjunctions, i.e., a label, implies
-- (in the logical sense) a disjunction. In other words, it checks if
-- d1 /\ ... /\ dn => d1.
--
-- Properties: 1. forall X, ALL `impliesDisj` X := True
--             2. forall X, X `impliesDisj` []  := True
--             3. forall X/=[],  [] `impliesDisj` X := False              
--
-- Note that the first two guards are only included 
-- for safety; the function is always called with a non-ALL label and 
-- non-null disjunction.
impliesDisj :: Label -> Disj -> Bool 
impliesDisj l d | isAllLabel l = True   -- Asserts 1
                | null (disj d) = True  -- Asserts 2
                | otherwise = or [ and [ e `elem` (disj d) | e <- disj d1 ]
                                 | d1 <- conj (label l)
                                 , not (isEmptyLabel l) ] -- Asserts 3

-- | Determines if a label implies (in the logical sense) another label. 
-- In other words, d1 /\ ... /\ dn => d1' /\ ... /\ dn'.
--
-- Properties: 1. forall X, ALL `implies` X := True
--             2. forall X/=ALL, X `implies` ALL := False
--             3. forall X, X `implies` [] := True
--             4. forall X/=[], [] `implies` X := False
implies :: Label -> Label -> Bool 
implies l1 l2 | isAllLabel l1 = True -- Asserts 1
              | isAllLabel l2 = False -- Asserts 2
              | otherwise = and [ impliesDisj l1 d 
                                | d <- conj . label . toLNF $ l2 ]


-- | Removes any duplicate principals from categories, and any duplicate
-- categories from the label. To return a clean label, it sorts the label
-- and removes empty disjunctions.
cleanLabel :: Label -> Label
cleanLabel MkLabelAll = MkLabelAll 
cleanLabel l = MkLabel . MkConj . sort . nub $
               [ MkDisj ( (sort . nub) (disj d) ) | d <- conj (label l)
                                                , not . null $ disj d ] 
-- | Class used to reduce labels to LNF.
-- It is used to overload the reduce function used by the 'Label', 'SLabel',
-- 'ILabel', and 'DCLabel'.
class ToLNF a where
  toLNF :: a -> a

-- | Reduce a label to LNF.
-- First it applies @cleanLabel@ to remove duplicate principals and categories.
-- Following, it removes extraneous/redundant categories. A category is said to
-- be extraneous if there is another category in the label that implies it.
instance ToLNF Label where
  toLNF MkLabelAll = MkLabelAll 
  toLNF l = MkLabel . MkConj $ l' \\ extraneous 
    where l' = conj . label $ cleanLabel l
          extraneous = [ d2 | d1 <- l', d2 <- l', d1 /= d2
                            , impliesDisj ((MkLabel . MkConj) [d1]) d2 ]

--
-- DC Labels
--


--
-- DC Labels : (Secrecy, Integrity)
--

-- | A DC label for secrecy and integrity.
data DCLabel = MkDCLabel { secrecy :: Label
                         , integrity :: Label } 
  deriving (Eq, Show, Read)

instance ToLNF DCLabel where
  toLNF l = MkDCLabel { secrecy = toLNF (secrecy l)
                      , integrity = toLNF (integrity l)}

instance Lattice DCLabel where
  bottom = MkDCLabel { secrecy = MkLabel $ MkConj []
                     , integrity = MkLabelAll }
  top = MkDCLabel { secrecy = MkLabelAll
                  , integrity = MkLabel $ MkConj [] }
  join l1 l2 = let s3 = (secrecy l1) `and_label` (secrecy l2)
                   i3 = (integrity l1) `or_label` (integrity l2)
               in toLNF $ MkDCLabel { secrecy = s3
                                    , integrity = i3 }
  meet l1 l2 = let s3 = (secrecy l1) `or_label` (secrecy l2)
                   i3 = (integrity l1) `and_label` (integrity l2)
               in toLNF $ MkDCLabel { secrecy = s3
                                    , integrity = i3 }
  canflowto l1 l2 = let l1' = toLNF l1
                        l2' = toLNF l2
                    in ((secrecy l2') `implies` (secrecy l1')) &&
                       ((integrity l1') `implies` (integrity l2'))


--
-- Principals
-- 

-- | Principal is a simple string.
newtype Principal = MkPrincipal { name :: String }
                  deriving (Eq, Ord, Show, Read)

-- | Generates a principal from an string. 
principal :: String -> Principal 
principal = MkPrincipal


--
-- Priviliges
-- 

-- | Privilege object is just a conjunction of disjunctions, i.e., a 'Label'.
-- A trusted privileged object must be introduced by trusted code, after which
-- trusted privileged objects can be created by delegation.
data TCBPriv = MkTCBPriv { priv :: Label } 
     deriving (Eq, Show)

-- | Untrusted privileged object, which can be converted to a 'TCBPriv' with
-- 'delegatePriv'.
type Priv = Label

-- | Class extending 'Lattice', by allowing for the more relaxed label
-- comparison  @canflowto_p@.
class (Lattice a) => RelaxedLattice a where
        -- ^ Relaxed partial-order relation
        canflowto_p :: TCBPriv -> a -> a -> Bool


instance RelaxedLattice DCLabel where
  canflowto_p p l1 l2 =
    let l1' =  MkDCLabel { secrecy = (secrecy l2)
                         , integrity = (and_label (priv p) (integrity l2)) }
        l2' =  MkDCLabel { secrecy = (and_label (priv p) (secrecy l2))
                         , integrity = (integrity l2) }
    in canflowto l1' l2' 


-- | Given trusted privilige and a \"desired\" untrusted privilege,
-- return a trusted version of the untrusted privilige, if the
-- provided (trusted) privilige implies it.
delegatePriv :: TCBPriv -> Priv -> Maybe TCBPriv
delegatePriv tPriv rPriv = let rPriv' = toLNF rPriv
                           in case (priv tPriv) `implies` rPriv' of
                                True -> Just (MkTCBPriv rPriv')
                                False -> Nothing

-- | Privilege object corresponding to no privileges.
noPriv :: TCBPriv
noPriv = MkTCBPriv { priv = emptyLabel }

-- | Privilege object corresponding to the \"root\", or all privileges.
-- Any other privilige may be delegated using this privilege object and it must
-- therefore not be exported to untrusted code. 
rootPrivTCB :: TCBPriv
rootPrivTCB = MkTCBPriv { priv = allLabel }

-- | This function creates any privilege object given an untrusted 
-- privilege 'Priv'. Note that this function should not be exported
-- to untrusted code.
createPrivTCB :: Priv -> TCBPriv
createPrivTCB = fromJust . (delegatePriv rootPrivTCB)
  		
-- | Class used for checking if a computation can use a privilege in place of
-- the other. This notion corresponds to the DLM \"can-act-for\".
class CanActFor a b where
        -- ^ Can use first privilige in place of second.
        canActFor :: a -> b -> Bool

instance CanActFor Priv Priv where
  canActFor p1 p2 = p1 `implies` p2

instance CanActFor Priv TCBPriv where
  canActFor p1 p2 = p1 `implies` (priv p2)

instance CanActFor TCBPriv Priv where
  canActFor p1 p2 = (priv p1) `implies` p2

instance CanActFor TCBPriv TCBPriv where
  canActFor p1 p2 = (priv p1) `implies` (priv p2)