-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | The Disjunction Category Label Format -- -- 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/). @package dclabel @version 0.0.2 -- | 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 Principals, 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. module DCLabel.Core -- | A category, i.e., disjunction, of Principals. The empty list -- '[]' corresponds to the disjunction of all principals. Conceptually, -- [] = [P_1 ⋁ P_2 ⋁ ...] newtype Disj MkDisj :: [Principal] -> Disj disj :: Disj -> [Principal] -- | 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 :: [Disj] -> Conj conj :: Conj -> [Disj] -- | 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 :: Label MkLabel :: Conj -> Label label :: Label -> Conj -- | 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 -- | 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 -- | 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 bottom :: Lattice a => a top :: Lattice a => a join :: Lattice a => a -> a -> a meet :: Lattice a => a -> a -> a canflowto :: Lattice a => a -> a -> Bool -- | 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 toLNF :: ToLNF a => a -> a -- | A DCLabel is a pair of secrecy and integrity category sets, -- i.e., a pair of Labels. data DCLabel MkDCLabel :: Label -> Label -> DCLabel -- | Integrity category set. secrecy :: DCLabel -> Label -- | Secrecy category set. integrity :: DCLabel -> Label -- | 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 :: String -> Principal name :: Principal -> String -- | Generates a principal from an string. principal :: String -> Principal -- | 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 :: Label -> TCBPriv priv :: TCBPriv -> Label -- | 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 canflowto_p :: RelaxedLattice a => TCBPriv -> a -> a -> Bool -- | Privilege object corresponding to no privileges. noPriv :: TCBPriv -- | 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 -- | 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 -- | 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 -- | 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 canDelegate :: CanDelegate a b => a -> b -> Bool -- | 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 Principals in the Disj. This class is used to -- check ownership class Owns a owns :: Owns a => TCBPriv -> a -> Bool -- | 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 -- | Given two labels, perform an "or". Note that the new label is not -- necessarily in LNF. or_label :: Label -> Label -> Label -- | 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 -- | Determines if a label implies (in the logical sense) another label. In -- other words, d_1 ⋀ ... ⋀ d_n => d_1' ⋀ ... ⋀ d_n'. -- -- Properties: -- -- implies :: Label -> Label -> Bool -- | Class used to convert list of principals to a disjunction category and -- vice versa. class DisjToFromList a listToDisj :: DisjToFromList a => [a] -> Disj disjToList :: DisjToFromList a => Disj -> [a] -- | Given a list of categories, return a label. listToLabel :: [Disj] -> Label -- | Given a label return a list of categories. labelToList :: Label -> [Disj] instance Eq Principal instance Ord Principal instance Show Principal instance Read Principal instance Eq Disj instance Ord Disj instance Show Disj instance Read Disj instance Eq Conj instance Ord Conj instance Show Conj instance Read Conj instance Show Label instance Read Label instance Eq DCLabel instance Show DCLabel instance Read DCLabel instance Eq TCBPriv instance Show TCBPriv instance DisjToFromList String instance DisjToFromList Principal instance Owns Label instance Owns Disj instance CanDelegate TCBPriv TCBPriv instance CanDelegate TCBPriv Priv instance CanDelegate Priv TCBPriv instance CanDelegate Priv Priv instance Monoid TCBPriv instance RelaxedLattice DCLabel instance Lattice DCLabel instance ToLNF DCLabel instance ToLNF Label instance Eq Label -- | This module implements a `nano`, very simple, embedded domain -- specific language to create Labels and Privilages from -- conjunctions of principal disjunctions. -- -- A 'Label'/'Priv' is created using the (.\/.) and (./\.) -- operators. The disjunction operator (.\/.) is used to create a -- category from Principals, Strings, 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 Labels, 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 -- -- module DCLabel.NanoEDSL (.\/.) :: DisjunctionOf a b => a -> b -> Label (./\.) :: ConjunctionOf a b => a -> b -> Label -- | Empty label. (<>) :: Label -- | All label. (><) :: Label singleton :: Singleton a => a -> Label newDC :: NewDC a b => a -> b -> DCLabel -- | Class used to create Privs and TCBPrivs. class NewPriv a newPriv :: NewPriv a => a -> Priv newTCBPriv :: NewPriv a => TCBPriv -> a -> Maybe TCBPriv instance NewPriv String instance NewPriv Principal instance NewPriv Label instance NewDC String String instance NewDC Label String instance NewDC String Label instance NewDC Principal Principal instance NewDC Label Principal instance NewDC Principal Label instance NewDC Label Label instance ConjunctionOf Disj String instance ConjunctionOf String Disj instance ConjunctionOf Disj Principal instance ConjunctionOf Principal Disj instance ConjunctionOf Label Disj instance ConjunctionOf Disj Label instance ConjunctionOf Disj Disj instance ConjunctionOf Label String instance ConjunctionOf String Label instance ConjunctionOf String String instance ConjunctionOf Label Label instance ConjunctionOf Label Principal instance ConjunctionOf Principal Label instance ConjunctionOf Principal Principal instance DisjunctionOf Label String instance DisjunctionOf String Label instance DisjunctionOf String String instance DisjunctionOf Label Label instance DisjunctionOf Label Principal instance DisjunctionOf Principal Label instance DisjunctionOf Principal Principal instance Singleton String instance Singleton Principal -- | 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.Secrecy -- | A secrecy-only DC label. newtype SLabel MkSLabel :: DCLabel -> SLabel instance Eq SLabel instance Show SLabel instance Read SLabel instance RelaxedLattice SLabel instance Lattice SLabel instance ToLNF SLabel module DCLabel.Integrity -- | An integrity-only DC label. newtype ILabel MkILabel :: DCLabel -> ILabel instance Eq ILabel instance Show ILabel instance Read ILabel instance RelaxedLattice ILabel instance Lattice ILabel instance ToLNF ILabel -- | This module exports a function prettyShow that pretty prints -- Principals, Disjunctions, Conjunctions, -- Labels and DCLabels. module DCLabel.PrettyShow -- | Class used to create a Doc type of DCLabel-related types class PrettyShow a pShow :: PrettyShow a => a -> Doc -- | Render a PrettyShow type to a string. prettyShow :: PrettyShow a => a -> String instance PrettyShow ILabel instance PrettyShow SLabel instance PrettyShow TCBPriv instance PrettyShow Principal instance PrettyShow DCLabel instance PrettyShow Label instance PrettyShow Conj instance PrettyShow Disj -- | 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 join :: Lattice a => a -> a -> a meet :: Lattice a => a -> a -> a top :: Lattice a => a bottom :: Lattice a => a canflowto :: Lattice a => a -> a -> Bool -- | 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 :: Label MkLabel :: Conj -> Label label :: Label -> Conj -- | A DCLabel is a pair of secrecy and integrity category sets, -- i.e., a pair of Labels. data DCLabel MkDCLabel :: Label -> Label -> DCLabel -- | Integrity category set. secrecy :: DCLabel -> Label -- | Secrecy category set. integrity :: DCLabel -> Label -- | A category, i.e., disjunction, of Principals. The empty list -- '[]' corresponds to the disjunction of all principals. Conceptually, -- [] = [P_1 ⋁ P_2 ⋁ ...] newtype Disj MkDisj :: [Principal] -> Disj disj :: Disj -> [Principal] -- | 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 :: [Disj] -> Conj conj :: Conj -> [Disj] -- | 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. data Principal -- | Generates a principal from an string. principal :: String -> Principal name :: Principal -> String singleton :: Singleton a => a -> Label listToDisj :: DisjToFromList a => [a] -> Disj disjToList :: DisjToFromList a => Disj -> [a] -- | Given a list of categories, return a label. listToLabel :: [Disj] -> Label -- | Given a label return a list of categories. labelToList :: Label -> [Disj] (.\/.) :: DisjunctionOf a b => a -> b -> Label (./\.) :: ConjunctionOf a b => a -> b -> Label -- | Empty label. (<>) :: Label -- | All label. (><) :: Label newDC :: NewDC a b => a -> b -> DCLabel -- | 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 -- | Untrusted privileged object, which can be converted to a -- TCBPriv with delegatePriv. type Priv = Label -- | Relaxed partial-order relation canflowto_p :: RelaxedLattice a => TCBPriv -> a -> a -> Bool -- | 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 -- | Can use first privilege in place of second. canDelegate :: CanDelegate a b => a -> b -> Bool -- | Checks if category restriction can be bypassed given the privilege. owns :: Owns a => TCBPriv -> a -> Bool -- | Class used to create Privs and TCBPrivs. class NewPriv a newPriv :: NewPriv a => a -> Priv newTCBPriv :: NewPriv a => TCBPriv -> a -> Maybe TCBPriv -- | Privilege object corresponding to no privileges. noPriv :: TCBPriv