{-# 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)