{-# LANGUAGE Safe #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE MultiParamTypeClasses #-} {-| This module implements Disjunction Category Labels (DCLabels). DCLabels is a label format for information flow control (IFC) systems. This library exports relevant data types and operations that may be used by dynamic IFC systems such as the "LIO" library. A 'DCLabel' is a pair of /secrecy/ and /integrity/ 'Component's (sometimes called category sets). Each 'Component' (or formula) is a conjunction (implemented in terms of 'Set's) of 'Clause's (or category) in propositional logic (without negation) specifying a restriction on the flow of information labeled as such. Alternatively, a 'Component' can take on the value 'DCFalse' corresponding to falsehood. Each 'Clause', in turn, is a disjunction of 'Principal's, , where a 'Principal' is a source of authority of type 'ByteString', whose meaning is application-specific (e.g., a 'Principal' can be a user name, a URL, etc.). A clause imposes an information flow restriction. In the case of secrecy, a clause restricts who can read, receive, or propagate the information, while in the case of integrity it restricts who can modify a piece of data. The principals composing a clause are said to /own/ the clause or category. For information to flow from a source labeled @L_1@ to a sink @L_2@, the restrictions imposed by the clauses of @L_2@ must at least as restrictive as all the restrictions imposed by the clauses of @L_1@ (hence the conjunction) in the case of secrecy, and at least as permissive in the case of integrity. More specifically, for information to flow from @L_1@ to @L_2@, the labels must satisfy the \"can-flow-to\" relation: @L_1 ⊑ L_2@. The ⊑ label check is implemented by the 'canFlowTo' function. For labels @L_1=\<S_1, I_1\>@, @L_2=\<S_2, I_2\>@ the can-flow-to relation is satisfied if the secrecy component @S_2@ /implies/ @S_1@ and @I_1@ /implies/ @I_2@ (recall that a category set is a conjunction of disjunctions of principals). For example, @\<P_1 ⋁ P_2, True\> ⊑ \<P_1, True\>@ because data that can be read by @P_1@ is more restricting than that readable by @P_1@ or @P_2@. Conversely, @\<True,P_1\> ⊑ \<True,P_1 ⋁ P_2\>@ because data vouched for by @P_1@ or @P_2@ is more permissive than just @P_1@ (note the same principle holds when writing to sinks with such labeling). -} module LIO.DCLabel.Core ( -- * Principals Principal(..), principal -- * Clauses , Clause(..), clause -- * Components -- $component , Component(..) , dcTrue, dcFalse, dcFormula , isTrue, isFalse -- * Labels , DCLabel(..), dcLabel, dcLabelNoReduce , dcPub, dcTop, dcBottom -- * Internal , dcReduce, dcImplies , dcAnd, dcOr ) where import qualified Data.ByteString.Char8 as S8 import Data.List (intercalate) import Data.Monoid import Data.Set (Set) import qualified Data.Set as Set import Data.Typeable import LIO.Label import LIO.Privs -- -- Principals -- -- | A @Principal@ is a simple string representing a source of -- authority. Any piece of code can create principals, regardless of how -- untrusted it is. newtype Principal = Principal { principalName :: S8.ByteString -- ^ Get the principal name. } deriving (Eq, Ord, Typeable) instance Show Principal where showsPrec _ = shows . principalName -- | Generate a principal from a 'String'. (To create one from a -- 'S8.ByteString', just use the 'Principal' constructor directly.) principal :: String -> Principal principal = Principal . S8.pack -- -- Category - disjunction clauses -- -- | A clause or disjunction category is a set of 'Principal's. -- Logically the set corresponds to a disjunction of the principals. newtype Clause = Clause { unClause :: Set Principal -- ^ Get underlying principal-set. } deriving (Eq, Typeable) instance Ord Clause where (Clause c1) <= (Clause c2) = case () of _ | Set.size c1 == Set.size c2 -> c1 <= c2 _ -> Set.size c1 < Set.size c2 instance Show Clause where show c@(Clause uc) | Set.size uc == 1 = show . head . Set.toList $ uc | otherwise = let ps = map show . Set.toList $! unClause c in parens . intercalate " \\/ " $! ps where parens x = "(" ++ x ++ ")" -- | Clause constructor clause :: Set Principal -> Clause clause = Clause -- | A component is a set of clauses, i.e., a formula (conjunction of -- disjunction of 'Principal's). @DCFalse@ corresponds to logical -- @False@, while @DCFormula Set.empty@ corresponds to logical @True@. data Component = DCFalse -- ^ Logical @False@ | DCFormula { unDCFormula :: !(Set Clause) -- ^ Get underlying clause-set. } -- ^ Conjunction of disjunction categories deriving (Eq, Typeable) instance Show Component where show c | isFalse c = show False | isTrue c = show True | otherwise = let cs = map show . Set.toList $! unDCFormula c in intercalate " /\\ " $! cs -- | Privileges can be combined using 'mappend' instance Monoid Component where mempty = dcTrue mappend p1 p2 = dcReduce $! p1 `dcAnd` p2 instance PrivDesc DCLabel Component where canFlowToPrivDesc pd l1 l2 | pd == dcTrue = canFlowTo l1 l2 | otherwise = let i1 = dcReduce $ dcIntegrity l1 `dcAnd` pd s2 = dcReduce $ dcSecrecy l2 `dcAnd` pd in l1 { dcIntegrity = i1 } `canFlowTo` l2 { dcSecrecy = s2 } partDowngradePrivDesc pd la lg | pd == mempty = la `lub` lg | pd == dcFalse = lg | otherwise = let sec_a = dcSecrecy la int_a = dcIntegrity la sec_g = dcSecrecy lg int_g = dcIntegrity lg sec_a' = dcFormula . Set.filter f $ unDCFormula sec_a sec_res = if isFalse sec_a then sec_a else sec_a' `dcAnd` sec_g int_res = (pd `dcAnd` int_a) `dcOr` int_g in dcLabel sec_res int_res where f c = not $ pd `dcImplies` (dcFormula . Set.singleton $ c) -- | Logical @True@. dcTrue :: Component dcTrue = DCFormula Set.empty -- | Logical @False@. dcFalse :: Component dcFalse = DCFalse -- | Arbitrary formula from a clause. dcFormula :: Set Clause -> Component dcFormula = DCFormula -- | Is the component @True@. isTrue :: Component -> Bool isTrue = (== dcTrue) -- | Is the component @False@. isFalse :: Component -> Bool isFalse = (== dcFalse) -- -- Labels -- {- $component A 'Component' is a conjunction of disjunctions of 'Principal's. A 'DCLabel' is simply a pair of such 'Component's. Hence, we define almost all operations in terms of this construct, from which the 'DCLabel' implementation follows almost trivially. -} -- | A @DCLabel@ is a pair of secrecy and integrity 'Component's. data DCLabel = DCLabel { dcSecrecy :: !Component -- ^ Extract secrecy component of a label , dcIntegrity :: !Component -- ^ Extract integrity component of a label } deriving (Eq, Typeable) instance Show DCLabel where showsPrec d l = showParen (d > 5) $ let s = dcSecrecy l i = dcIntegrity l in showsPrec (d + 1) s . showString " %% " . showsPrec (d + 1) i -- | @dcLabel secrecyComponent integrityComponent@ creates a label, -- reducing each component to CNF. dcLabel :: Component -> Component -> DCLabel dcLabel c1 c2 = DCLabel (dcReduce c1) (dcReduce c2) -- | Label contstructor. Note: the components should already be reduced. dcLabelNoReduce :: Component -> Component -> DCLabel dcLabelNoReduce = DCLabel -- | Element in the DCLabel lattice corresponding to the most secret -- and least trustworthy data. -- @dcTop = \< False, True \> @. dcTop :: DCLabel dcTop = dcLabel dcFalse dcTrue -- | Element in the DCLabel lattice corresponding to the least secret -- and most trustworthy data. -- @dcTop = \< True, False \> @. dcBottom :: DCLabel dcBottom = dcLabel dcTrue dcFalse -- | Element in the DCLabel lattice corresponding to public data. -- @dcPub = \< True, True \> @. This corresponds to data that is not -- secret nor trustworthy. dcPub :: DCLabel dcPub = DCLabel { dcSecrecy = dcTrue, dcIntegrity = dcTrue } -- -- Bounded by \< True, False \> and \< False, True \> -- instance Bounded DCLabel where minBound = dcBottom maxBound = dcTop -- -- Lattice operations -- instance Label DCLabel where -- | Partial /can-flow-to/ relation on labels. canFlowTo l1 l2 = (dcSecrecy l2 `dcImplies` dcSecrecy l1) && (dcIntegrity l1 `dcImplies` dcIntegrity l2) -- | The least upper bound of two labels, i.e., the join. lub l1 l2 = DCLabel { dcSecrecy = dcReduce $ dcSecrecy l1 `dcAnd` dcSecrecy l2 , dcIntegrity = dcReduce $ dcIntegrity l1 `dcOr` dcIntegrity l2 } -- | The greatest lower bound of two labels, i.e., the meet. glb l1 l2 = DCLabel { dcSecrecy = dcReduce $ dcSecrecy l1 `dcOr` dcSecrecy l2 , dcIntegrity = dcReduce $ dcIntegrity l1 `dcAnd` dcIntegrity l2 } -- -- Helpers -- -- | Logical implication. dcImplies :: Component -> Component -> Bool dcImplies DCFalse _ = True dcImplies _ DCFalse = False dcImplies f1@(DCFormula cs1) f2@(DCFormula cs2) | isTrue f2 = True | isTrue f1 = False | otherwise = Set.foldl' dcImpliesDisj True cs2 where dcImpliesDisj :: Bool -> Clause -> Bool dcImpliesDisj False _ = False dcImpliesDisj _ (Clause c2) = Set.foldl' f False cs1 where f True _ = True f _ c1 = unClause c1 `Set.isSubsetOf` c2 -- | Logical conjunction dcAnd :: Component -> Component -> Component dcAnd x y | isFalse x || isFalse y = dcFalse | otherwise = DCFormula $! unDCFormula x `Set.union` unDCFormula y -- | Logical disjunction dcOr :: Component -> Component -> Component dcOr x y | isTrue x || isTrue y = dcTrue dcOr x y | isFalse x = y | isFalse y = x | otherwise = let cs1 = unDCFormula x cs2 = unDCFormula y in DCFormula $! doOr cs1 cs2 where -- | Perform disjunction of two components. doOr :: Set Clause -> Set Clause -> Set Clause doOr cs1 cs2 = Set.foldl' disjFunc Set.empty cs2 where disjFunc acc c = acc `Set.union` singleOr c cs1 -- | Given a clause and a formula, perform logical or of -- clause with every clause in formula. singleOr :: Clause -> Set Clause -> Set Clause singleOr (Clause c1) = Set.map (Clause . Set.union c1 . unClause) -- | Reduce component to conjunction normal form by removing clauses -- implied by other. dcReduce :: Component -> Component dcReduce f | isFalse f || isTrue f = f | otherwise = DCFormula . doReduce . unDCFormula $ f where doReduce cs | Set.null cs = cs doReduce cs = let (x@(Clause x'), xs) = Set.deleteFindMin cs ys = doReduce $ Set.filter (not . Set.isSubsetOf x' . unClause) xs in Set.singleton x `Set.union` ys