module LMonad.Label.DisjunctionCategory where
import Data.Set (Set)
import qualified Data.Set as Set
import Prelude
import LMonad
type Disjunction p = Set p
type Conjunction p = Set (Disjunction p)
data Ord p => DCLabel p = DCLabel {
dcConfidentiality :: Conjunction p
, dcIntegrity :: Conjunction p
}
deriving (Eq, Show)
dcSingleton :: Ord p => p -> DCLabel p
dcSingleton p =
let conj = Set.singleton (Set.singleton p) in
DCLabel conj conj
dcConfidentialitySingleton :: Ord p => p -> DCLabel p
dcConfidentialitySingleton p = DCLabel (Set.singleton (Set.singleton p)) $ Set.singleton Set.empty
dcIntegritySingleton :: Ord p => p -> DCLabel p
dcIntegritySingleton p = DCLabel Set.empty (Set.singleton (Set.singleton p))
forall :: (a -> Bool) -> Set a -> Bool
forall pred = Set.foldl' (\acc el -> acc && (pred el)) True
exists :: (a -> Bool) -> Set a -> Bool
exists pred = Set.foldl' (\acc el -> acc || (pred el)) False
subset :: Ord p => Disjunction p -> Disjunction p -> Bool
subset = Set.isSubsetOf
implies :: Ord p => Conjunction p -> Conjunction p -> Bool
implies a b =
forall (\elB -> exists (\elA -> subset elA elB) a) b
conjunctionInsertDisjunction :: Ord p => Conjunction p -> Disjunction p -> Conjunction p
conjunctionInsertDisjunction conj disj =
if exists (`subset` disj) conj then
conj
else
Set.insert disj $ Set.filter (\el -> not (disj `subset` el)) conj
conjunctionAnd :: Ord p => Conjunction p -> Conjunction p -> Conjunction p
conjunctionAnd = Set.foldl' conjunctionInsertDisjunction
conjunctionOr :: Ord p => Conjunction p -> Conjunction p -> Conjunction p
conjunctionOr conj1 = Set.foldl' (\acc disj2 -> Set.foldl' (\acc disj1 ->
conjunctionInsertDisjunction acc (Set.union disj1 disj2)
) acc conj1) Set.empty
instance Ord p => Label (DCLabel p) where
glb (DCLabel c1 i1) (DCLabel c2 i2) =
DCLabel (c1 `conjunctionOr` c2) (i1 `conjunctionAnd` i2)
lub (DCLabel c1 i1) (DCLabel c2 i2) =
DCLabel (c1 `conjunctionAnd` c2) (i1 `conjunctionOr` i2)
canFlowTo (DCLabel c1 i1) (DCLabel c2 i2) =
c2 `implies` c1 && i1 `implies` i2
bottom = DCLabel Set.empty $ Set.singleton Set.empty