packages feed

dclabel 0.0.6 → 0.9.0.0

raw patch · 22 files changed

+776/−1272 lines, 22 filesdep +containersdep +criteriondep +quickcheck-instancesdep −prettydep ~basedep ~bytestringdep ~cereal

Dependencies added: containers, criterion, quickcheck-instances

Dependencies removed: pretty

Dependency ranges changed: base, bytestring, cereal

Files

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