diff --git a/DCLabel.hs b/DCLabel.hs new file mode 100644 --- /dev/null +++ b/DCLabel.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +{-# LANGUAGE Safe #-} +#endif +{- | + +This module re-export the core /DCLabel/ interface. For a description +of DCLabels see "DCLabel.Core". + +-} + +module DCLabel ( module DCLabel.Core + , module DCLabel.Privs + , module DCLabel.DSL + ) where + +import DCLabel.Core ( + Principal, principal + , Clause, clause + , Component, dcTrue, dcFalse, dcFormula + , isTrue, isFalse + , DCLabel, dcSecrecy, dcIntegrity, dcLabel + , dcBot, dcTop, dcPub + , canFlowTo, dcJoin, dcMeet + ) +import DCLabel.Privs +import DCLabel.DSL +import DCLabel.Serialize () diff --git a/DCLabel/Core.hs b/DCLabel/Core.hs --- a/DCLabel/Core.hs +++ b/DCLabel/Core.hs @@ -1,549 +1,274 @@ {-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) && (__GLASGOW_HASKELL__ < 704) -{-# LANGUAGE SafeImports #-} -#endif -#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 704) -{-# LANGUAGE Unsafe #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +{-# LANGUAGE Safe #-} #endif -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} - +{-# LANGUAGE DeriveDataTypeable #-} {-| -This module implements Disjunction Category Labels. -A DCLabel is a pair of 'secrecy' and 'integrity' category sets or -components, of type 'Component'. Each component is simply a set of -clauses in propositional logic (without negation). A component -can either correspond to the term 'MkComponentAll', representing -falsehood, or a set of categories (clauses): (of type 'Conj') -corresponding to the conjunction of ategories (of type 'Disj'). -Each category, in turn, is a disjunction of 'Principal's, where -a 'Principal' is just a 'ByteString' whose meaning is up to the -application. +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 category imposes an information flow restriction. In the case of -secrecy, a category 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 constructing a category -are said to /own/ the category. +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 categories of @L_2@ must at least as restrictive as -all the restrictions imposed by the categories of @L_1@ (hence the conjunction) +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 +label check is implemented by the 'canFlowTo' function. For labels @L_1=\@, @L_2=\@ the can-flow-to relation is satisfied -if the secrecy category set @S_2@ 'implies' @S_1@ and @I_1@ 'implies' @I_2@ +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]},{}\> ⊑ \<{[P_1]},{}\>@ because data +For example, @\ ⊑ \@ because data that can be read by @P_1@ is more restricting than that readable by @P_1@ -or @P_2@. Conversely, @\<{{},[P_1]}\> ⊑ \<{},[P_1 ⋁ P_2]},{}\>@ +or @P_2@. Conversely, @\ ⊑ \@ because data vouched for by @P_1@ or @P_2@ is more permissive than just @P_1@ -(note the same idea holds when writing to sinks with such labeling). - -A piece of a code running with a privilege object (of type 'TCBPriv'), i.e., -owning a 'Principal' confers the right to modify labels by removing any -'secrecy' categories containing that 'Principal' and adding any 'integrity' -categories containing the 'Principal' (hence the name disjunction categories: -the category @[P1 ⋁ P2]@ can be /downgraded/ by either 'Principal' -@P1@ or @P2@). More specifically, privileges can be used to bypass -information flow restrictions by using the more permissive \"can-flow-to given -permission\" relation:⊑ᵨ. The label check function implementing -this restriction is 'canflowto_p', taking an additional argument (of type -'TCBPriv'). For example, if @L_1=\<{[P_1 ⋁ P_2] ⋀ [P_3]},{}\>@, -and @L_2=\<{[P_1]},{}\>@, then @L_1 ⋢ L_2@, but given a privilege -object corresponding to @[P_3]@ the @L_1 ⊑ᵨ L_2@ holds. - -To construct DC labels and privilege objects the constructors exported by -this module may be used, but we strongly suggest using "DCLabel.NanoEDSL" -as exported by "DCLabel.TCB" and "DCLabel.Safe". The former is to be used by -trusted code only, while the latter module should be imported by untrusted -code as it prevents the creation of arbitrary privileges. +(note the same principle holds when writing to sinks with such labeling). -} -module DCLabel.Core ( -- * Components - -- $labels - Disj(..), Conj(..), Component(..) - , emptyComponent, allComponent - , Lattice(..) - , ToLNF(..) - -- ** DC Components - , DCLabel(..) - -- * Principals - , Principal(..), CreatePrincipal(..) - -- * Privileges - -- $privs - , TCBPriv(..), Priv - , RelaxedLattice(..) - , noPriv, rootPrivTCB - , delegatePriv, createPrivTCB - , CanDelegate(..), Owns(..) - -- * Component/internal operations - , and_component, or_component, cleanComponent, implies - , DisjToFromList(..) - , listToComponent, componentToList - ) where +module DCLabel.Core ( + -- * Principals + Principal(..), principal + -- * Clauses + , Clause(..), clause + -- * Components + -- $component + , Component(..) + , dcTrue, dcFalse, dcFormula + , isTrue, isFalse + -- * Labels + , DCLabel(..), dcLabel, dcLabelNoReduce + , dcBot, dcTop, dcPub + , canFlowTo, dcJoin, dcMeet + -- * Internal + , dcReduce, dcImplies + , dcAnd, dcOr + ) where +import qualified Data.ByteString.Char8 as S8 +import Data.Typeable +import Data.Set (Set) +import qualified Data.Set as Set -#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) -import safe Data.List (nub, sort, (\\)) -import safe Data.Maybe (fromJust) -import safe Data.Monoid -import safe Data.Functor ((<$>)) -#else -import Data.List (nub, sort, (\\)) -import Data.Maybe (fromJust) -import Data.Monoid -import safe Data.Functor ((<$>)) -#endif +import Data.List (intercalate) -import qualified Data.ByteString as B -import qualified Data.ByteString.Char8 as C -import Data.Serialize +type S8 = S8.ByteString + -- --- Categories +-- Principals -- --- | A category, i.e., disjunction, of 'Principal's. --- The empty list '[]' corresponds to the disjunction of all principals. --- Conceptually, @[] = [P_1 ⋁ P_2 ⋁ ...]@ -newtype Disj = MkDisj { disj :: [Principal] } - deriving (Eq, Ord, Show, Read) +-- | 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 } + deriving (Eq, Ord, Typeable) +instance Show Principal where + show = S8.unpack . principalName --- | A category set, i.e., a conjunction of disjunctions. --- The empty list '[]' corresponds to the single disjunction of all principals. --- In other words, conceptually, @[] = {[P_1 ⋁ P_2 ⋁ ...]}@ --- Logically '[]' = @True@. -newtype Conj = MkConj { conj :: [Disj] } - deriving (Eq, Ord, Show, Read) +-- | Principal constructor +principal :: S8 -> Principal +principal = Principal -- --- Components +-- Category - disjunction clauses -- -{- $labels - A component is a conjunction of disjunctions of principals. A - 'DCLabel' is simply a pair of such components. Hence, we define - almost all operations in terms of this construct, from which the - 'DCLabel' implementation follows almost trivially. Moreover, we - note that secrecy-only and integrity-only labels are implemented - in "DCLabel.Secrecy" and "DCLabel.Integrity", respectively. --} - --- | Labels form a partial order according to the ⊑ relation. --- Specifically, this means that for any two labels @L_1@ and @L_2@ there is a --- unique label @L_3 = L_1 ⊔ L_2@, known as the /join/, such that --- @L_1 ⊑ L_3@ and @L_2 ⊑ L_3@. Similarly, there is a unique label --- @L_3' = L_1 ⊓ L_2@, known as the /meet/, such that --- @L_3 ⊑ L_1@ and @L_3 ⊑ L_2@. This class defines a /bounded/ --- lattice, which further requires the definition of the /bottom/ ⊥ and --- /top/ ⊤ elements of the lattice, such that @⊥ ⊑ L@ and --- @L ⊑ ⊤@ for any label @L@. -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 components is a conjunction of disjunctions, where @MkComponentAll@ is --- the constructor that is associated with the logical @False@. -data Component = MkComponentAll - | MkComponent { component :: Conj } - deriving (Show, Read) +-- | 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 } + deriving (Eq, Ord, Typeable) --- | Components have a unique LNF (see 'ToLNF') form, and equality testing is --- perfomed on labels of this form. -instance Eq Component where - (==) MkComponentAll MkComponentAll = True - (==) MkComponentAll _ = False - (==) _ MkComponentAll = False - (==) l1 l2 = (component . toLNF $ l1) == (component . toLNF $ l2) +instance Ord Clause where + (Clause c1) <= (Clause c2) = + case () of + _ | Set.size c1 == Set.size c2 -> c1 <= c2 + _ -> Set.size c1 < Set.size c2 --- | A component without any disjunctions or conjunctions. This --- component, conceptually corresponds to the label consisting of --- a single category containing all principals. Conceptually (in a --- closed-world system), --- @emptyComponent = \<{[P_1 ⋁ P_2 ⋁ ...]}\>@. --- Logically, of course, this is equivalent to @True@. -emptyComponent :: Component -emptyComponent = MkComponent (MkConj []) +instance Show Clause where + show c = let ps = map show . Set.toList $! unClause c + in parens . intercalate " \\/ " $! ps + where parens x = "[" ++ x ++ "]" --- | The dual of 'emptyComponent', 'allComponent' consists of the conjunction of --- all possible disjunctions, i.e., it is the label that implies all --- other labels. Conceptually (in a closed-world system), --- @allComponent = \<{[P_1] ⋀ [P_2] ⋀ ...}\>@ --- Logically, of course, this is equivalent to @False@. -allComponent :: Component -allComponent = MkComponentAll +-- | Clause constructor +clause :: Set Principal -> Clause +clause = Clause --- | Predicate function that returns @True@ if the label corresponds to --- the 'emptyComponent'. -isEmptyComponent :: Component -> Bool -isEmptyComponent MkComponentAll = False -isEmptyComponent l = and [ null (disj d) | d <- conj (component l) ] +-- | 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) } + -- ^ Conjunction of disjunction categories + deriving (Eq, Typeable) --- | Predicate function that retuns @True@ if the label corresponds to --- the 'allComponent'. -isAllComponent :: Component -> Bool -isAllComponent MkComponentAll = True -isAllComponent _ = False +instance Show Component where + show c | isFalse c = "|False" + | isTrue c = "|True" + | otherwise = let cs = map show . Set.toList $! unDCFormula c + in parens . intercalate " /\\ " $! cs + where parens x = "{" ++ x ++ "}" +-- | Logical @True@. +dcTrue :: Component +dcTrue = DCFormula Set.empty --- --- Helper functions --- +-- | Logical @False@. +dcFalse :: Component +dcFalse = DCFalse +-- | Arbitrary formula from a clause. +dcFormula :: Set Clause -> Component +dcFormula = DCFormula --- | Given two components, take the union of the disjunctions, i.e., simply --- perform an \"and\". Note the new component is not necessarily in LNF. -and_component :: Component -> Component -> Component -and_component l1 l2 | isAllComponent l1 || isAllComponent l2 = allComponent - | otherwise = MkComponent {component = MkConj $ - conj (component l1) ++ conj (component l2)} +-- | Is the component @True@. +isTrue :: Component -> Bool +isTrue = (== dcTrue) --- | Given two components, perform an \"or\". --- Note that the new component is not necessarily in LNF. -or_component :: Component -> Component -> Component -or_component l1 l2 | isEmptyComponent l1 || isEmptyComponent l2 = emptyComponent - | isAllComponent l2 = l1 - | isAllComponent l1 = l2 - | otherwise = MkComponent . MkConj $ - [ MkDisj (disj d1 ++ disj d2) - | d1 <- (conj (component l1)) - , d2 <- (conj (component l2)) - , not . null . disj $ d1 - , not . null . disj $ d2] +-- | Is the component @False@. +isFalse :: Component -> Bool +isFalse = (== dcFalse) --- | Determines if a conjunction of disjunctions, i.e., a component, implies --- (in the logical sense) a disjunction. In other words, it checks if --- d_1 ⋀ ... ⋀ d_n => d_1. -- --- Properties: --- --- * ∀ X, 'allComponent' \``impliesDisj`\` X = True --- --- * ∀ X, X \``impliesDisj`\` 'emptyComponent' = True --- --- * ∀ X≠'emptyComponent', 'emptyComponent' \``impliesDisj`\` X = False +-- Labels -- --- Note that the first two guards are only included --- for safety; the function is always called with a non-ALL component and --- non-null disjunction. -impliesDisj :: Component -> Disj -> Bool -impliesDisj l d | isAllComponent l = True -- Asserts 1 - | null (disj d) = True -- Asserts 2 - | otherwise = or [ and [ e `elem` (disj d) | e <- disj d1 ] - | d1 <- conj (component l) - , not (isEmptyComponent l) ] -- Asserts 3 --- | Determines if a component logically implies another component. --- In other words, d_1 ⋀ ... ⋀ d_n => d_1' ⋀ ... ⋀ d_n'. --- --- Properties: --- --- * ∀ X, 'allComponent' \``implies`\` X := True --- --- * ∀ X≠'allComponent', X \``implies`\` 'allComponent' := False --- --- * ∀ X, X \``implies`\` 'emptyComponent' := True --- --- * ∀ X≠'emptyComponent', 'emptyComponent' \``implies`\` X := False -implies :: Component -> Component -> Bool -implies l1 l2 | isAllComponent l1 = True -- Asserts 1 - | isAllComponent l2 = False -- Asserts 2 - | otherwise = and [ impliesDisj (toLNF l1) d - | d <- conj . component . toLNF $ l2 ] - - --- | Removes any duplicate principals from categories, and any duplicate --- categories from the component. To return a clean component, it sorts the --- component and removes empty disjunctions. -cleanComponent :: Component -> Component -cleanComponent MkComponentAll = MkComponentAll -cleanComponent l = MkComponent . MkConj . sort . nub $ - [ MkDisj ( (sort . nub) (disj d) ) | d <- conj (component l) - , not . null $ disj d ] +{- $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. +-} --- | Class used to reduce labels and components to unique label normal form --- (LNF), which corresponds to conjunctive normal form of principals. We use --- this class to overload the reduce function used by the 'Component', --- 'DCLabel', etc. -class ToLNF a where - toLNF :: a -> a +-- | A @DCLabel@ is a pair of secrecy and integrity 'Component's. +data DCLabel = DCLabel { dcSecrecy :: !Component + , dcIntegrity :: !Component } + deriving (Eq, Typeable) --- | Reduce a 'Component' to LNF. --- First it applies @cleanComponent@ 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 component that implies it. -instance ToLNF Component where - toLNF MkComponentAll = MkComponentAll - toLNF l = MkComponent . MkConj $ l' \\ extraneous - where l' = conj . component $ cleanComponent l - extraneous = [ d2 | d1 <- l', d2 <- l', d1 /= d2 - , impliesDisj ((MkComponent . MkConj) [d1]) d2 ] +instance Show DCLabel where + show l = let s = dcSecrecy l + i = dcIntegrity l + in "< " ++ show s ++ " , " ++ show i ++ " >" --- --- DC Labels --- +-- | Label constructor. Note that each component is first reduced 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 --- --- DC Labels : (Secrecy, Integrity) --- +-- | Minimal element of the DCLabel lattice, /bottom/ ⊥, +-- such that @⊥ ⊑ L@ for any label @L@. +-- Bottom is defined as: @ ⊥ = \< True, False \> @ dcBot :: DCLabel +dcBot :: DCLabel +dcBot = DCLabel { dcSecrecy = dcTrue, dcIntegrity = dcFalse } --- | A @DCLabel@ is a pair of secrecy and integrity category sets, i.e., --- a pair of 'Component's. -data DCLabel = MkDCLabel { secrecy :: Component -- ^ Integrity category set. - , integrity :: Component -- ^ Secrecy category set. - } - deriving (Eq, Show, Read) +-- | Maximum element of the DCLabel lattice, /top/ ⊤, +-- such that @L ⊑ ⊤@ for any label @L@. +-- Bottom is defined as: @ ⊤ = \< False, True \> @ +dcTop :: DCLabel +dcTop = DCLabel { dcSecrecy = dcFalse, dcIntegrity = dcTrue } --- | Each 'DCLabel' can be reduced a unique label representation in LNF, using --- the 'toLNF' function. -instance ToLNF DCLabel where - toLNF l = MkDCLabel { secrecy = toLNF (secrecy l) - , integrity = toLNF (integrity l)} +-- | 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 } --- | Elements of 'DCLabel' form a bounded lattice, where: -- --- * @⊥ = \<'emptyComponent', 'allComponent'\>@ --- --- * @⊤ = \<'allComponent', 'emptyComponent'\>@ --- --- * @ \ ⊔ \ = \@ --- --- * @ \ ⊓ \ = \@ +-- Lattice operations -- --- * @ \ ⊑ \ = S_2 => S_1 ⋀ I_1 => I_2@ -instance Lattice DCLabel where - bottom = MkDCLabel { secrecy = emptyComponent - , integrity = allComponent } - top = MkDCLabel { secrecy = allComponent - , integrity = emptyComponent } - join l1 l2 = let s3 = (secrecy l1) `and_component` (secrecy l2) - i3 = (integrity l1) `or_component` (integrity l2) - in toLNF $ MkDCLabel { secrecy = s3 - , integrity = i3 } - meet l1 l2 = let s3 = (secrecy l1) `or_component` (secrecy l2) - i3 = (integrity l1) `and_component` (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')) +-- | Partial /can-flow-to/ relation on labels. +canFlowTo :: DCLabel -> DCLabel -> Bool +canFlowTo l1 l2 = (dcSecrecy l2 `dcImplies` dcSecrecy l1) && + (dcIntegrity l1 `dcImplies` dcIntegrity l2) --- --- Principals --- --- | Principal is a simple string representing a source of authority. Any piece --- of code can create principals, regarless of how untrusted it is. However, --- for principals to be used in integrity components or be ignoerd a --- corresponding privilege ('TCBPriv') must be created (by trusted code) or --- delegated. -newtype Principal = MkPrincipal { name :: B.ByteString } - deriving (Eq, Ord, Show, Read) +-- | The least upper bound of two labels, i.e., the join. +dcJoin :: DCLabel -> DCLabel -> DCLabel +dcJoin l1 l2 = DCLabel + { dcSecrecy = dcReduce $ dcSecrecy l1 `dcAnd` dcSecrecy l2 + , dcIntegrity = dcReduce $ dcIntegrity l1 `dcOr` dcIntegrity l2 } --- | Generates a principal from an string. -class CreatePrincipal s where - principal :: s -> Principal +-- | The greatest lower bound of two labels, i.e., the meet. +dcMeet :: DCLabel -> DCLabel -> DCLabel +dcMeet l1 l2 = DCLabel + { dcSecrecy = dcReduce $ dcSecrecy l1 `dcOr` dcSecrecy l2 + , dcIntegrity = dcReduce $ dcIntegrity l1 `dcAnd` dcIntegrity l2 } -instance CreatePrincipal B.ByteString where - principal = MkPrincipal -instance CreatePrincipal String where - principal = MkPrincipal . C.pack - -- --- Privileges --- - -{- $privs -As previously mentioned privileges allow a piece of code to bypass certain -information flow restrictions. Like principals, privileges of type 'Priv' -may be created by any piece of code. A privilege is simply a conjunction of -disjunctions, i.e., a 'Component' where a category consisting of a single -principal corresponds to the notion of /owning/ that principal. We, however, -allow for the more general notion of ownership of a category as to create a -privilege-hierarchy. Specifically, a piece of code exercising a privilege @P@ -can always exercise privilege @P'@ (instead), if @P' => P@. This is similar to -the DLM notion of \"can act for\", and, as such, we provide a function which -tests if one privilege may be use in pace of another: 'canDelegate'. - -Note that the privileges form a partial order over @=>@, such that -@'rootPrivTCB' => P@ and @P => 'noPriv'@ for any privilege @P@. -As such we have a privilege hierarchy which can be concretely built through -delegation, with 'rootPrivTCB' corresponding to the /root/, or all, privileges -from which all others may be created. More specifically, given a minted -privilege @P'@ of type 'TCBPriv', and an un-minted privilege @P@ of type 'Priv', -any piece of code can use 'delegatePriv' to mint @P@, assuming @P' => P@. - -Finally, given a set of privileges a piece of code can check if it owns a -category using the 'owns' function. --} - --- | Privilege object is just a conjunction of disjunctions, i.e., 'Component'. --- A trusted privileged object must be introduced by trusted code, after which --- trusted privileged objects can be created by delegation. -data TCBPriv = MkTCBPriv { priv :: Component } - deriving (Eq, Show) - --- | Untrusted privileged object, which can be converted to a 'TCBPriv' with --- 'delegatePriv'. -type Priv = Component - --- | 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 l1) - , integrity = (and_component (priv p) (integrity l1)) } - l2' = MkDCLabel { secrecy = (and_component (priv p) (secrecy l2)) - , integrity = (integrity l2) } - in canflowto l1' l2' - - --- | Given trusted privilege and a \"desired\" untrusted privilege, --- return a trusted version of the untrusted privilege, if the --- provided (trusted) privilege 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 = emptyComponent } - --- | Privilege object corresponding to the \"root\", or all privileges. --- Any other privilege may be delegated using this privilege object and it must --- therefore not be exported to untrusted code. -rootPrivTCB :: TCBPriv -rootPrivTCB = MkTCBPriv { priv = allComponent } - --- | 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) - --- | @TCBPriv@ is an instance of 'Monoid'. -instance Monoid TCBPriv where - mempty = noPriv - mappend p1 p2 = createPrivTCB $ toLNF ((priv p1) `and_component` (priv p2)) - - --- | Class used for checking if a computation can use a privilege in place of --- the other. This notion is similar to the DLM \"can-act-for\". -class CanDelegate a b where - -- | Can use first privilege in place of second. - canDelegate :: a -> b -> Bool - -instance CanDelegate Priv Priv where - canDelegate p1 p2 = p1 `implies` p2 - -instance CanDelegate Priv TCBPriv where - canDelegate p1 p2 = p1 `implies` (priv p2) - -instance CanDelegate TCBPriv Priv where - canDelegate p1 p2 = (priv p1) `implies` p2 - -instance CanDelegate TCBPriv TCBPriv where - canDelegate p1 p2 = (priv p1) `implies` (priv p2) - - --- | We say a 'TCBPriv' privilege object owns a category when the privileges --- allow code to bypass restrictions implied by the category. This is the --- case if and only if the 'TCBPriv' object contains one of the 'Principal's --- in the 'Disj'. This class is used to check ownership -class Owns a where - -- | Checks if category restriction can be bypassed given the privilege. - owns :: TCBPriv -> a -> Bool - -instance Owns Disj where - owns p d = priv p `impliesDisj` d - -instance Owns Component where - owns p l = priv p `implies` l - - - --- | Class used to convert list of principals to a disjunction category and --- vice versa. -class DisjToFromList a where - listToDisj :: [a] -> Disj -- ^ Given list return category. - disjToList :: Disj -> [a] -- ^ Given category return list. - --- | To/from 'Principal's and 'Disj'unction categories. -instance DisjToFromList Principal where - listToDisj ps = MkDisj ps - disjToList d = disj d - --- | To/from 'String's and 'Disj'unction categories. -instance DisjToFromList String where - listToDisj ps = MkDisj $ map (principal . C.pack) ps - disjToList d = map (C.unpack . name) $ disj d - --- | To/from 'ByteString's and 'Disj'unction categories. -instance DisjToFromList B.ByteString where - listToDisj ps = MkDisj $ map principal ps - disjToList d = map name $ disj d - --- | Given a list of categories, return a component. -listToComponent :: [Disj] -> Component -- ^ Given list return category. -listToComponent = MkComponent . MkConj - --- | Given a component return a list of categories. -componentToList :: Component -> [Disj] -- ^ Given category return list. -componentToList = conj . component - - - +-- Helpers -- --- Serialize instances --- - -instance Serialize Principal where - put = put . name - get = MkPrincipal <$> get - -instance Serialize Disj where - put = put . disj - get = MkDisj <$> get - -instance Serialize Conj where - put = put . conj - get = MkConj <$> get +-- | 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 -instance Serialize Component where - put c | c == MkComponentAll = put (Nothing :: Maybe Conj) - | otherwise = put (Just $ component c) - get = do mc <- get - case mc of - Nothing -> return MkComponentAll - Just c -> return $ MkComponent c +-- | Logical conjunction +dcAnd :: Component -> Component -> Component +dcAnd x y | isFalse x || isFalse y = dcFalse + | otherwise = DCFormula $! unDCFormula x `Set.union` unDCFormula y -instance Serialize DCLabel where - put (MkDCLabel s i) = put s >> put i - get = do s <- get - i <- get - return $ MkDCLabel s i +-- | 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 diff --git a/DCLabel/DSL.hs b/DCLabel/DSL.hs new file mode 100644 --- /dev/null +++ b/DCLabel/DSL.hs @@ -0,0 +1,153 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +{-# LANGUAGE Safe #-} +#endif +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} + +{-| + This module implements a ``nano``, very simple, embedded domain + specific language to create 'Component's and privilage descriptions + from conjunctions of principal disjunctions. + + A 'Component'/'DCPrivDesc' is created using the ('\/') and ('/\') operators. + The disjunction operator ('\/') is used to create a 'Clause' from + 'Principal's, ByteStrings, or a disjunctive sub-expression. For example: + + @ + p1 = 'principal' \"p1\" + p2 = 'principal' \"p2\" + p3 = 'principal' \"p3\" + e1 = p1 '\/' p2 + e2 = e1 '\/' \"p4\" + @ + + Similarly, the conjunction operator ('/\') is used to create category-sets + from 'Principal's, ByteStrings, and conjunctive or disjunctive sub-expressions. + For example: + + @ + e3 = p1 '\/' p2 + e4 = e1 '/\' \"p4\" '/\' p3 + @ + + /Note/ that because a clause consists of a disjunction of principals, and a + component is composed of the conjunction of categories, ('\/') binds + more tightly than ('/\'). + + Given two 'Component's, one for secrecy and one for integrity, you + can create a 'DCLabel' with 'dcLabel'. Given a 'Component' you can + create a 'DCPrivDesc' using 'dcPrivDesc'. Finally, given a 'DCPriv' + and 'DCPrivDesc' you can create a new minted privilege with + 'dcDelegatePriv'. + + + Consider the following, example: + + @ + l1 = \"Alice\" '\/' \"Bob\" '/\' \"Carla\" + l2 = \"Alice\" '/\' \"Carla\" + dc1 = 'dcLabel' l1 l2 + dc2 = 'dcLabel' ('toComponent' \"Djon\") ('toComponent' \"Alice\") + pr = 'dcPrivTCB' . 'dcPrivDesc' $ \"Alice\" '/\' \"Carla\" + @ + +where + + * @ dc1 = \<{[\"Alice\" ⋁ \"Bob\"] ⋀ [\"Carla\"]} , {[\"Alice\"] ⋀ [\"Carla\"]}\>@ + + * @ dc2 = \<{[\"Djon\"]} , {[\"Alice\"]}\>@ + + * @ 'canFlowTo' dc1 dc2 = False @ + + * @ 'canFlowToP' pr dc1 dc2 = True@ + +-} + +module DCLabel.DSL ( -- * Operators + (\/), (/\), ToComponent(..) + , fromList, toList + -- * Aliases + , everybody, anybody + ) where + +import DCLabel.Core +import qualified Data.Set as Set +import qualified Data.ByteString.Char8 as S8 + +type S8 = S8.ByteString + +-- | Convert a type (e.g., 'Clause', 'Principal') to a label component. +class ToComponent a where + -- | Convert to 'Component' + toComponent :: a -> Component + +-- | Identity of 'Component'. +instance ToComponent Component where + toComponent = id +-- | Convert singleton 'Clause' to 'Component'. +instance ToComponent Clause where + toComponent c = DCFormula $! Set.singleton c +-- | Convert singleton 'Principal' to 'Component'. +instance ToComponent Principal where + toComponent p = toComponent . Clause $! Set.singleton p +-- | Convert singleton 'Principal' (in the form of a @ByteString@)to 'Component'. +instance ToComponent S8 where + toComponent = toComponent . principal +-- | Convert singleton 'Principal' (in the form of a 'String')to 'Component'. +instance ToComponent String where + toComponent = toComponent . S8.pack + +infixl 7 \/ +infixl 6 /\\ + +-- | Conjunction of two 'Principal'-based elements. +-- +-- @ +-- infixl 6 /\ +-- @ +-- +(/\) :: (ToComponent a, ToComponent b) => a -> b -> Component +a /\ b = dcReduce $! toComponent a `dcAnd` toComponent b + +-- | Disjunction of two 'Principal'-based elements. +-- +-- @ +-- infixl 7 \\/ +-- @ +-- +(\/) :: (ToComponent a, ToComponent b) => a -> b -> Component +a \/ b = dcReduce $! toComponent a `dcOr` toComponent b + +-- +-- Aliases +-- + +-- | Logical falsehood can be thought of as the component containing +-- every possible principal: +-- +-- > everybody = dcFalse +-- +everybody :: Component +everybody = dcFalse + +-- | Logical truth can be thought of as the component containing +-- no specific principal: +-- +-- > anybody = dcTrue +-- +anybody :: Component +anybody = dcTrue + + +-- | Convert a 'Component' to a list of list of 'Principal's if the +-- 'Component' does not have the value 'DCFalse'. In the latter case +-- the function returns 'Nothing'. +toList :: Component -> [[Principal]] +toList DCFalse = error "toList: Invalid use, expected DCFormula" +toList (DCFormula cs) = map (Set.toList . unClause) $! Set.toList cs + +-- | Convert a list of list of 'Principal's to a 'Component'. Each +-- inner list is considered to correspond to a 'Clause'. +fromList :: [[Principal]] -> Component +fromList ps = DCFormula . Set.fromList $! map (Clause . Set.fromList) ps diff --git a/DCLabel/Integrity.hs b/DCLabel/Integrity.hs deleted file mode 100644 --- a/DCLabel/Integrity.hs +++ /dev/null @@ -1,31 +0,0 @@ -{-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) -{-# LANGUAGE Trustworthy #-} -#endif -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} --- | This module implements integrity-only DC Labels. -module DCLabel.Integrity ( ILabel(..) ) where - -import DCLabel.Core - --- | An integrity-only DC label. -newtype ILabel = MkILabel DCLabel - deriving (Eq, Show, Read) - -instance ToLNF ILabel where - toLNF (MkILabel l) = MkILabel (toLNF l) - -instance Lattice ILabel where - bottom = MkILabel bottom - top = MkILabel top - join (MkILabel l1) (MkILabel l2) = MkILabel $ - join l1 { secrecy = emptyComponent } l2 { secrecy = emptyComponent } - meet (MkILabel l1) (MkILabel l2) = MkILabel $ - meet l1 { secrecy = emptyComponent } l2 { secrecy = emptyComponent } - canflowto (MkILabel l1) (MkILabel l2) = - canflowto l1 { secrecy = emptyComponent } l2 { secrecy = emptyComponent } - -instance RelaxedLattice ILabel where - canflowto_p p (MkILabel l1) (MkILabel l2) = - canflowto_p p l1 { secrecy = emptyComponent } l2 { secrecy = emptyComponent } diff --git a/DCLabel/NanoEDSL.hs b/DCLabel/NanoEDSL.hs deleted file mode 100644 --- a/DCLabel/NanoEDSL.hs +++ /dev/null @@ -1,236 +0,0 @@ -{-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) -{-# LANGUAGE Trustworthy #-} -#endif -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} - -{-| This module implements a ``nano``, very simple, embedded domain specific - language to create 'Component's and 'Priv'ilages from conjunctions of - principal disjunctions. - - A 'Component'/'Priv' is created using the ('.\/.') and ('./\.') operators. - The disjunction operator ('.\/.') is used to create a category from - 'Principal's, 'String's, or a disjunctive sub-expression. For example: - - @ - p1 = 'principal' \"p1\" - p2 = 'principal' \"p2\" - p3 = 'principal' \"p3\" - e1 = p1 '.\/.' p2 - e2 = e1 '.\/.' \"p4\" - @ - - Similarly, the conjunction operator ('./\.') is used to create category-sets - from 'Principals', 'Strings', and conjunctive or disjunctive sub-expressions. - For example: - - @ - e3 = p1 '.\/.' p2 - e4 = e1 './\.' \"p4\" './\.' p3 - @ - - /Note/ that because a category consists of a disjunction of principals, and a - category set is composed of the conjunction of categories, ('.\/.') binds - more tightly than ('./\.'). - - Given two 'Component's, one for secrecy and one for integrity, you can - create a 'DCLabel' with 'newDC'. And, similarly, given a 'TCBPriv' and 'Priv' - you can create a new minted privilege with 'newTCBPriv'. - - - Consider the following, example: - - @ - l1 = \"Alice\" '.\/.' \"Bob\" './\.' \"Carla\" - l2 = \"Alice\" './\.' \"Carla\" - dc1 = 'newDC' l1 l2 - dc2 = 'newDC' \"Deian\" \"Alice\" - pr = 'createPrivTCB' $ 'newPriv' (\"Alice\" './\.' \"Carla\") - @ - -where - - * @ dc1 = \<{[\"Alice\" ⋁ \"Bob\"] ⋀ [\"Carla\"]} , {[\"Alice\"] ⋀ [\"Carla\"]}\>@ - - * @ dc2 = \<{[\"Deian\"]} , {[\"Alice\"]}\>@ - - * @ 'canflowto' dc1 dc2 = False @ - - * @ 'canflowto_p' pr dc1 dc2 = True@ - --} - -module DCLabel.NanoEDSL ( -- * Operators - (.\/.), (./\.) - , (<>), (><) - , singleton - -- * DCLabel creation - , newDC - -- * Privilege object creation - , NewPriv, newPriv, newTCBPriv - ) where - -import DCLabel.Core -import qualified Data.ByteString as B -import qualified Data.ByteString.Char8 as C -import Data.String - -infixl 7 .\/. -infixl 6 ./\. - --- | Class used to create single-principal labels. -class Singleton a where - singleton :: a -> Component -- ^ Creates a singleton component. - -instance Singleton Principal where - singleton p = MkComponent $ MkConj [ MkDisj [p] ] - -instance Singleton String where - singleton s = singleton (C.pack s) - -instance Singleton B.ByteString where - singleton s = MkComponent $ MkConj [ MkDisj [principal s] ] - - --- | Class used to create disjunctions. -class DisjunctionOf a b where - (.\/.) :: a -> b -> Component -- ^ Given two elements it joins them with ⋁ - -instance DisjunctionOf Principal Principal where - p1 .\/. p2 = MkComponent $ MkConj [ MkDisj [p1,p2] ] - -instance DisjunctionOf Principal Component where - p .\/. l = (singleton p) `or_component` l - -instance DisjunctionOf Component Principal where - l .\/. p = p .\/. l - -instance DisjunctionOf Component Component where - l1 .\/. l2 = l1 `or_component` l2 - -instance DisjunctionOf String String where - s1 .\/. s2 = singleton s1 .\/. singleton s2 - -instance DisjunctionOf String Component where - s .\/. l = singleton s .\/. l - -instance DisjunctionOf Component String where - l .\/. p = p .\/. l - - --- | Class used to create conjunctions. -class ConjunctionOf a b where - (./\.) :: a -> b -> Component -- ^ Given two elements it joins them with ⋀ - -instance ConjunctionOf Principal Principal where - p1 ./\. p2 = MkComponent $ MkConj [ MkDisj [p1], MkDisj [p2] ] - -instance ConjunctionOf Principal Component where - p ./\. l = singleton p `and_component` l - -instance ConjunctionOf Component Principal where - l ./\. p = p ./\. l - -instance ConjunctionOf Component Component where - l1 ./\. l2 = l1 `and_component` l2 - --- | Instances using strings and not principals -instance ConjunctionOf String String where - s1 ./\. s2 = singleton s1 ./\. singleton s2 - -instance ConjunctionOf String Component where - s ./\. l = singleton s `and_component` l - -instance ConjunctionOf Component String where - l ./\. s = s ./\. l - --- | Instances using disjunctions. -instance ConjunctionOf Disj Disj where - d1 ./\. d2 = MkComponent $ MkConj [ d1, d2 ] - -instance ConjunctionOf Disj Component where - d ./\. l = (MkComponent $ MkConj [d]) `and_component` l - -instance ConjunctionOf Component Disj where - l ./\. d = d ./\. l - -instance ConjunctionOf Principal Disj where - p ./\. d = singleton p ./\. d - -instance ConjunctionOf Disj Principal where - d ./\. p = p ./\. d - -instance ConjunctionOf String Disj where - p ./\. d = singleton p ./\. d - -instance ConjunctionOf Disj String where - d ./\. p = p ./\. d - - - --- | Empty component (logically this is @True@). -(<>) :: Component -(<>) = emptyComponent - --- | All component (logically this is @False@). -(><) :: Component -(><) = allComponent - ---- ---- Creating 'DCLabel's ---- - --- | Class used to create 'DCLabel's. -class NewDC a b where - newDC :: a -> b -> DCLabel -- ^ Given two elements create label. - -instance NewDC Component Component where - newDC l1 l2 = MkDCLabel l1 l2 - -instance NewDC Principal Component where - newDC p l = MkDCLabel (singleton p) l - -instance NewDC Component Principal where - newDC l p = MkDCLabel l (singleton p) - -instance NewDC Principal Principal where - newDC p1 p2 = MkDCLabel (singleton p1) (singleton p2) - -instance NewDC String Component where - newDC p l = MkDCLabel (singleton p) l - -instance NewDC Component String where - newDC l p = MkDCLabel l (singleton p) - -instance NewDC String String where - newDC p1 p2 = MkDCLabel (singleton p1) (singleton p2) - --- --- Creating 'Priv's and 'TCBPriv's. --- - --- | Class used to create 'Priv's and 'TCBPriv's. -class NewPriv a where - -- | Given element create privilege. - newPriv :: a -> Priv - -- | Given privilege and new element, create (maybe) trusted privileged object. - newTCBPriv :: TCBPriv -> a -> Maybe TCBPriv - newTCBPriv p = delegatePriv p . newPriv - -instance NewPriv Component where - newPriv = id - -instance NewPriv Principal where - newPriv p = singleton p - -instance NewPriv String where - newPriv p = singleton p - --- --- Instances of IsString --- - -instance IsString Principal where - fromString = principal . C.pack diff --git a/DCLabel/PrettyShow.hs b/DCLabel/PrettyShow.hs deleted file mode 100644 --- a/DCLabel/PrettyShow.hs +++ /dev/null @@ -1,57 +0,0 @@ -{-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) -{-# LANGUAGE Trustworthy #-} -#endif -{-| This module exports a function 'prettyShow' that pretty prints 'Principal's, -'Disj'unctions, 'Conj'unctions, 'Component's and 'DCLabel's. --} -module DCLabel.PrettyShow (PrettyShow(..), prettyShow) where - -import DCLabel.Core -import DCLabel.Secrecy -import DCLabel.Integrity -import Text.PrettyPrint - - - --- | Class used to create a 'Doc' type of DCLabel-related types -class PrettyShow a where - pShow :: a -> Doc -- ^ Convert to 'Doc'. - --- | Render a 'PrettyShow' type to a string. -prettyShow :: PrettyShow a => a -> String -prettyShow = render . pShow - -instance PrettyShow Disj where - pShow (MkDisj xs) = bracks $ showDisj xs - where showDisj [] = empty - showDisj [x] = pShow x - showDisj (x:ys) = pShow x <+> ( text "\\/") <+> showDisj ys - bracks x = lbrack <> x <> rbrack - -instance PrettyShow Conj where - pShow (MkConj []) = text "True" - pShow (MkConj (x:[])) = pShow x - pShow (MkConj (x:xs)) = pShow x <+> (text "/\\") <+> pShow (MkConj xs) - -instance PrettyShow Component where - pShow MkComponentAll = text "False" - pShow l = let (MkComponent c) = toLNF l - showC = pShow c - in if c == MkConj [] then showC else braces showC - -instance PrettyShow DCLabel where - pShow (MkDCLabel s i) = angle $ pShow s <+> comma <+> pShow i - where angle txt = (text "<") <> txt <> (text ">") - -instance PrettyShow Principal where - pShow (MkPrincipal s) = text (show s) - -instance PrettyShow TCBPriv where - pShow (MkTCBPriv p) = pShow p - -instance PrettyShow SLabel where - pShow (MkSLabel dcL) = pShow . secrecy $ dcL - -instance PrettyShow ILabel where - pShow (MkILabel dcL) = pShow . integrity $ dcL diff --git a/DCLabel/Privs.hs b/DCLabel/Privs.hs new file mode 100644 --- /dev/null +++ b/DCLabel/Privs.hs @@ -0,0 +1,79 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +{-# LANGUAGE Trustworthy #-} +#endif +{-# LANGUAGE TypeSynonymInstances #-} +{- | + +Privileges allow a piece of code to bypass certain information flow +restrictions imposed by labels. A privilege is simply a conjunction +of disjunctions of 'Principal's, i.e., a 'Component'. We say that a +piece of code containing a singleton 'Clause' owns the 'Principal' +composing the 'Clause'. However, we allow for the more general notion +of ownership of a clause, or category, as to create a +privilege-hierarchy. Specifically, a piece of code exercising a +privilege @P@ can always exercise privilege @P'@ (instead), if @P' => P@. +(This is similar to the DLM notion of \"can act for\".) Hence, if a +piece of code with certain privileges implies a clause, then it is +said to own the clause. Consequently it can bypass the restrictions of +the clause in any label. + +Note that the privileges form a partial order over logicla implication +(@=>@), such that @'allPrivTCB' => P@ and @P => 'noPriv'@ for any +privilege @P@. Hence, a privilege hierarchy which can be concretely +built through delegation, with 'allPrivTCB' corresponding to the +/root/, or all, privileges from which all others may be created. More +specifically, given a privilege @P'@ of type 'DCPriv', and a privilege +description @P@ of type 'DCPrivDesc', any piece of code can use +'delegatePriv' to \"mint\" @P@, assuming @P' => P@. + +-} + +module DCLabel.Privs ( + DCPrivDesc + , DCPriv + , noPriv + , dcDelegatePriv + , dcOwns + , canFlowToP + ) where + +import DCLabel.Core +import DCLabel.Privs.TCB +import qualified Data.Set as Set + + +-- | Given a privilege and a privilege description turn the privilege +-- description into a privilege (i.e., mint). Such delegation succeeds +-- only if the supplied privilege implies the privilege description. +dcDelegatePriv :: DCPriv -> DCPrivDesc -> Maybe DCPriv +dcDelegatePriv p pd = let c = unDCPriv $! p + in if c `dcImplies` pd + then Just $! dcPrivTCB pd + else Nothing + +-- | We say a piece of code having a privilege object (of type 'DCPriv') +-- owns a clause when the privileges allow code to bypass restrictions +-- imposed by the clause. This is the case if and only if the 'DCPriv' +-- object contains one of the 'Principal's in the 'Clause'. This +-- function can be used to make such checks. +dcOwns :: DCPrivDesc -> Clause -> Bool +dcOwns pd c = pd `dcImplies` dcFormula (Set.singleton c) + + +-- | Class used to implement the pre-order /can flow to/ given +-- privileges relation. +class CanFlowToP p where + -- | Can flow to relation given a set of privileges. + canFlowToP :: p -> DCLabel -> DCLabel -> Bool + +instance CanFlowToP DCPrivDesc where + canFlowToP 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 } + +instance CanFlowToP DCPriv where + canFlowToP p = canFlowToP (unDCPriv p) + diff --git a/DCLabel/Privs/TCB.hs b/DCLabel/Privs/TCB.hs new file mode 100644 --- /dev/null +++ b/DCLabel/Privs/TCB.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 704) +{-# LANGUAGE Unsafe #-} +#endif +{-# LANGUAGE DeriveDataTypeable #-} + +{-| + +This module implements the trusted compoenet of DCLabel privileges, +documented in "DCLabel.Privs". +Since privilege objects may be used unsafely, this module is marked +@-XUnsafe@. Untrusted code may access privileges using the interface +provided by "DCLabel.Privs". + +-} + +module DCLabel.Privs.TCB ( + -- * Privileges + DCPrivDesc + , DCPriv(..), dcPrivTCB + , noPriv, allPrivTCB + ) where + +import Data.Monoid +import Data.Typeable +import DCLabel.Core + +-- | A privilege description is simply a conjunction of disjunctions. +-- Unlike (actually minted) privileges (see 'DCPriv'), privilege +-- descriptions may be created by untrusted code. +type DCPrivDesc = Component + +-- | A privilege is a minted and protected privilege description +-- ('DCPrivDesc') that may only be created by trusted code or +-- delegated from an existing @DCPriv@. +newtype DCPriv = DCPrivTCB { unDCPriv :: DCPrivDesc } + deriving (Eq, Show, Typeable) + +-- | Privileges can be combined using 'mappend' +instance Monoid DCPriv where + mempty = noPriv + mappend p1 p2 = DCPrivTCB . dcReduce $! (unDCPriv p1) `dcAnd` (unDCPriv p2) + +-- | The empty privilege, or no privileges, corresponds to logical +-- @True@. +noPriv :: DCPriv +noPriv = DCPrivTCB dcTrue + +-- | The all privilege corresponds to logical @False@ +allPrivTCB :: DCPriv +allPrivTCB = dcPrivTCB dcFalse + +-- | Create a new privilege given a description. +dcPrivTCB :: DCPrivDesc -> DCPriv +dcPrivTCB = DCPrivTCB diff --git a/DCLabel/Safe.hs b/DCLabel/Safe.hs deleted file mode 100644 --- a/DCLabel/Safe.hs +++ /dev/null @@ -1,37 +0,0 @@ -{-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) -{-# LANGUAGE Trustworthy #-} -#endif -{-| -This module exports a safe-subset of "DCLabel.Core", -implementing Disjunction Category Components. -The exported functions and constructors may be used by -untrusted code, guaranteeing that they cannot perform -anything unsafe. --} - - -module DCLabel.Safe ( -- * DC Components with EDSL - join, meet, top, bottom, canflowto - , Component(..), DCLabel(..), Disj(..), Conj(..) - , Principal, principal, name, singleton - , listToDisj, disjToList - , listToComponent, componentToList - , (.\/.), (./\.) - , (<>), (><) - , newDC - -- * Privilegies - , TCBPriv, priv, Priv - , canflowto_p - , delegatePriv - , canDelegate, owns - , newPriv, NewPriv, newTCBPriv, noPriv - ) where - -import DCLabel.Core - -#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) -import safe DCLabel.NanoEDSL -#else -import DCLabel.NanoEDSL -#endif diff --git a/DCLabel/Secrecy.hs b/DCLabel/Secrecy.hs deleted file mode 100644 --- a/DCLabel/Secrecy.hs +++ /dev/null @@ -1,31 +0,0 @@ -{-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) -{-# LANGUAGE Trustworthy #-} -#endif -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} --- | This module implements secrecy-only DC Labels. -module DCLabel.Secrecy ( SLabel(..) ) where - -import DCLabel.Core - --- | A secrecy-only DC label. -newtype SLabel = MkSLabel DCLabel - deriving (Eq, Show, Read) - -instance ToLNF SLabel where - toLNF (MkSLabel l) = MkSLabel (toLNF l) - -instance Lattice SLabel where - bottom = MkSLabel bottom - top = MkSLabel top - join (MkSLabel l1) (MkSLabel l2) = MkSLabel $ - join l1 { integrity = emptyComponent } l2 { integrity = emptyComponent } - meet (MkSLabel l1) (MkSLabel l2) = MkSLabel $ - meet l1 { integrity = emptyComponent } l2 { integrity = emptyComponent } - canflowto (MkSLabel l1) (MkSLabel l2) = - canflowto l1 { integrity = emptyComponent } l2 { integrity = emptyComponent } - -instance RelaxedLattice SLabel where - canflowto_p p (MkSLabel l1) (MkSLabel l2) = - canflowto_p p l1 { integrity = emptyComponent } l2 { integrity = emptyComponent } diff --git a/DCLabel/Serialize.hs b/DCLabel/Serialize.hs new file mode 100644 --- /dev/null +++ b/DCLabel/Serialize.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 704) +{-# LANGUAGE Trustworthy #-} +#endif +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +{- | This module provides instances for binary serialization of +'DCLabel's. Specifically, we provide insgtances for @cereal@\'s +@Data.Serialize@. -} + +module DCLabel.Serialize () where + + +import DCLabel.Core +import Data.Serialize +import Control.Monad + +deriving instance Serialize Principal +deriving instance Serialize Clause + +-- | Serialize components by converting them to maybe's +instance Serialize Component where + put c = put . dcToMaybe $! c + where dcToMaybe DCFalse = Nothing + dcToMaybe (DCFormula f) = Just f + get = dcFromMaybe `liftM` get + where dcFromMaybe Nothing = dcFalse + dcFromMaybe (Just f) = dcFormula f + +-- | Serialize labels by converting them to pairs of components. +instance Serialize DCLabel where + put l = put (dcSecrecy l, dcIntegrity l) + get = uncurry dcLabelNoReduce `liftM` get diff --git a/DCLabel/TCB.hs b/DCLabel/TCB.hs deleted file mode 100644 --- a/DCLabel/TCB.hs +++ /dev/null @@ -1,16 +0,0 @@ -{-| -This module exports an unsafe-subset of "DCLabel.Core", -implementing Disjunction Category Labels. -A subset of the exported functions and constructors -shoul not be exposed to untrusted code; instead, -untursted code should import the "DCLabel.Safe" -module. --} - - -module DCLabel.TCB ( module DCLabel.Core - , module DCLabel.NanoEDSL - ) where - -import DCLabel.Core -import DCLabel.NanoEDSL diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,5 @@ -Copyright (c) 2011 Deian Stefan, Alejandro Russo, John C. Mitchell, David Mazieres +Copyright (c) 2011 Deian Stefan, Alejandro Russo, John C. Mitchell, +David Mazieres, Amit Levy Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are diff --git a/dclabel.cabal b/dclabel.cabal --- a/dclabel.cabal +++ b/dclabel.cabal @@ -1,34 +1,29 @@ Name: dclabel -Version: 0.0.6 +Version: 0.9.0.0 build-type: Simple License: BSD3 License-File: LICENSE -Copyright: (c) 2011 Deian Stefan, Alejandro Russo, John C. Mitchell, David Mazieres -Author: Deian Stefan, Alejandro Russo -Maintainer: Deian Stefan +Copyright: (c) 2012 Hails team +Author: Hails Team +Maintainer: Hails Team Stability: experimental -Synopsis: The Disjunction Category Label Format +Synopsis: This packge is deprecated. See the the "LIO.DCLabel" in the "lio" package. Category: Security Cabal-Version: >=1.8 Extra-source-files: - examples/ExamplesDCLabels.hs - examples/Labels.hs - examples/ListExamples.hs - examples/UsingEDSL.hs - tests/Tests.hs + test_and_bench/test.hs + test_and_bench/Instances.hs + test_and_bench/bench.hs Description: - The /DC Label/ (DCLabel) library provides dynamic information - flow control label format in the form of conjunctions of - disjunctions of principals. Most code should import module - "DCLabel.Safe"; trusted code should import "DCLabel.TCB". - The core functionality of the library is documented in - "DCLabel.Core", while the small EDSL used to create labels is - documents in "DCLabel.NanoEDSL". DCLabel was implemented by David - Mazieres (), Deian Stefan - (), and Alejandro Russo - (). + The /DC Label/ (DCLabel) library provides an information flow + control label format in the form of conjunctions of + disjunctions of principals. Most code should import module + "DCLabel"; trusted code may additionally import + "DCLabel.Privs.TCB". The core functionality of the library is + documented in "DCLabel.Core", while the small EDSL used to + create labels is documents in "DCLabel.NanoEDSL". Source-repository head Type: git @@ -37,34 +32,53 @@ Library Build-depends: base >= 4 && < 5, - bytestring > 0.9.2 && < 2, - cereal >= 0.3.3 && < 0.4, - pretty > 1.0.1 && < 2 + bytestring >= 0.9.2 && < 1.0, + containers >= 0.3 && < 1.0, + cereal >= 0.3.3 && < 0.4 ghc-options: -Wall -fno-warn-orphans Exposed-modules: - DCLabel.Safe, - DCLabel.TCB, - DCLabel.Core, - DCLabel.NanoEDSL, - DCLabel.PrettyShow, - DCLabel.Secrecy, - DCLabel.Integrity + DCLabel + DCLabel.Core + DCLabel.Privs + DCLabel.Privs.TCB + DCLabel.Serialize + DCLabel.DSL test-suite tests type: exitcode-stdio-1.0 - hs-source-dirs: tests - main-is: Tests.hs + hs-source-dirs: test_and_bench + main-is: test.hs ghc-options: - -Wall -threaded -rtsopts + -threaded -rtsopts build-depends: QuickCheck, + quickcheck-instances, test-framework, test-framework-quickcheck2, base, + containers, + dclabel, + bytestring, + cereal + +benchmark benchmarks + type: exitcode-stdio-1.0 + hs-source-dirs: test_and_bench + main-is: bench.hs + + ghc-options: + -O2 -threaded -rtsopts + + build-depends: + base, + QuickCheck, + quickcheck-instances, + containers, + criterion, dclabel, bytestring, cereal diff --git a/examples/ExamplesDCLabels.hs b/examples/ExamplesDCLabels.hs deleted file mode 100644 --- a/examples/ExamplesDCLabels.hs +++ /dev/null @@ -1,27 +0,0 @@ -{-# LANGUAGE Trustworthy #-} -module ExamplesDCLabels where - -import DCLabel.TCB -import DCLabel.PrettyShow - -l1 = "Alice" .\/. "Bob" ./\. "Carla" - -l2 = "Alice" ./\. "Carla" - -dc1 = newDC l1 l2 - -dc2 = newDC ("Deian") ("Alice") - -pr = createPrivTCB (newPriv ("Alice" ./\. "Carla")) - -main = do - putStrLn . prettyShow $ dc1 - putStrLn . prettyShow $ dc2 - putStrLn . show $ canflowto dc1 dc2 - putStrLn . show $ canflowto_p pr dc1 dc2 -{- -<{["Alice" \/ "Bob"] /\ ["Carla"]} , {["Alice"] /\ ["Carla"]}> -<{["Deian"]} , {["Alice"]}> -False -True --} diff --git a/examples/Labels.hs b/examples/Labels.hs deleted file mode 100644 --- a/examples/Labels.hs +++ /dev/null @@ -1,46 +0,0 @@ -{-# LANGUAGE Safe #-} -module Labels where - -import DCLabel.Safe -import DCLabel.PrettyShow - --- Creating categories -c1 = "Alice" - -c2 = "Alice" .\/. "Bob" - -c3 = (<>) - --- Labels, i.e. conjunctions of disjunctions --- Observe the precedence of .\/. is higher than ./\. - -l1 = "Alice" .\/. "Bob" ./\. "Carla" - -l2 = "Alice" ./\. "Carla" - --- DCLabels - -dc1 = newDC l1 l2 - -dc2 = newDC ("Deian") ("Alice") - -main = do - putStrLn . prettyShow $ dc1 - putStrLn . prettyShow $ dc2 - putStrLn . prettyShow $ join dc1 dc2 - putStrLn . prettyShow $ meet dc1 dc2 - - putStrLn . prettyShow $ dc1 - putStrLn . prettyShow $ join dc1 top - putStrLn . show $ canflowto dc1 top - putStrLn . show $ canflowto bottom dc1 -{- -<{["Alice" \/ "Bob"] /\ ["Carla"]} , {["Alice"] /\ ["Carla"]}> -<{["Deain"]} , {["Alice"]}> -<{["Alice" \/ "Bob"] /\ ["Carla"] /\ ["Deain"]} , {["Alice"]}> -<{["Alice" \/ "Bob" \/ "Deain"] /\ ["Carla" \/ "Deain"]} , {["Alice"] /\ ["Carla"]}> -<{["Alice" \/ "Bob"] /\ ["Carla"]} , {["Alice"] /\ ["Carla"]}> -<{ALL} , {}> -True -True --} diff --git a/examples/ListExamples.hs b/examples/ListExamples.hs deleted file mode 100644 --- a/examples/ListExamples.hs +++ /dev/null @@ -1,45 +0,0 @@ -{-# LANGUAGE Safe #-} -module ListExamples where - -import DCLabel.Safe -import DCLabel.PrettyShow - -c1 = listToDisj [principal "Alice"] - -c2 = listToDisj ["Alice", "Bob"] - -c3 = (<>) - --- Labels, i.e. conjunctions of disjunctions --- Observe the precedence of .\/. is higher than ./\. - -l1 = c2 ./\. "Carla" - -l2 = "Alice" ./\. "Carla" - --- DCLabels - -dc1 = newDC l1 l2 - -dc2 = newDC ("Deian") ("Alice") - -main = do - putStrLn . prettyShow $ dc1 - putStrLn . prettyShow $ dc2 - putStrLn . prettyShow $ join dc1 dc2 - putStrLn . prettyShow $ meet dc1 dc2 - - putStrLn . prettyShow $ dc1 - putStrLn . prettyShow $ join dc1 top - putStrLn . show $ canflowto dc1 top - putStrLn . show $ canflowto bottom dc1 -{- -<{["Alice" \/ "Bob"] /\ ["Carla"]} , {["Alice"] /\ ["Carla"]}> -<{["Deain"]} , {["Alice"]}> -<{["Alice" \/ "Bob"] /\ ["Carla"] /\ ["Deain"]} , {["Alice"]}> -<{["Alice" \/ "Bob" \/ "Deain"] /\ ["Carla" \/ "Deain"]} , {["Alice"] /\ ["Carla"]}> -<{["Alice" \/ "Bob"] /\ ["Carla"]} , {["Alice"] /\ ["Carla"]}> -<{ALL} , {}> -True -True --} diff --git a/examples/UsingEDSL.hs b/examples/UsingEDSL.hs deleted file mode 100644 --- a/examples/UsingEDSL.hs +++ /dev/null @@ -1,34 +0,0 @@ -{-# LANGUAGE Safe #-} -module UsingEDSL where - -import DCLabel.Safe -import DCLabel.PrettyShow - --- Creating categories: -c1 = "Alice" - -c2 = "Alice" .\/. "Bob" - -c3 = (<>) - --- Labels, i.e. conjunctions of disjunctions --- Observe the precedence of .\/. is higher than ./\. - -l1 = "Alice" .\/. "Bob" ./\. "Carla" -l2 = "Alice" ./\. "Carla" -l3 = "Alice" .\/. ("Bob" ./\. "Carla") - --- DCLabels - -dc1 = newDC l1 l2 -dc2 = newDC ("Deian") ("Alice") -dc3 = newDC l3 (<>) -dc4 = newDC c3 (><) - - -main = do - putStrLn $ prettyShow dc1 - putStrLn $ prettyShow dc2 - putStrLn $ prettyShow dc3 - putStrLn $ prettyShow dc4 - diff --git a/test_and_bench/Instances.hs b/test_and_bench/Instances.hs new file mode 100644 --- /dev/null +++ b/test_and_bench/Instances.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE OverloadedStrings #-} + +-- | Instances for "QuicCheck"\'s 'Arbitrary' class. +module Instances () where + +import Control.Monad (liftM) +import Test.QuickCheck +import Test.QuickCheck.Instances +import DCLabel.Core +import DCLabel.Privs.TCB +import Data.Set hiding (map) +import qualified Data.ByteString.Char8 as S8 + +instance Arbitrary Principal where + arbitrary = oneof $ map (\x -> return . Principal . S8.singleton $ x) ['A'..'Z'] + +instance Arbitrary Clause where + arbitrary = Clause `liftM` arbitrary + +instance Arbitrary Component where + arbitrary = oneof [ return DCFalse + , do cs <- arbitrary + return . DCFormula $ if (Clause empty) `member` cs + then empty + else cs + ] + +instance Arbitrary DCLabel where + arbitrary = do + s <- dcReduce `liftM` arbitrary + i <- dcReduce `liftM` arbitrary + return (dcLabel s i) + +instance Arbitrary DCPriv where + arbitrary = DCPrivTCB `liftM` arbitrary diff --git a/test_and_bench/bench.hs b/test_and_bench/bench.hs new file mode 100644 --- /dev/null +++ b/test_and_bench/bench.hs @@ -0,0 +1,27 @@ + +module Main (main) where + +import DCLabel +import Instances +import Test.QuickCheck +import Criterion.Main + +main = do + b0 <- mkCanFlowTo + b1 <- mkCanFlowToP + defaultMain $ b0 ++ b1 + +mkCanFlowTo = do + xs <- sample' (arbitrary :: Gen DCLabel) + ys <- sample' (arbitrary :: Gen DCLabel) + let zs = zipWith (\x y -> whnf (canFlowTo x) y) xs ys + bs = zipWith (\n b -> bench ("canFlowTo " ++ show n) b) [1..] zs + return bs + +mkCanFlowToP = do + xs <- sample' (arbitrary :: Gen DCLabel) + ys <- sample' (arbitrary :: Gen DCLabel) + ps <- sample' (arbitrary :: Gen DCPriv) + let zs = zipWith3 (\p x y -> whnf (canFlowToP p x) y) ps xs ys + bs = zipWith (\n b -> bench ("canFlowToP " ++ show n) b) [1..] zs + return bs diff --git a/test_and_bench/test.hs b/test_and_bench/test.hs new file mode 100644 --- /dev/null +++ b/test_and_bench/test.hs @@ -0,0 +1,108 @@ +{-# LANGUAGE OverloadedStrings #-} +module Main (main) where + +import Test.Framework (Test, defaultMain) +import Test.Framework.Providers.QuickCheck2 (testProperty) +import Test.QuickCheck +import Test.QuickCheck.Instances +import DCLabel +import DCLabel.Core +import Data.Monoid +import Data.Set hiding (map) +import Data.Serialize + +import Instances + + +-- Reduction function toLNF does not modify the semantics of the label +prop_dcReduce :: Component -> Bool +prop_dcReduce l = let l' = dcReduce l + in l `dcImplies` l' && l' `dcImplies` l + +-- Idempotenncy of dcReduce +prop_dcReduce_idem :: Property +prop_dcReduce_idem = forAll (arbitrary :: Gen Component) $ \l-> + let l' = dcReduce l + l'' = dcReduce l' + in l' == l'' + + +-- Partial order for DCLabels +prop_dc_porder :: DCLabel -> DCLabel -> Bool +prop_dc_porder l1 l2 = let ge = l1 `canFlowTo` l2 + le = l2 `canFlowTo` l1 + eq = l2 == l1 + in (eq && ge && le) || -- == + ((not eq) && (ge || le) && (ge /= le)) || -- < or > + (not (eq || ge || le)) -- incomparable + +-- L_1 CanFlowTo L_2 ==> L_1 `CanFlowToP p` L_2 for andy p +prop_dc_canFlowToP :: DCLabel -> DCLabel -> Property +prop_dc_canFlowToP l1 l2 = forAll (arbitrary :: Gen DCPriv) $ \p -> + l1 `canFlowTo` l2 ==> canFlowToP p l1 l2 + +-- L_1 CanFlowTo_P1 L_2 ==> L_1 `CanFlowToP (P1 /\ P2)` L_2 for andy P2 +prop_dc_mappendPrivs :: DCLabel -> DCLabel -> DCPriv -> Property +prop_dc_mappendPrivs l1 l2 p1 = forAll (arbitrary :: Gen DCPriv) $ \p2 -> + canFlowToP p1 l1 l2 ==> canFlowToP (p1 `mappend` p2) l1 l2 + +-- Check that labels flow to their join for DCLabels +prop_dc_join :: DCLabel -> DCLabel -> Bool +prop_dc_join l1 l2 = let l3 = l1 `dcJoin` l2 + t1 = l1 `canFlowTo` l3 + t2 = l2 `canFlowTo` l3 + in t1 && t2 + +-- Check that join is the least upper bound for DCLabels +prop_dc_join_lub :: DCLabel -> DCLabel -> Property +prop_dc_join_lub l1 l2 = forAll (arbitrary :: Gen DCLabel) $ \l3' -> + (l1 `canFlowTo` l3') && (l2 `canFlowTo` l3') ==> (l1 `dcJoin` l2) `canFlowTo` l3' + + +-- Check that meet flows to the labels making it, for DCLabels +prop_dc_meet :: DCLabel -> DCLabel -> Bool +prop_dc_meet l1 l2 = let l3 = l1 `dcMeet` l2 + t1 = l3 `canFlowTo` l1 + t2 = l3 `canFlowTo` l2 + in t1 && t2 + +-- Check that meet the greatest lower bound for DCLabels +prop_dc_meet_glb :: DCLabel -> DCLabel -> Property +prop_dc_meet_glb l1 l2 = forAll (arbitrary :: Gen DCLabel) $ \l3' -> + (l3' `canFlowTo` l1) && (l3' `canFlowTo` l2) ==> l3' `canFlowTo` (l1 `dcMeet` l2) + +-- Check that the top is indeed indeed the highest element in the lattice +prop_dc_top :: DCLabel -> Property +prop_dc_top l1 = forAll (gen l1) $ \l -> l `canFlowTo` dcTop + where gen :: DCLabel -> Gen DCLabel + gen _ = arbitrary + +-- Check that the bottom is indeed indeed the lowest element in the lattice +prop_dc_bottom :: DCLabel -> Property +prop_dc_bottom _ = forAll (arbitrary :: Gen DCLabel) $ \l -> dcBot `canFlowTo` l + +-- | Test serialization. +prop_dc_serialize :: DCLabel -> Bool +prop_dc_serialize l = case decode (encode l) of + Left _ -> False + Right l' -> l == l' + +main :: IO () +main = defaultMain tests +-- +tests :: [Test] +tests = [ + testProperty "dcReduce" prop_dcReduce + , testProperty "Idempotence of function dcReduce" prop_dcReduce_idem + , testProperty "Property of top" prop_dc_top + , testProperty "Property of bottom" prop_dc_bottom + , testProperty "Join operation" prop_dc_join + , testProperty "Join operation is the least upper bound" prop_dc_join_lub + , testProperty "Meet operation" prop_dc_meet + , testProperty "Meet operation is the greatest lower bound" prop_dc_meet_glb + , testProperty "DC labels form a partial order" prop_dc_porder + , testProperty "Flow check with privs is less restricting" prop_dc_canFlowToP + , testProperty "Combined privileges are stronger" prop_dc_mappendPrivs + , testProperty "Serialization of DC labels" prop_dc_serialize + ] + diff --git a/tests/Tests.hs b/tests/Tests.hs deleted file mode 100644 --- a/tests/Tests.hs +++ /dev/null @@ -1,195 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} -module Main (main) where - -import Test.Framework (Test, defaultMain) -import Test.Framework.Providers.QuickCheck2 (testProperty) -import Test.QuickCheck -import Control.Monad (liftM) -import DCLabel.TCB -import DCLabel.Secrecy -import DCLabel.Integrity -import Data.List (tails) -import Data.Serialize - -instance Arbitrary Principal where - arbitrary = do p <- oneof $ map return ["A", "B", "C"] - return $ principal p - - -instance Arbitrary Disj where - arbitrary = sized disjunction - where disjunction 0 = return $ MkDisj { disj = [] } - disjunction n = do a <- arbitrary - m <- choose (0, n-1) - djs <- disjunction m - return $ MkDisj $ a:(disj djs) - - -instance Arbitrary Conj where - arbitrary = sized conjunction - where conjunction 0 = oneof [return $ MkConj { conj = [] } , - return $ MkConj { conj = [MkDisj []] }, - return $ MkConj { conj = [MkDisj [], MkDisj []] } ] - conjunction n = do a <- arbitrary - m <- choose (0, n-1) - cjs <- conjunction m - return $ MkConj $ a:(conj cjs) - shrink (MkConj ls) = [MkConj ll | l <- tails ls, ll <- shrink l] - -instance Arbitrary Component where - arbitrary = do m <- choose (0, 1) :: Gen Int - if m==0 then mkArbLbl arbitrary - else return MkComponentAll - where mkArbLbl :: Gen Conj -> Gen Component - mkArbLbl = liftM MkComponent - -instance Arbitrary (SLabel) where - arbitrary = do s <- arbitrary - return $ MkSLabel s - -instance Arbitrary (ILabel) where - arbitrary = do s <- arbitrary - return $ MkILabel s - -instance Arbitrary DCLabel where - arbitrary = do s <- arbitrary - i <- arbitrary - return $ MkDCLabel { secrecy = s, integrity = i } - -instance Arbitrary TCBPriv where - arbitrary = do p <- arbitrary - return $ MkTCBPriv p - --- cleanComponent does not modify the semantics of the label -prop_cleanComponent :: Component -> Bool -prop_cleanComponent l = let l' = cleanComponent l - in l `implies` l' && l' `implies` l - --- Reduction function toLNF does not modify the semantics of the label -prop_toLNF :: Component -> Bool -prop_toLNF l = let l' = toLNF l - in l `implies` l' && l' `implies` l - --- Idempotenncy of toLNF -prop_toLNF_idem :: Property -prop_toLNF_idem = forAll (arbitrary :: Gen Component) $ \l-> - let l' = toLNF l - l'' = toLNF l' - in l' == l'' - --- Partial order for DCLabels -prop_dc_porder :: (DCLabel, DCLabel) -> Bool -prop_dc_porder (l1,l2) = let l1' = toLNF l1 - l2' = toLNF l2 - ge = l1' `canflowto` l2' - le = l2' `canflowto` l1' - eq = l2' == l1' - in (eq && ge && le) || -- == - ((not eq) && (ge || le) && (ge /= le)) || -- < or > - (not (eq || ge || le)) -- incomparable - --- Check that labels flow to their join for DCLabels -prop_DC_join :: (DCLabel, DCLabel) -> Bool -prop_DC_join (l1,l2) = let l3 = l1 `join` l2 - t1 = l1 `canflowto` l3 - t2 = l2 `canflowto` l3 - in t1 && t2 - --- Check that join is the least upper bound for DCLabels --- TODO: we need to fix this since it is difficult to satisfy the --- hypothesis. -prop_dc_join_lub :: (DCLabel, DCLabel) -> Property -prop_dc_join_lub (l1,l2) = forAll (arbitrary :: Gen DCLabel) $ \l3' -> - (l1 `canflowto` l3') && (l2 `canflowto` l3') ==> (l1 `join` l2) `canflowto` l3' - - --- Check that meet flows to the labels making it, for DCLabels -prop_dc_meet :: (DCLabel, DCLabel) -> Bool -prop_dc_meet (l1,l2) = let l3 = l1 `meet` l2 - t1 = l3 `canflowto` l1 - t2 = l3 `canflowto` l2 - in t1 && t2 - --- Check that meet the greatest lower bound for DCLabels -prop_dc_meet_glb :: (DCLabel, DCLabel) -> Property -prop_dc_meet_glb (l1,l2) = forAll (arbitrary :: Gen DCLabel) $ \l3' -> - (l3' `canflowto` l1) && (l3' `canflowto` l2) ==> l3' `canflowto` (l1 `meet` l2) - --- Check that the top is indeed indeed the highest element in the lattice -prop_dc_top :: DCLabel -> Property -prop_dc_top l1 = forAll (gen l1) $ \l -> l `canflowto` top - where gen :: DCLabel -> Gen DCLabel - gen _ = arbitrary - --- Check that the bottom is indeed indeed the lowest element in the lattice -prop_dc_bottom :: DCLabel -> Property -prop_dc_bottom _ = forAll (arbitrary :: Gen DCLabel) $ \l -> bottom `canflowto` l - --- LIO's lostar -lostar :: TCBPriv -> DCLabel -> DCLabel -> DCLabel -lostar p l g = - let (ls, li) = (toLNF . secrecy $ l, toLNF . integrity $ l) - (gs, gi) = (toLNF . secrecy $ g, toLNF . integrity $ g) - lp = toLNF $ priv p - rs' = c2l [c | c <- getCats ls - , not (lp `implies` (c2l [c]))] - rs'' = c2l [c | c <- getCats gs - , not (rs' `implies` (c2l [c]))] - rs = if ls == allComponent || gs == allComponent - then allComponent - else rs' `and_component` rs'' - ri = (li `and_component` lp) `or_component` gi - in toLNF $ simpleNewComponent p (newDC rs ri) - where getCats = conj . component - c2l = MkComponent . MkConj - simpleNewComponent pr lr | pr == rootPrivTCB = g - | pr == noPriv = l `join` g - | otherwise = lr - -{- -lr = lostar p li lg satisfies: - - canflowto lg lr - - canflowto_p p li lr - - lr is the greatest lower bound --} -prop_lostar :: TCBPriv -> DCLabel -> DCLabel -> Property -prop_lostar p li lg = - let lr = lostar p li lg - in forAll (arbitrary :: Gen DCLabel) $ \lr' -> - canflowto lg lr && - canflowto_p p li lr && - not ( canflowto lg lr' && - canflowto_p p li lr' && - lr' /= lr && - canflowto lr' lr) - --- | Test serialization. -prop_DC_serialize :: DCLabel -> Bool -prop_DC_serialize l = case decode (encode l) of - Left _ -> False - Right l' -> l == l' - -main :: IO () -main = defaultMain tests - -tests :: [Test] -tests = [ - testProperty "cleanComponent" (prop_cleanComponent :: Component -> Bool) - , testProperty "toLNF" (prop_toLNF :: Component -> Bool) - , testProperty "Idempotence of function toLNF" (prop_toLNF_idem :: Property) - , testProperty "Property of top" (prop_dc_top :: DCLabel -> Property) - , testProperty "Property of bottom" (prop_dc_bottom :: DCLabel -> Property) - , testProperty "Join operation" (prop_DC_join :: (DCLabel, DCLabel) -> Bool) - , testProperty "Join operation is the least upper bound" - (prop_dc_join_lub :: (DCLabel, DCLabel) -> Property) - , testProperty "Meet operation" (prop_dc_meet :: (DCLabel, DCLabel) -> Bool) - , testProperty "Meet operation is the greatest lower bound" - (prop_dc_meet_glb :: (DCLabel, DCLabel) -> Property) - , testProperty "DC labels form a partial order" - (prop_dc_porder :: (DCLabel, DCLabel) -> Bool) - , testProperty "lostar implementation" - (prop_lostar :: TCBPriv -> DCLabel -> DCLabel -> Property) - , testProperty "Serialization of DC labels" - (prop_DC_serialize :: DCLabel -> Bool) - ]