dclabel (empty) → 0.0.1
raw patch · 14 files changed
+1212/−0 lines, 14 filesdep +QuickCheckdep +basedep +prettysetup-changed
Dependencies added: QuickCheck, base, pretty
Files
- DCLabel/Core.hs +470/−0
- DCLabel/Integrity.hs +26/−0
- DCLabel/NanoEDSL.hs +219/−0
- DCLabel/PrettyShow.hs +52/−0
- DCLabel/Safe.hs +37/−0
- DCLabel/Secrecy.hs +26/−0
- DCLabel/TCB.hs +25/−0
- Examples/ExamplesDCLabels.hs +26/−0
- Examples/Labels.hs +45/−0
- Examples/UsingEDSL.hs +33/−0
- LICENSE +25/−0
- Setup.hs +3/−0
- Tests/Main.hs +175/−0
- dclabel.cabal +50/−0
+ DCLabel/Core.hs view
@@ -0,0 +1,470 @@+{-|+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 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+all the restrictions imposed by the categories of @L_1@ (hence the conjunction)+in the case of secrecy, and at least as permissive in the case of integrity.+More specifically, for information to flow from @L_1@ to @L_2@, the labels+must satisfy the \"can-flow-to\" relation: @L_1 ⊑ L_2@. The ⊑+label check is implemented by the 'canflowto' function. For labels+@L_1=\<S_1, I_1\>@, @L_2=\<S_2, I_2\>@ the can-flow-to relation is satisfied+if the secrecy category set @S_2@ 'implies' @S_1@ and @I_1@ 'implies' @I_2@+(recall that a category set is a conjunction of disjunctions of principals).+For example, @\<{[P_1 ⋁ P_2]},{}\> ⊑ \<{[P_1]},{}\>@ because data+that can be read by @P_1@ is more restricting than that readable by @P_1@+or @P_2@. Conversely, @\<{{},[P_1]}\> ⊑ \<{},[P_1 ⋁ P_2]},{}\>@+because data vouched for by @P_1@ or @P_2@ is more permissive than just @P_1@+(note the same idea holds when writing to sinks with such labeling).++A piece of a code running with a privilege object (of type 'TCBPriv'), i.e.,+owning a 'Principal' confers the right to modify labels by removing any+'secrecy' categories containing that 'Principal' and adding any 'integrity'+categories containing the 'Principal' (hence the name disjunction categories:+the category @[P1 ⋁ P2]@ can be /downgraded/ by either 'Principal'+@P1@ or @P2@). More specifically, privileges can be used to bypass+information flow restrictions by using the more permissive \"can-flow-to given+permission\" relation:⊑ᵨ. The label check function implementing+this restriction is 'canflowto_p', taking an additional argument (of type+'TCBPriv'). For example, if @L_1=\<{[P_1 ⋁ P_2] ⋀ [P_3]},{}\>@,+and @L_2=\<{[P_1]},{}\>@, then @L_1 ⋢ L_2@, but given a privilege+object corresponding to @[P_3]@ the @L_1 ⊑ᵨ L_2@ holds.++To construct DC labels and privilege objects the constructors exported by+this module may be used, but we strongly suggest using "DCLabel.NanoEDSL"+as exported by "DCLabel.TCB" and "DCLabel.Safe". The former is to be used by+trusted code only, while the latter module should be imported by untrusted+code as it prevents the creation of arbitrary privileges.++-}++{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+module DCLabel.Core ( -- * Labels + -- $labels+ Disj(..), Conj(..), Label(..)+ , emptyLabel, allLabel+ , Lattice(..)+ , ToLNF(..)+ -- ** DC Labels+ , DCLabel(..)+ -- * Principals+ , Principal(..), principal+ -- * Privileges+ -- $privs+ , TCBPriv(..), Priv+ , RelaxedLattice(..)+ , noPriv, rootPrivTCB+ , delegatePriv, createPrivTCB+ , CanDelegate(..), Owns(..)+ -- * Label/internal operations+ , and_label, or_label, cleanLabel, implies+ , DisjToFromList(..)+ , listToLabel, labelToList+ ) where+++import Data.List (nub, sort, (\\))+import Data.Maybe (fromJust)+import Data.Monoid++--+-- Categories+--++-- | A category, i.e., disjunction, of 'Principal's.+-- The empty list '[]' corresponds to the disjunction of all principals.+-- Conceptually, @[] = [P_1 ⋁ P_2 ⋁ ...]@+newtype Disj = MkDisj { disj :: [Principal] }+ deriving (Eq, Ord, Show, Read)+++-- | A category set, i.e., a conjunction of disjunctions. +-- The empty list '[]' corresponds to the single disjunction of all principals.+-- In other words, conceptually, @[] = {[P_1 ⋁ P_2 ⋁ ...]}@+newtype Conj = MkConj { conj :: [Disj] }+ deriving (Eq, Ord, Show, Read)++--+-- Labels+--++{- $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.+-}++-- | Labels forma a partial order according to the ⊑ relation.+-- Specifically, this means that for any two labels @L_1@ and @L_2@ there is a +-- unique label @L_3 = L_1 ⊔ L_2@, known as the /join/, such that+-- @L_1 ⊑ L_3@ and @L_2 ⊑ L_3@. Similarly, there is a unique label +-- @L_3' = L_1 ⊓ L_2@, known as the /meet/, such that+-- @L_3 ⊑ L_1@ and @L_3 ⊑ L_2@. This class defines a /bounded/ +-- lattice, which further requires the definition of the /bottom/ ⊥ and +-- /top/ ⊤ elements of the lattice, such that @⊥ ⊑ L@ and+-- @L ⊑ ⊤@ for any label @L@.+class Eq a => Lattice a where+ bottom :: a -- ^ Bottom of lattice, ⊥+ top :: a -- ^ Top of lattice, ⊤+ join :: a -> a -> a -- ^ Join of two elements, ⊔+ meet :: a -> a -> a -- ^ Meet of two elements, ⊓+ canflowto :: a -> a -> Bool -- ^ Partial order relation, ⊑+++-- | A 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 }+ deriving (Show, Read)++-- | Labels 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)++-- | A label without any disjunctions or conjunctions. This label, conceptually+-- corresponds to the label consisting of a single category containing all+-- principals. Conceptually,+-- @emptyLabel = \<{[P_1 ⋁ P_2 ⋁ ...]}\>@+emptyLabel :: Label+emptyLabel = MkLabel (MkConj [])++-- | The dual of 'emptyLabel', 'allLabel' consists of the conjunction of+-- all possible disjunctions, i.e., it is the label that implies all+-- other labels. Conceptually,+-- @allLabel = \<{[P_1] ⋀ [P_2] ⋀ ...}\>@+allLabel :: Label+allLabel = MkLabelAll++-- | 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) ]++-- | Predicate function that retuns @True@ if the label corresponds to+-- the 'allLabel'.+isAllLabel :: Label -> Bool+isAllLabel MkLabelAll = True+isAllLabel _ = False+++--+-- Helper functions+--+++-- | 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 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] ++-- | Determines if a conjunction of disjunctions, i.e., a label, implies+-- (in the logical sense) a disjunction. In other words, it checks if+-- d_1 ⋀ ... ⋀ d_n => d_1.+--+-- Properties:+--+-- * ∀ X, 'allLabel' \``impliesDisj`\` X = True+--+-- * ∀ X, X \``impliesDisj`\` 'emptyLabel' = True+--+-- * ∀ X≠'emptyLabel', 'emptyLabel' \``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 +-- non-null disjunction.+impliesDisj :: Label -> Disj -> Bool +impliesDisj l d | isAllLabel 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++-- | Determines if a label implies (in the logical sense) another label. +-- In other words, d_1 ⋀ ... ⋀ d_n => d_1' ⋀ ... ⋀ d_n'.+--+-- Properties:+--+-- * ∀ X, 'allLabel' \``implies`\` X := True+--+-- * ∀ X≠'allLabel', X \``implies`\` 'allLabel' := False+--+-- * ∀ X, X \``implies`\` 'emptyLabel' := True+--+-- * ∀ X≠'emptyLabel', 'emptyLabel' \``implies`\` X := False+implies :: Label -> Label -> Bool +implies l1 l2 | isAllLabel l1 = True -- Asserts 1+ | isAllLabel l2 = False -- Asserts 2+ | otherwise = and [ impliesDisj l1 d + | d <- conj . label . 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.+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+ extraneous = [ d2 | d1 <- l', d2 <- l', d1 /= d2+ , impliesDisj ((MkLabel . MkConj) [d1]) d2 ]++--+-- DC Labels+--+++--+-- DC Labels : (Secrecy, Integrity)+--++-- | 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.+ } + deriving (Eq, Show, Read)++-- | 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)}++-- | Elements of 'DCLabel' form a bounded lattice, where:+--+-- * @⊥ = \<'emptyLabel', 'allLabel'\>@+--+-- * @⊤ = \<'allLabel', 'emptyLabel'\>@+--+-- * @ \<S_1, I_1\> ⊔ \<S_2, I_2\> = \<S_1 ⋀ S_2, I_1 ⋁ I_2\>@+--+-- * @ \<S_1, I_1\> ⊓ \<S_2, I_2\> = \<S_1 ⋁ S_2, I_1 ⋀ I_2\>@+--+-- * @ \<S_1, I_1\> ⊑ \<S_2, I_2\> = S_2 => S_1 ⋀ I_1 => I_2@+instance Lattice DCLabel where+ bottom = MkDCLabel { secrecy = emptyLabel+ , integrity = allLabel }+ top = MkDCLabel { secrecy = allLabel+ , integrity = emptyLabel }+ join l1 l2 = let s3 = (secrecy l1) `and_label` (secrecy l2)+ i3 = (integrity l1) `or_label` (integrity l2)+ 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)+ 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'))+++--+-- 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 labels or be ignoerd a corresponding +-- privilege ('TCBPriv') must be created (by trusted code) or delegated.+newtype Principal = MkPrincipal { name :: String }+ deriving (Eq, Ord, Show, Read)++-- | Generates a principal from an string. +principal :: String -> Principal +principal = MkPrincipal+++--+-- 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 '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 +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., a 'Label'.+-- 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 } + deriving (Eq, Show)++-- | Untrusted privileged object, which can be converted to a 'TCBPriv' with+-- 'delegatePriv'.+type Priv = Label++-- | 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_label (priv p) (integrity l1)) }+ l2' = MkDCLabel { secrecy = (and_label (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 = emptyLabel }++-- | 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 }++-- | 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_label` (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 Label 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 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 label return a list of categories.+labelToList :: Label -> [Disj] -- ^ Given category return list.+labelToList = conj . label
+ DCLabel/Integrity.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+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 = emptyLabel } l2 { secrecy = emptyLabel }+ meet (MkILabel l1) (MkILabel l2) = MkILabel $ + meet l1 { secrecy = emptyLabel } l2 { secrecy = emptyLabel }+ canflowto (MkILabel l1) (MkILabel l2) =+ canflowto l1 { secrecy = emptyLabel } l2 { secrecy = emptyLabel }++instance RelaxedLattice ILabel where+ canflowto_p p (MkILabel l1) (MkILabel l2) =+ canflowto_p p l1 { secrecy = emptyLabel } l2 { secrecy = emptyLabel }
+ DCLabel/NanoEDSL.hs view
@@ -0,0 +1,219 @@+{-| This module implements a ``nano``, very simple, embedded domain specific+ language to create 'Label's and 'Priv'ilages from conjunctions of+ principal disjunctions.+ + A 'Label'/'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 'Label's, one for secrecy and one for integrity, you can+ create a 'DCLabel' with 'newDC'. And, similarly, given a 'TCBPriv' and 'Priv' + you can create a new minted privilege with 'newTCBPriv'.+ + + Consider the following, example:++ @+ l1 = \"Alice\" '.\/.' \"Bob\" './\.' \"Carla\" + l2 = \"Alice\" './\.' \"Carla\" + dc1 = 'newDC' l1 l2+ dc2 = 'newDC' \"Deian\" \"Alice\"+ pr = 'createPrivTCB' $ 'newPriv' (\"Alice\" './\.' \"Carla\")+ @++where++ * @ dc1 = \<{[\"Alice\" ⋁ \"Bob\"] ⋀ [\"Carla\"]} , {[\"Alice\"] ⋀ [\"Carla\"]}\>@+ + * @ dc2 = \<{[\"Deian\"]} , {[\"Alice\"]}\>@++ * @ 'canflowto' dc1 dc2 = False @++ * @ 'canflowto_p' pr dc1 dc2 = True@++-}+++{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+module DCLabel.NanoEDSL ( -- * Operators+ (.\/.), (./\.)+ , (<>), (><)+ , singleton+ -- * DCLabel creation+ , newDC+ -- * Privilege object creation+ , NewPriv, newPriv, newTCBPriv+ ) where++import DCLabel.Core++infixl 7 .\/.+infixl 6 ./\.++-- | Class used to create single-principal labels.+class Singleton a where + singleton :: a -> Label -- ^ Creates a singleton label.++instance Singleton Principal where + singleton p = MkLabel $ MkConj [ MkDisj [p] ]++instance Singleton String where + singleton s = MkLabel $ MkConj [ MkDisj [principal s] ]+++-- | Class used to create disjunctions.+class DisjunctionOf a b where+ (.\/.) :: a -> b -> Label -- ^ Given two elements it joins them with ⋁++instance DisjunctionOf Principal Principal where+ p1 .\/. p2 = MkLabel $ MkConj [ MkDisj [p1,p2] ]++instance DisjunctionOf Principal Label where+ p .\/. l = (singleton p) `or_label` l ++instance DisjunctionOf Label Principal where+ l .\/. p = p .\/. l++instance DisjunctionOf Label Label where+ l1 .\/. l2 = l1 `or_label` l2++instance DisjunctionOf String String where+ s1 .\/. s2 = singleton s1 .\/. singleton s2++instance DisjunctionOf String Label where+ s .\/. l = singleton s .\/. l ++instance DisjunctionOf Label 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 ⋀++instance ConjunctionOf Principal Principal where+ p1 ./\. p2 = MkLabel $ MkConj [ MkDisj [p1], MkDisj [p2] ] ++instance ConjunctionOf Principal Label where+ p ./\. l = singleton p `and_label` l ++instance ConjunctionOf Label Principal where+ l ./\. p = p ./\. l ++instance ConjunctionOf Label Label where+ l1 ./\. l2 = l1 `and_label` 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 Label String where+ l ./\. s = s ./\. l ++-- | Instances using disjunctions.+instance ConjunctionOf Disj Disj where+ d1 ./\. d2 = MkLabel $ MkConj [ d1, d2 ] ++instance ConjunctionOf Disj Label where+ d ./\. l = (MkLabel $ MkConj [d]) `and_label` l ++instance ConjunctionOf Label 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 label.+(<>) :: Label+(<>) = emptyLabel++-- | All label.+(><) :: Label+(><) = allLabel++---+--- 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 Label Label where+ newDC l1 l2 = MkDCLabel l1 l2 ++instance NewDC Principal Label where+ newDC p l = MkDCLabel (singleton p) l ++instance NewDC Label 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+ newDC p l = MkDCLabel (singleton p) l ++instance NewDC Label 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 Label where+ newPriv = id++instance NewPriv Principal where+ newPriv p = singleton p++instance NewPriv String where+ newPriv p = singleton p
+ DCLabel/PrettyShow.hs view
@@ -0,0 +1,52 @@+{-| This module exports a function 'prettyShow' that pretty prints 'Principal's,+'Disj'unctions, 'Conj'unctions, 'Label'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:xs) = pShow x <+> ( text "\\/") <+> showDisj xs+ bracks x = lbrack <> x <> rbrack++instance PrettyShow Conj where + pShow (MkConj []) = empty+ 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 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/Safe.hs view
@@ -0,0 +1,37 @@+{-|+This module exports a safe-subset of "DCLabel.Core",+implementing Disjunction Category Labels. +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+ join, meet, top, bottom, canflowto+ , Label, DCLabel, secrecy, integrity+ , principal, singleton+ , listToDisj, disjToList+ , listToLabel, labelToList+ , (.\/.), (./\.)+ , (<>), (><)+ , newDC+ -- * Privilegies + , TCBPriv, Priv+ , canflowto_p+ , delegatePriv+ , canDelegate, owns+ , newPriv, NewPriv, newTCBPriv+ ) where++import DCLabel.Core+import DCLabel.NanoEDSL+++++++++
+ DCLabel/Secrecy.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+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 = emptyLabel } l2 { integrity = emptyLabel }+ meet (MkSLabel l1) (MkSLabel l2) = MkSLabel $ + meet l1 { integrity = emptyLabel } l2 { integrity = emptyLabel }+ canflowto (MkSLabel l1) (MkSLabel l2) =+ canflowto l1 { integrity = emptyLabel } l2 { integrity = emptyLabel }++instance RelaxedLattice SLabel where+ canflowto_p p (MkSLabel l1) (MkSLabel l2) =+ canflowto_p p l1 { integrity = emptyLabel } l2 { integrity = emptyLabel }
+ DCLabel/TCB.hs view
@@ -0,0 +1,25 @@+{-|+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+++++++++
+ Examples/ExamplesDCLabels.hs view
@@ -0,0 +1,26 @@+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 view
@@ -0,0 +1,45 @@+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/UsingEDSL.hs view
@@ -0,0 +1,33 @@+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+
+ LICENSE view
@@ -0,0 +1,25 @@+Disjunction Category Labels +Copyright (C) 2011, Deian Stefan, Alejandro Russo, and David Mazieres+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:+ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+ * Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.+ * Neither the name of the <organization> nor the+ names of its contributors may be used to endorse or promote products+ derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,3 @@+import Distribution.Simple+main :: IO ()+main = defaultMain
+ Tests/Main.hs view
@@ -0,0 +1,175 @@+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 (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 li lg = + let lip = newDC (secrecy li) ((integrity li) ./\. lp)+ lgp = newDC ((secrecy lg) ./\. lp) (integrity lg)+ lp = priv p+ in join lip lgp++{-+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)
+ dclabel.cabal view
@@ -0,0 +1,50 @@+Name: dclabel+Version: 0.0.1+build-type: Simple+License: BSD3+License-File: LICENSE+Copyright: (c) 2011 Deian Stefan, David Mazieres, Alejandro Russo+Author: Deain Stefan, David Mazieres, Alejandro Russo+Maintainer: Deian Stefan <deian at cs dot stanford dot edu>,+ Alejandro Russo < russo at chalmers dot se >,+Stability: experimental+Synopsis: The Disjunction Category Label Format.+Category: Security+Cabal-Version: >=1.6++Extra-source-files:+ Examples/UsingEDSL.hs,+ Examples/Labels.hs,+ Examples/ExamplesDCLabels.hs,+ Tests/Main.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/>).++Source-repository head+ Type: git+ Location: http://www.scs.stanford.edu/~deian/dclabels/dclabel.git+++Library + Build-depends: base >= 4 && < 5, + pretty > 1.0.1 && < 2,+ QuickCheck >= 2.1++ Exposed-modules:+ DCLabel.Safe,+ DCLabel.TCB,+ DCLabel.Core, + DCLabel.NanoEDSL,+ DCLabel.PrettyShow,+ DCLabel.Secrecy,+ DCLabel.Integrity