diff --git a/DCLabel/Core.hs b/DCLabel/Core.hs new file mode 100644 --- /dev/null +++ b/DCLabel/Core.hs @@ -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=\@, @L_2=\@ the can-flow-to relation is satisfied +if the secrecy category set @S_2@ 'implies' @S_1@ and @I_1@ 'implies' @I_2@ +(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_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 diff --git a/DCLabel/Integrity.hs b/DCLabel/Integrity.hs new file mode 100644 --- /dev/null +++ b/DCLabel/Integrity.hs @@ -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 } diff --git a/DCLabel/NanoEDSL.hs b/DCLabel/NanoEDSL.hs new file mode 100644 --- /dev/null +++ b/DCLabel/NanoEDSL.hs @@ -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 diff --git a/DCLabel/PrettyShow.hs b/DCLabel/PrettyShow.hs new file mode 100644 --- /dev/null +++ b/DCLabel/PrettyShow.hs @@ -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 diff --git a/DCLabel/Safe.hs b/DCLabel/Safe.hs new file mode 100644 --- /dev/null +++ b/DCLabel/Safe.hs @@ -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 + + + + + + + + + diff --git a/DCLabel/Secrecy.hs b/DCLabel/Secrecy.hs new file mode 100644 --- /dev/null +++ b/DCLabel/Secrecy.hs @@ -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 } diff --git a/DCLabel/TCB.hs b/DCLabel/TCB.hs new file mode 100644 --- /dev/null +++ b/DCLabel/TCB.hs @@ -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 + + + + + + + + + diff --git a/Examples/ExamplesDCLabels.hs b/Examples/ExamplesDCLabels.hs new file mode 100644 --- /dev/null +++ b/Examples/ExamplesDCLabels.hs @@ -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 +-} diff --git a/Examples/Labels.hs b/Examples/Labels.hs new file mode 100644 --- /dev/null +++ b/Examples/Labels.hs @@ -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 +-} diff --git a/Examples/UsingEDSL.hs b/Examples/UsingEDSL.hs new file mode 100644 --- /dev/null +++ b/Examples/UsingEDSL.hs @@ -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 + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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 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 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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,3 @@ +import Distribution.Simple +main :: IO () +main = defaultMain diff --git a/Tests/Main.hs b/Tests/Main.hs new file mode 100644 --- /dev/null +++ b/Tests/Main.hs @@ -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) diff --git a/dclabel.cabal b/dclabel.cabal new file mode 100644 --- /dev/null +++ b/dclabel.cabal @@ -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 , + 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 (), Deian Stefan + (), and Alejandro 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