dclabel 0.0.2 → 0.0.4

raw patch · 17 files changed

+662/−562 lines, 17 filesdep +bytestringdep +cerealdep +dclabeldep ~QuickCheckdep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: bytestring, cereal, dclabel, test-framework, test-framework-quickcheck2

Dependency ranges changed: QuickCheck, base

API changes (from Hackage documentation)

Files

• DCLabel/Core.hs +213/−143
• DCLabel/Integrity.hs +5/−6
• DCLabel/NanoEDSL.hs +46/−43
• DCLabel/PrettyShow.hs +13/−9
• DCLabel/Safe.hs +4/−6
• DCLabel/Secrecy.hs +5/−6
• Examples/ExamplesDCLabels.hs +0/−27
• Examples/Labels.hs +0/−46
• Examples/ListExamples.hs +0/−45
• Examples/UsingEDSL.hs +0/−34
• Tests/Main.hs +0/−188
• dclabel.cabal +29/−9
• examples/ExamplesDCLabels.hs +27/−0
• examples/Labels.hs +46/−0
• examples/ListExamples.hs +45/−0
• examples/UsingEDSL.hs +34/−0
• tests/Tests.hs +195/−0

@@ -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 &#8897; P_2 &#8897; ...]}@+-- 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 &#8849; relation.+-- | Labels form a partial order according to the &#8849; relation. -- Specifically, this means that for any two labels @L_1@ and @L_2@ there is a  -- unique label @L_3 = L_1 &#8852; L_2@, known as the /join/, such that -- @L_1 &#8849; L_3@ and @L_2 &#8849; L_3@. Similarly, there is a unique label @@ -126,46 +150,48 @@   canflowto :: a -> a -> Bool -- ^ Partial order relation, &#8849;  --- | 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 &#8897; P_2 &#8897; ...]}\>@-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 &#8897; P_2 &#8897; ...]}\>@.+-- 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] &#8896; [P_2] &#8896; ...}\>@-allLabel :: Label-allLabel = MkLabelAll+-- other labels. Conceptually (in a closed-world system),+-- @allComponent = \<{[P_1] &#8896; [P_2] &#8896; ...}\>@+-- 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 &#8896; ... &#8896; d_n => d_1. -- -- Properties: -----      * &#8704; X, 'allLabel' \``impliesDisj`\` X = True+--      * &#8704; X, 'allComponent' \``impliesDisj`\` X = True -----      * &#8704; X, X \``impliesDisj`\` 'emptyLabel'  = True+--      * &#8704; X, X \``impliesDisj`\` 'emptyComponent'  = True -----      * &#8704; X&#8800;'emptyLabel', 'emptyLabel' \``impliesDisj`\` X = False+--      * &#8704; X&#8800;'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 &#8896; ... &#8896; d_n => d_1' &#8896; ... &#8896; d_n'. -- -- Properties: ----- 	* &#8704; X, 'allLabel' \``implies`\` X := True+-- 	* &#8704; X, 'allComponent' \``implies`\` X := True -----      * &#8704; X&#8800;'allLabel', X \``implies`\` 'allLabel' := False+--      * &#8704; X&#8800;'allComponent', X \``implies`\` 'allComponent' := False -----      * &#8704; X, X \``implies`\` 'emptyLabel' := True+--      * &#8704; X, X \``implies`\` 'emptyComponent' := True -----      * &#8704; X&#8800;'emptyLabel', 'emptyLabel' \``implies`\` X := False-implies :: Label -> Label -> Bool -implies l1 l2 | isAllLabel l1 = True -- Asserts 1-              | isAllLabel l2 = False -- Asserts 2+--      * &#8704; X&#8800;'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: ----- 	* @&#8869; = \<'emptyLabel', 'allLabel'\>@+-- 	* @&#8869; = \<'emptyComponent', 'allComponent'\>@ ----- 	* @&#8868; = \<'allLabel', 'emptyLabel'\>@+-- 	* @&#8868; = \<'allComponent', 'emptyComponent'\>@ -- -- 	* @ \<S_1, I_1\> &#8852; \<S_2, I_2\> = \<S_1 &#8896; S_2, I_1 &#8897; I_2\>@ --@@ -292,16 +322,16 @@ -- -- 	* @ \<S_1, I_1\> &#8849; \<S_2, I_2\> = S_2 => S_1 &#8896; 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+

@@ -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 }

@@ -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 &#8897;+  (.\/.) :: a -> b -> Component -- ^ Given two elements it joins them with &#8897;  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 &#8896;+  (./\.) :: a -> b -> Component -- ^ Given two elements it joins them with &#8896;  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

@@ -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

@@ -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

@@ -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 }

@@ -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--}

@@ -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--}

@@ -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--}

@@ -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-  

@@ -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)

@@ -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

@@ -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+-}

@@ -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+-}

@@ -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+-}

@@ -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+  

@@ -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)+  ]