diff --git a/DCLabel/Core.hs b/DCLabel/Core.hs --- a/DCLabel/Core.hs +++ b/DCLabel/Core.hs @@ -1,19 +1,29 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +{-# LANGUAGE SafeImports #-} +#endif {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-| -This module implements Disjunction Category labels. +This module implements Disjunction Category Labels. -A DCLabel is a pair of 'secrecy' and 'integrity' category sets (of type -'Label'). A category set (of type 'Conj') is a conjunction of categories -(of type 'Disj'). Each category, in turn, is a disjunction of 'Principal's, -where a 'Principal' is just a 'String' whose meaning is up to the application. +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. -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 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. 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 @@ -52,13 +62,13 @@ -} -module DCLabel.Core ( -- * Labels +module DCLabel.Core ( -- * Components -- $labels - Disj(..), Conj(..), Label(..) - , emptyLabel, allLabel + Disj(..), Conj(..), Component(..) + , emptyComponent, allComponent , Lattice(..) , ToLNF(..) - -- ** DC Labels + -- ** DC Components , DCLabel(..) -- * Principals , Principal(..), principal @@ -69,17 +79,29 @@ , noPriv, rootPrivTCB , delegatePriv, createPrivTCB , CanDelegate(..), Owns(..) - -- * Label/internal operations - , and_label, or_label, cleanLabel, implies + -- * Component/internal operations + , and_component, or_component, cleanComponent, implies , DisjToFromList(..) - , listToLabel, labelToList + , listToComponent, componentToList ) where +#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 qualified Data.ByteString as B +import qualified Data.ByteString.Char8 as C +import Data.Serialize + -- -- Categories -- @@ -94,22 +116,24 @@ -- | 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) -- --- Labels +-- Components -- {- $labels -A label is a conjunction of disjunctions of principals. A 'DCLabel' is simply a -pair of such labels. 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. + 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 forma a partial order according to the ⊑ relation. +-- | 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 @@ -126,46 +150,48 @@ 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 } +-- | 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) --- | Labels have a unique LNF (see 'ToLNF') form, and equality testing is +-- | Components have a unique LNF (see 'ToLNF') form, and equality testing is -- perfomed on labels of this form. -instance Eq Label where - (==) MkLabelAll MkLabelAll = True - (==) MkLabelAll _ = False - (==) _ MkLabelAll = False - (==) l1 l2 = (label . toLNF $ l1) == (label . toLNF $ l2) +instance Eq Component where + (==) MkComponentAll MkComponentAll = True + (==) MkComponentAll _ = False + (==) _ MkComponentAll = False + (==) l1 l2 = (component . toLNF $ l1) == (component . toLNF $ l2) --- | A label without any disjunctions or conjunctions. This label, conceptually --- corresponds to the label consisting of a single category containing all --- principals. Conceptually, --- @emptyLabel = \<{[P_1 ⋁ P_2 ⋁ ...]}\>@ -emptyLabel :: Label -emptyLabel = MkLabel (MkConj []) +-- | 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 []) --- | The dual of 'emptyLabel', 'allLabel' consists of the conjunction of +-- | 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, --- @allLabel = \<{[P_1] ⋀ [P_2] ⋀ ...}\>@ -allLabel :: Label -allLabel = MkLabelAll +-- 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 -- | 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) ] +-- the 'emptyComponent'. +isEmptyComponent :: Component -> Bool +isEmptyComponent MkComponentAll = False +isEmptyComponent l = and [ null (disj d) | d <- conj (component l) ] -- | Predicate function that retuns @True@ if the label corresponds to --- the 'allLabel'. -isAllLabel :: Label -> Bool -isAllLabel MkLabelAll = True -isAllLabel _ = False +-- the 'allComponent'. +isAllComponent :: Component -> Bool +isAllComponent MkComponentAll = True +isAllComponent _ = False -- @@ -173,90 +199,94 @@ -- --- | 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 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)} --- | 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] +-- | 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] --- | Determines if a conjunction of disjunctions, i.e., a label, implies +-- | 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, 'allLabel' \``impliesDisj`\` X = True +-- * ∀ X, 'allComponent' \``impliesDisj`\` X = True -- --- * ∀ X, X \``impliesDisj`\` 'emptyLabel' = True +-- * ∀ X, X \``impliesDisj`\` 'emptyComponent' = True -- --- * ∀ X≠'emptyLabel', 'emptyLabel' \``impliesDisj`\` X = False +-- * ∀ X≠'emptyComponent', 'emptyComponent' \``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 +-- for safety; the function is always called with a non-ALL component and -- non-null disjunction. -impliesDisj :: Label -> Disj -> Bool -impliesDisj l d | isAllLabel l = True -- Asserts 1 +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 (label l) - , not (isEmptyLabel l) ] -- Asserts 3 + | d1 <- conj (component l) + , not (isEmptyComponent l) ] -- Asserts 3 --- | Determines if a label implies (in the logical sense) another label. +-- | Determines if a component logically implies another component. -- In other words, d_1 ⋀ ... ⋀ d_n => d_1' ⋀ ... ⋀ d_n'. -- -- Properties: -- --- * ∀ X, 'allLabel' \``implies`\` X := True +-- * ∀ X, 'allComponent' \``implies`\` X := True -- --- * ∀ X≠'allLabel', X \``implies`\` 'allLabel' := False +-- * ∀ X≠'allComponent', X \``implies`\` 'allComponent' := False -- --- * ∀ X, X \``implies`\` 'emptyLabel' := True +-- * ∀ X, X \``implies`\` 'emptyComponent' := True -- --- * ∀ X≠'emptyLabel', 'emptyLabel' \``implies`\` X := False -implies :: Label -> Label -> Bool -implies l1 l2 | isAllLabel l1 = True -- Asserts 1 - | isAllLabel l2 = False -- Asserts 2 +-- * ∀ 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 . label . toLNF $ l2 ] + | d <- conj . component . 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 a 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 'Label', 'DCLabel', etc. +-- 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 ] + +-- | 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 --- | 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 +-- | 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 ((MkLabel . MkConj) [d1]) d2 ] + , impliesDisj ((MkComponent . MkConj) [d1]) d2 ] -- -- DC Labels @@ -268,9 +298,9 @@ -- -- | A @DCLabel@ is a pair of secrecy and integrity category sets, i.e., --- a pair of 'Label's. -data DCLabel = MkDCLabel { secrecy :: Label -- ^ Integrity category set. - , integrity :: Label -- ^ Secrecy category set. +-- a pair of 'Component's. +data DCLabel = MkDCLabel { secrecy :: Component -- ^ Integrity category set. + , integrity :: Component -- ^ Secrecy category set. } deriving (Eq, Show, Read) @@ -282,9 +312,9 @@ -- | Elements of 'DCLabel' form a bounded lattice, where: -- --- * @⊥ = \<'emptyLabel', 'allLabel'\>@ +-- * @⊥ = \<'emptyComponent', 'allComponent'\>@ -- --- * @⊤ = \<'allLabel', 'emptyLabel'\>@ +-- * @⊤ = \<'allComponent', 'emptyComponent'\>@ -- -- * @ \ ⊔ \ = \@ -- @@ -292,16 +322,16 @@ -- -- * @ \ ⊑ \ = S_2 => S_1 ⋀ I_1 => I_2@ instance Lattice DCLabel where - bottom = MkDCLabel { secrecy = emptyLabel - , integrity = allLabel } - top = MkDCLabel { secrecy = allLabel - , integrity = emptyLabel } - join l1 l2 = let s3 = (secrecy l1) `and_label` (secrecy l2) - i3 = (integrity l1) `or_label` (integrity l2) + 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_label` (secrecy l2) - i3 = (integrity l1) `and_label` (integrity l2) + 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 @@ -316,14 +346,15 @@ -- | 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 labels or be ignoerd a corresponding --- privilege ('TCBPriv') must be created (by trusted code) or delegated. -newtype Principal = MkPrincipal { name :: String } +-- 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) -- | Generates a principal from an string. -principal :: String -> Principal -principal = MkPrincipal +principal :: B.ByteString -> Principal +principal = MkPrincipal -- @@ -334,9 +365,9 @@ 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 'Label' 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 +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 @@ -354,15 +385,15 @@ category using the 'owns' function. -} --- | Privilege object is just a conjunction of disjunctions, i.e., a 'Label'. +-- | 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 :: Label } +data TCBPriv = MkTCBPriv { priv :: Component } deriving (Eq, Show) -- | Untrusted privileged object, which can be converted to a 'TCBPriv' with -- 'delegatePriv'. -type Priv = Label +type Priv = Component -- | Class extending 'Lattice', by allowing for the more relaxed label -- comparison @canflowto_p@. @@ -374,8 +405,8 @@ instance RelaxedLattice DCLabel where canflowto_p p l1 l2 = let l1' = MkDCLabel { secrecy = (secrecy l1) - , integrity = (and_label (priv p) (integrity l1)) } - l2' = MkDCLabel { secrecy = (and_label (priv p) (secrecy l2)) + , integrity = (and_component (priv p) (integrity l1)) } + l2' = MkDCLabel { secrecy = (and_component (priv p) (secrecy l2)) , integrity = (integrity l2) } in canflowto l1' l2' @@ -391,13 +422,13 @@ -- | Privilege object corresponding to no privileges. noPriv :: TCBPriv -noPriv = MkTCBPriv { priv = emptyLabel } +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 = allLabel } +rootPrivTCB = MkTCBPriv { priv = allComponent } -- | This function creates any privilege object given an untrusted -- privilege 'Priv'. Note that this function should not be exported @@ -408,7 +439,7 @@ -- | @TCBPriv@ is an instance of 'Monoid'. instance Monoid TCBPriv where mempty = noPriv - mappend p1 p2 = createPrivTCB $ toLNF ((priv p1) `and_label` (priv p2)) + 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 @@ -441,7 +472,7 @@ instance Owns Disj where owns p d = priv p `impliesDisj` d -instance Owns Label where +instance Owns Component where owns p l = priv p `implies` l @@ -459,13 +490,52 @@ -- | 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 label. -listToLabel :: [Disj] -> Label -- ^ Given list return category. -listToLabel = MkLabel . MkConj +-- | Given a list of categories, return a component. +listToComponent :: [Disj] -> Component -- ^ Given list return category. +listToComponent = MkComponent . MkConj --- | Given a label return a list of categories. -labelToList :: Label -> [Disj] -- ^ Given category return list. -labelToList = conj . label +-- | Given a component return a list of categories. +componentToList :: Component -> [Disj] -- ^ Given category return list. +componentToList = conj . component + + + +-- +-- 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 + +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 + +instance Serialize DCLabel where + put (MkDCLabel s i) = put s >> put i + get = do s <- get + i <- get + return $ MkDCLabel s i + diff --git a/DCLabel/Integrity.hs b/DCLabel/Integrity.hs --- a/DCLabel/Integrity.hs +++ b/DCLabel/Integrity.hs @@ -1,11 +1,10 @@ {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) {-# LANGUAGE Trustworthy #-} -#else -#warning "This module is not using SafeHaskell" #endif {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} +-- | This module implements integrity-only DC Labels. module DCLabel.Integrity ( ILabel(..) ) where import DCLabel.Core @@ -21,12 +20,12 @@ bottom = MkILabel bottom top = MkILabel top join (MkILabel l1) (MkILabel l2) = MkILabel $ - join l1 { secrecy = emptyLabel } l2 { secrecy = emptyLabel } + join l1 { secrecy = emptyComponent } l2 { secrecy = emptyComponent } meet (MkILabel l1) (MkILabel l2) = MkILabel $ - meet l1 { secrecy = emptyLabel } l2 { secrecy = emptyLabel } + meet l1 { secrecy = emptyComponent } l2 { secrecy = emptyComponent } canflowto (MkILabel l1) (MkILabel l2) = - canflowto l1 { secrecy = emptyLabel } l2 { secrecy = emptyLabel } + canflowto l1 { secrecy = emptyComponent } l2 { secrecy = emptyComponent } instance RelaxedLattice ILabel where canflowto_p p (MkILabel l1) (MkILabel l2) = - canflowto_p p l1 { secrecy = emptyLabel } l2 { secrecy = emptyLabel } + canflowto_p p l1 { secrecy = emptyComponent } l2 { secrecy = emptyComponent } diff --git a/DCLabel/NanoEDSL.hs b/DCLabel/NanoEDSL.hs --- a/DCLabel/NanoEDSL.hs +++ b/DCLabel/NanoEDSL.hs @@ -1,18 +1,16 @@ {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) {-# LANGUAGE Trustworthy #-} -#else -#warning "This module is not using SafeHaskell" #endif {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} {-| This module implements a ``nano``, very simple, embedded domain specific - language to create 'Label's and 'Priv'ilages from conjunctions of + language to create 'Component's and 'Priv'ilages from conjunctions of principal disjunctions. - A 'Label'/'Priv' is created using the ('.\/.') and ('./\.') operators. + 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: @@ -37,7 +35,7 @@ category set is composed of the conjunction of categories, ('.\/.') binds more tightly than ('./\.'). - Given two 'Label's, one for secrecy and one for integrity, you can + 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'. @@ -75,81 +73,86 @@ ) where import DCLabel.Core +import qualified Data.ByteString as B +import qualified Data.ByteString.Char8 as C infixl 7 .\/. infixl 6 ./\. -- | Class used to create single-principal labels. class Singleton a where - singleton :: a -> Label -- ^ Creates a singleton label. + singleton :: a -> Component -- ^ Creates a singleton component. instance Singleton Principal where - singleton p = MkLabel $ MkConj [ MkDisj [p] ] + singleton p = MkComponent $ MkConj [ MkDisj [p] ] instance Singleton String where - singleton s = MkLabel $ MkConj [ MkDisj [principal s] ] + 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 -> Label -- ^ Given two elements it joins them with ⋁ + (.\/.) :: a -> b -> Component -- ^ Given two elements it joins them with ⋁ instance DisjunctionOf Principal Principal where - p1 .\/. p2 = MkLabel $ MkConj [ MkDisj [p1,p2] ] + p1 .\/. p2 = MkComponent $ MkConj [ MkDisj [p1,p2] ] -instance DisjunctionOf Principal Label where - p .\/. l = (singleton p) `or_label` l +instance DisjunctionOf Principal Component where + p .\/. l = (singleton p) `or_component` l -instance DisjunctionOf Label Principal where +instance DisjunctionOf Component Principal where l .\/. p = p .\/. l -instance DisjunctionOf Label Label where - l1 .\/. l2 = l1 `or_label` l2 +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 Label where +instance DisjunctionOf String Component where s .\/. l = singleton s .\/. l -instance DisjunctionOf Label String where +instance DisjunctionOf Component String where l .\/. p = p .\/. l -- | Class used to create conjunctions. class ConjunctionOf a b where - (./\.) :: a -> b -> Label -- ^ Given two elements it joins them with ⋀ + (./\.) :: a -> b -> Component -- ^ Given two elements it joins them with ⋀ instance ConjunctionOf Principal Principal where - p1 ./\. p2 = MkLabel $ MkConj [ MkDisj [p1], MkDisj [p2] ] + p1 ./\. p2 = MkComponent $ MkConj [ MkDisj [p1], MkDisj [p2] ] -instance ConjunctionOf Principal Label where - p ./\. l = singleton p `and_label` l +instance ConjunctionOf Principal Component where + p ./\. l = singleton p `and_component` l -instance ConjunctionOf Label Principal where +instance ConjunctionOf Component Principal where l ./\. p = p ./\. l -instance ConjunctionOf Label Label where - l1 ./\. l2 = l1 `and_label` l2 +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 Label where - s ./\. l = singleton s `and_label` l +instance ConjunctionOf String Component where + s ./\. l = singleton s `and_component` l -instance ConjunctionOf Label String where +instance ConjunctionOf Component String where l ./\. s = s ./\. l -- | Instances using disjunctions. instance ConjunctionOf Disj Disj where - d1 ./\. d2 = MkLabel $ MkConj [ d1, d2 ] + d1 ./\. d2 = MkComponent $ MkConj [ d1, d2 ] -instance ConjunctionOf Disj Label where - d ./\. l = (MkLabel $ MkConj [d]) `and_label` l +instance ConjunctionOf Disj Component where + d ./\. l = (MkComponent $ MkConj [d]) `and_component` l -instance ConjunctionOf Label Disj where +instance ConjunctionOf Component Disj where l ./\. d = d ./\. l instance ConjunctionOf Principal Disj where @@ -166,13 +169,13 @@ --- | Empty label. -(<>) :: Label -(<>) = emptyLabel +-- | Empty component (logically this is @True@). +(<>) :: Component +(<>) = emptyComponent --- | All label. -(><) :: Label -(><) = allLabel +-- | All component (logically this is @False@). +(><) :: Component +(><) = allComponent --- --- Creating 'DCLabel's @@ -182,22 +185,22 @@ class NewDC a b where newDC :: a -> b -> DCLabel -- ^ Given two elements create label. -instance NewDC Label Label where +instance NewDC Component Component where newDC l1 l2 = MkDCLabel l1 l2 -instance NewDC Principal Label where +instance NewDC Principal Component where newDC p l = MkDCLabel (singleton p) l -instance NewDC Label Principal where +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 Label where +instance NewDC String Component where newDC p l = MkDCLabel (singleton p) l -instance NewDC Label String where +instance NewDC Component String where newDC l p = MkDCLabel l (singleton p) instance NewDC String String where @@ -215,7 +218,7 @@ newTCBPriv :: TCBPriv -> a -> Maybe TCBPriv newTCBPriv p = delegatePriv p . newPriv -instance NewPriv Label where +instance NewPriv Component where newPriv = id instance NewPriv Principal where diff --git a/DCLabel/PrettyShow.hs b/DCLabel/PrettyShow.hs --- a/DCLabel/PrettyShow.hs +++ b/DCLabel/PrettyShow.hs @@ -1,18 +1,21 @@ {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) {-# LANGUAGE Trustworthy #-} -#else -#warning "This module is not using SafeHaskell" #endif {-| This module exports a function 'prettyShow' that pretty prints 'Principal's, -'Disj'unctions, 'Conj'unctions, 'Label's and 'DCLabel'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 +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +-- import safe Text.PrettyPrint import Text.PrettyPrint +#else +import Text.PrettyPrint +#endif @@ -28,18 +31,19 @@ pShow (MkDisj xs) = bracks $ showDisj xs where showDisj [] = empty showDisj [x] = pShow x - showDisj (x:xs) = pShow x <+> ( text "\\/") <+> showDisj xs + showDisj (x:ys) = pShow x <+> ( text "\\/") <+> showDisj ys bracks x = lbrack <> x <> rbrack instance PrettyShow Conj where - pShow (MkConj []) = empty + pShow (MkConj []) = text "True" pShow (MkConj (x:[])) = pShow x pShow (MkConj (x:xs)) = pShow x <+> (text "/\\") <+> pShow (MkConj xs) -instance PrettyShow Label where - pShow MkLabelAll = braces $ text "ALL" - pShow l = let (MkLabel conj) = toLNF l - in braces $ pShow conj +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 diff --git a/DCLabel/Safe.hs b/DCLabel/Safe.hs --- a/DCLabel/Safe.hs +++ b/DCLabel/Safe.hs @@ -1,24 +1,22 @@ {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) {-# LANGUAGE Trustworthy #-} -#else -#warning "This module is not using SafeHaskell" #endif {-| This module exports a safe-subset of "DCLabel.Core", -implementing Disjunction Category Labels. +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 Labels with EDSL +module DCLabel.Safe ( -- * DC Components with EDSL join, meet, top, bottom, canflowto - , Label(..), DCLabel(..), Disj(..), Conj(..) + , Component(..), DCLabel(..), Disj(..), Conj(..) , Principal, principal, name, singleton , listToDisj, disjToList - , listToLabel, labelToList + , listToComponent, componentToList , (.\/.), (./\.) , (<>), (><) , newDC diff --git a/DCLabel/Secrecy.hs b/DCLabel/Secrecy.hs --- a/DCLabel/Secrecy.hs +++ b/DCLabel/Secrecy.hs @@ -1,11 +1,10 @@ {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) {-# LANGUAGE Trustworthy #-} -#else -#warning "This module is not using SafeHaskell" #endif {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} +-- | This module implements secrecy-only DC Labels. module DCLabel.Secrecy ( SLabel(..) ) where import DCLabel.Core @@ -21,12 +20,12 @@ bottom = MkSLabel bottom top = MkSLabel top join (MkSLabel l1) (MkSLabel l2) = MkSLabel $ - join l1 { integrity = emptyLabel } l2 { integrity = emptyLabel } + join l1 { integrity = emptyComponent } l2 { integrity = emptyComponent } meet (MkSLabel l1) (MkSLabel l2) = MkSLabel $ - meet l1 { integrity = emptyLabel } l2 { integrity = emptyLabel } + meet l1 { integrity = emptyComponent } l2 { integrity = emptyComponent } canflowto (MkSLabel l1) (MkSLabel l2) = - canflowto l1 { integrity = emptyLabel } l2 { integrity = emptyLabel } + canflowto l1 { integrity = emptyComponent } l2 { integrity = emptyComponent } instance RelaxedLattice SLabel where canflowto_p p (MkSLabel l1) (MkSLabel l2) = - canflowto_p p l1 { integrity = emptyLabel } l2 { integrity = emptyLabel } + canflowto_p p l1 { integrity = emptyComponent } l2 { integrity = emptyComponent } 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/Tests/Main.hs b/Tests/Main.hs deleted file mode 100644 --- a/Tests/Main.hs +++ /dev/null @@ -1,188 +0,0 @@ -module Main (main) where - -import Test.QuickCheck hiding (label) -import Control.Monad (liftM) -import DCLabel.TCB -import DCLabel.PrettyShow -import DCLabel.Secrecy -import DCLabel.Integrity -import Data.List (tails) -import System.Environment (getArgs) - -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 Label where - arbitrary = do m <- choose (0, 1) :: Gen Int - if m==0 then mkArbLbl arbitrary - else return MkLabelAll - where mkArbLbl :: Gen Conj -> Gen Label - mkArbLbl = liftM MkLabel - -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 - --- cleanLabel does not modify the semantics of the label -prop_cleanLabel :: Label -> Bool -prop_cleanLabel l = let l' = cleanLabel l - in l `implies` l' && l' `implies` l - --- Reduction function toLNF does not modify the semantics of the label -prop_toLNF :: Label -> 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 Label) $ \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 l1 = 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 == allLabel || gs == allLabel - then allLabel - else rs' `and_label` rs'' - ri = (li `and_label` lp) `or_label` gi - in toLNF $ simpleNewLabel p (newDC rs ri) - where getCats = conj . label - c2l = MkLabel . MkConj - simpleNewLabel p lr | p == rootPrivTCB = g - | p == 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) -main = do - putStrLn "Run program with number of runs" - n <- getArgs >>= return . read . head - let args = stdArgs { maxSuccess = n, maxSize = n, maxDiscard = 10000} - putStrLn "Checking function cleanLabel..." - quickCheckWith args (prop_cleanLabel :: Label -> Bool) - putStrLn "Checking function toLNF..." - quickCheckWith args (prop_toLNF :: Label -> Bool) - putStrLn "Checking idempotence of function toLNF..." - quickCheckWith args (prop_toLNF_idem :: Property) - putStrLn "Checking the property of top..." - quickCheckWith args (prop_dc_top :: DCLabel -> Property) - putStrLn "Checking the property of bottom..." - quickCheckWith args (prop_dc_bottom :: DCLabel -> Property) - putStrLn "Checking the join operation..." - quickCheckWith args (prop_DC_join :: (DCLabel, DCLabel) -> Bool) - putStrLn "Checking the join operation is indeed the least upper bound..." - quickCheckWith args (prop_dc_join_lub :: (DCLabel, DCLabel) -> Property) - putStrLn "Checking the meet operation..." - quickCheckWith args (prop_dc_meet :: (DCLabel, DCLabel) -> Bool) - putStrLn "Checking the meet operation is indeed the greatest lower bound..." - quickCheckWith args (prop_dc_meet_glb :: (DCLabel, DCLabel) -> Property) - putStrLn "Checking DC labels form a partial order..." - quickCheckWith args (prop_dc_porder :: (DCLabel, DCLabel) -> Bool) - putStrLn "Checking lostar implementation..." - quickCheckWith args (prop_lostar :: TCBPriv -> DCLabel -> DCLabel -> Property) diff --git a/dclabel.cabal b/dclabel.cabal --- a/dclabel.cabal +++ b/dclabel.cabal @@ -1,5 +1,5 @@ Name: dclabel -Version: 0.0.2 +Version: 0.0.4 build-type: Simple License: BSD3 License-File: LICENSE @@ -9,14 +9,14 @@ Stability: experimental Synopsis: The Disjunction Category Label Format Category: Security -Cabal-Version: >=1.6 +Cabal-Version: >=1.8 Extra-source-files: - Examples/ExamplesDCLabels.hs - Examples/Labels.hs - Examples/ListExamples.hs - Examples/UsingEDSL.hs - Tests/Main.hs + examples/ExamplesDCLabels.hs + examples/Labels.hs + examples/ListExamples.hs + examples/UsingEDSL.hs + tests/Tests.hs Description: The /DC Label/ (DCLabel) library provides dynamic information @@ -37,9 +37,12 @@ Library Build-depends: base >= 4 && < 5, - pretty > 1.0.1 && < 2, - QuickCheck >= 2.1 + bytestring > 0.9.2 && < 2, + cereal >= 0.3.3 && < 0.4, + pretty > 1.0.1 && < 2 + ghc-options: -Wall -fno-warn-orphans + Exposed-modules: DCLabel.Safe, DCLabel.TCB, @@ -48,3 +51,20 @@ DCLabel.PrettyShow, DCLabel.Secrecy, DCLabel.Integrity + +test-suite tests + type: exitcode-stdio-1.0 + hs-source-dirs: tests + main-is: Tests.hs + + ghc-options: + -Wall -threaded -rtsopts + + build-depends: + QuickCheck, + test-framework, + test-framework-quickcheck2, + base, + dclabel, + bytestring, + cereal diff --git a/examples/ExamplesDCLabels.hs b/examples/ExamplesDCLabels.hs new file mode 100644 --- /dev/null +++ b/examples/ExamplesDCLabels.hs @@ -0,0 +1,27 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/examples/Labels.hs @@ -0,0 +1,46 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/examples/ListExamples.hs @@ -0,0 +1,45 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/examples/UsingEDSL.hs @@ -0,0 +1,34 @@ +{-# 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/tests/Tests.hs b/tests/Tests.hs new file mode 100644 --- /dev/null +++ b/tests/Tests.hs @@ -0,0 +1,195 @@ +{-# 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) + ]