diff --git a/DCLabel/Core.hs b/DCLabel/Core.hs --- a/DCLabel/Core.hs +++ b/DCLabel/Core.hs @@ -1,41 +1,101 @@ +{-| +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 ( -- * Constructors +module DCLabel.Core ( -- * Labels + -- $labels Disj(..), Conj(..), Label(..) - -- * DC Labels - , Lattice(..), DCLabel(..) , emptyLabel, allLabel + , Lattice(..) + , ToLNF(..) + -- ** DC Labels + , DCLabel(..) -- * Principals , Principal(..), principal - -- * Priviliges + -- * Privileges + -- $privs , TCBPriv(..), Priv , RelaxedLattice(..) , noPriv, rootPrivTCB , delegatePriv, createPrivTCB - , CanActFor(..) + , CanDelegate(..), Owns(..) -- * Label/internal operations - , and_label, or_label, ToLNF(..), cleanLabel, implies + , and_label, or_label, cleanLabel, implies + , DisjToFromList(..) + , listToLabel, labelToList ) where import Data.List (nub, sort, (\\)) import Data.Maybe (fromJust) +import Data.Monoid -- -- Categories -- --- | A disjunction of ordered elements. +-- | A category, i.e., disjunction, of 'Principal's. -- The empty list '[]' corresponds to the disjunction of all principals. --- In other words, conceptually, @[] = [P_1 \/ P_2 \/ ...]@ +-- Conceptually, @[] = [P_1 ⋁ P_2 ⋁ ...]@ newtype Disj = MkDisj { disj :: [Principal] } deriving (Eq, Ord, Show, Read) --- | A conjunction of ordered elements. +-- | 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 \/ ...]}@ +-- In other words, conceptually, @[] = {[P_1 ⋁ P_2 ⋁ ...]}@ newtype Conj = MkConj { conj :: [Disj] } deriving (Eq, Ord, Show, Read) @@ -43,13 +103,29 @@ -- Labels -- --- | (Bounded) Lattice definition +{- $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 + 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 @@ -59,6 +135,8 @@ | 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 @@ -67,15 +145,15 @@ -- | A label without any disjunctions or conjunctions. This label, conceptually -- corresponds to the label consisting of a single category containing all --- principals. --- In other words, conceptually, @emptyLabel = <{[P_1 \/ P_2 \/ ...]}>@ +-- 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. --- In other words, conceptually, @allLabel = <{[P_1] /\ [P_2] /\ ...}>@ +-- other labels. Conceptually, +-- @allLabel = \<{[P_1] ⋀ [P_2] ⋀ ...}\>@ allLabel :: Label allLabel = MkLabelAll @@ -118,12 +196,16 @@ -- | Determines if a conjunction of disjunctions, i.e., a label, implies -- (in the logical sense) a disjunction. In other words, it checks if --- d1 /\ ... /\ dn => d1. +-- d_1 ⋀ ... ⋀ d_n => d_1. -- --- Properties: 1. forall X, ALL `impliesDisj` X := True --- 2. forall X, X `impliesDisj` [] := True --- 3. forall X/=[], [] `impliesDisj` X := False +-- 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. @@ -135,12 +217,17 @@ , not (isEmptyLabel l) ] -- Asserts 3 -- | Determines if a label implies (in the logical sense) another label. --- In other words, d1 /\ ... /\ dn => d1' /\ ... /\ dn'. +-- In other words, d_1 ⋀ ... ⋀ d_n => d_1' ⋀ ... ⋀ d_n'. -- --- Properties: 1. forall X, ALL `implies` X := True --- 2. forall X/=ALL, X `implies` ALL := False --- 3. forall X, X `implies` [] := True --- 4. forall X/=[], [] `implies` X := False +-- 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 @@ -156,13 +243,13 @@ 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 LNF. --- It is used to overload the reduce function used by the 'Label', 'SLabel', --- 'ILabel', and 'DCLabel'. +-- | 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. +-- | 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. @@ -182,20 +269,35 @@ -- DC Labels : (Secrecy, Integrity) -- --- | A DC label for secrecy and integrity. -data DCLabel = MkDCLabel { secrecy :: Label - , integrity :: Label } +-- | 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 = MkLabel $ MkConj [] - , integrity = MkLabelAll } - top = MkDCLabel { secrecy = MkLabelAll - , integrity = MkLabel $ MkConj [] } + 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 @@ -214,7 +316,10 @@ -- Principals -- --- | Principal is a simple string. +-- | 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) @@ -224,9 +329,33 @@ -- --- Priviliges +-- 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. @@ -240,22 +369,22 @@ -- | Class extending 'Lattice', by allowing for the more relaxed label -- comparison @canflowto_p@. class (Lattice a) => RelaxedLattice a where - -- ^ Relaxed partial-order relation + -- | Relaxed partial-order relation canflowto_p :: TCBPriv -> a -> a -> Bool instance RelaxedLattice DCLabel where canflowto_p p l1 l2 = - let l1' = MkDCLabel { secrecy = (secrecy l2) - , integrity = (and_label (priv p) (integrity 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 privilige and a \"desired\" untrusted privilege, --- return a trusted version of the untrusted privilige, if the --- provided (trusted) privilige implies it. +-- | 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 @@ -267,7 +396,7 @@ noPriv = MkTCBPriv { priv = emptyLabel } -- | Privilege object corresponding to the \"root\", or all privileges. --- Any other privilige may be delegated using this privilege object and it must +-- 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 } @@ -277,21 +406,68 @@ -- 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 corresponds to the DLM \"can-act-for\". -class CanActFor a b where - -- ^ Can use first privilige in place of second. - canActFor :: a -> b -> Bool +-- 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 CanActFor Priv Priv where - canActFor p1 p2 = p1 `implies` p2 +instance CanDelegate Priv Priv where + canDelegate p1 p2 = p1 `implies` p2 -instance CanActFor Priv TCBPriv where - canActFor p1 p2 = p1 `implies` (priv p2) +instance CanDelegate Priv TCBPriv where + canDelegate p1 p2 = p1 `implies` (priv p2) -instance CanActFor TCBPriv Priv where - canActFor p1 p2 = (priv p1) `implies` p2 +instance CanDelegate TCBPriv Priv where + canDelegate p1 p2 = (priv p1) `implies` p2 -instance CanActFor TCBPriv TCBPriv where - canActFor p1 p2 = (priv p1) `implies` (priv 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 --- a/DCLabel/Integrity.hs +++ b/DCLabel/Integrity.hs @@ -4,7 +4,7 @@ import DCLabel.Core --- ^ An integrity-only DC label. +-- | An integrity-only DC label. newtype ILabel = MkILabel DCLabel deriving (Eq, Show, Read) diff --git a/DCLabel/NanoEDSL.hs b/DCLabel/NanoEDSL.hs --- a/DCLabel/NanoEDSL.hs +++ b/DCLabel/NanoEDSL.hs @@ -1,3 +1,60 @@ +{-| 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 #-} @@ -26,9 +83,9 @@ singleton s = MkLabel $ MkConj [ MkDisj [principal s] ] --- | Class used to create disjunctions +-- | Class used to create disjunctions. class DisjunctionOf a b where - (.\/.) :: a -> b -> Label + (.\/.) :: a -> b -> Label -- ^ Given two elements it joins them with ⋁ instance DisjunctionOf Principal Principal where p1 .\/. p2 = MkLabel $ MkConj [ MkDisj [p1,p2] ] @@ -52,9 +109,9 @@ l .\/. p = p .\/. l --- | Class used to create conjunctions +-- | Class used to create conjunctions. class ConjunctionOf a b where - (./\.) :: a -> b -> Label + (./\.) :: a -> b -> Label -- ^ Given two elements it joins them with ⋀ instance ConjunctionOf Principal Principal where p1 ./\. p2 = MkLabel $ MkConj [ MkDisj [p1], MkDisj [p2] ] @@ -68,7 +125,7 @@ instance ConjunctionOf Label Label where l1 ./\. l2 = l1 `and_label` l2 --- | Instances usng strings and not principals +-- | Instances using strings and not principals instance ConjunctionOf String String where s1 ./\. s2 = singleton s1 ./\. singleton s2 @@ -78,7 +135,30 @@ 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 @@ -122,9 +202,9 @@ -- | Class used to create 'Priv's and 'TCBPriv's. class NewPriv a where - -- ^ Given element create privilege. + -- | Given element create privilege. newPriv :: a -> Priv - -- ^ Given element create (maybe) trusted privileged object. + -- | Given privilege and new element, create (maybe) trusted privileged object. newTCBPriv :: TCBPriv -> a -> Maybe TCBPriv newTCBPriv p = delegatePriv p . newPriv diff --git a/DCLabel/PrettyShow.hs b/DCLabel/PrettyShow.hs --- a/DCLabel/PrettyShow.hs +++ b/DCLabel/PrettyShow.hs @@ -1,15 +1,20 @@ +{-| 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 used to create a 'Doc' type of DCLabel-related types class PrettyShow a where - pShow :: a -> Doc + pShow :: a -> Doc -- ^ Convert to 'Doc'. --- ^ Render a 'PrettyShow' type to a string. +-- | Render a 'PrettyShow' type to a string. prettyShow :: PrettyShow a => a -> String prettyShow = render . pShow @@ -36,3 +41,12 @@ 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 --- a/DCLabel/Safe.hs +++ b/DCLabel/Safe.hs @@ -11,14 +11,16 @@ join, meet, top, bottom, canflowto , Label, DCLabel, secrecy, integrity , principal + , listToDisj, disjToList + , listToLabel, labelToList , (.\/.), (./\.) , (<>), (><) , newDC - -- * Priviligies + -- * Privilegies , TCBPriv, Priv , canflowto_p , delegatePriv - , canActFor + , canDelegate, owns , newPriv, newTCBPriv ) where diff --git a/DCLabel/Secrecy.hs b/DCLabel/Secrecy.hs --- a/DCLabel/Secrecy.hs +++ b/DCLabel/Secrecy.hs @@ -4,7 +4,7 @@ import DCLabel.Core --- ^ A secrecy-only DC label. +-- | A secrecy-only DC label. newtype SLabel = MkSLabel DCLabel deriving (Eq, Show, Read) 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/Tests/Main.hs b/Tests/Main.hs --- a/Tests/Main.hs +++ b/Tests/Main.hs @@ -2,7 +2,8 @@ import Test.QuickCheck hiding (label) import Control.Monad (liftM) -import DCLabel.Core +import DCLabel.TCB +import DCLabel.PrettyShow import DCLabel.Secrecy import DCLabel.Integrity import Data.List (tails) @@ -53,6 +54,9 @@ 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 @@ -119,6 +123,30 @@ 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 @@ -143,6 +171,5 @@ 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-eci11.cabal b/dclabel-eci11.cabal --- a/dclabel-eci11.cabal +++ b/dclabel-eci11.cabal @@ -1,22 +1,41 @@ Name: dclabel-eci11 -Version: 0.2 +Version: 0.3 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: Alejandro Russo < russo at chalmers dot se >, Deian Stefan +Maintainer: Deian Stefan , + Alejandro Russo < russo at chalmers dot se >, Stability: experimental -Synopsis: Dynamic labels to assign confidentiality and integrity levels in scenarios of mutual distrust +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:s A package that provides dynamic labels in the form of conjunctions of disjunctions of principals. This package is intended to only be used at the computer science school ECI 2011 (Buenos Aires, Argentina) . Please, refer to the official release of dclabels if you plan to use it for other purposes. +Description: + A package that provides dynamic labels in the form of conjunctions of disjunctions of principals. This package is intended to only be used at the computer science school ECI 2011 (Buenos Aires, Argentina) . Please, refer to the official release of dclabels if you plan to use it for other purposes. + 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 + documented in "DCLabel.NanoEDSL". DCLabel was implemented by David + Mazieres (), Deian Stefan + (), and Alejandro Russo + (). + + To obtain the latest experimental source code, run: + + @git clone http:\/\/www.scs.stanford.edu\/~deian\/dclabel.git@ + Library Build-depends: base >= 4 && < 5, pretty > 1.0.1 && < 2, @@ -24,6 +43,7 @@ Exposed-modules: DCLabel.Safe, + DCLabel.TCB, DCLabel.Core, DCLabel.NanoEDSL, DCLabel.PrettyShow,