-- 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.4 -- | This module implements Disjunction Category Labels. -- -- A DCLabel is a pair of secrecy and integrity category -- sets or components, of type Component. Each component is simply -- a set of clauses in propositional logic (without negation). A -- component can either correspond to the term MkComponentAll, -- representing falsehood, or a set of categories (clauses): (of type -- Conj) corresponding to the conjunction of ategories (of type -- Disj). Each category, in turn, is a disjunction of -- Principals, where a Principal is just a -- ByteString 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 ⋁ ...]} Logically '[]' -- = True. newtype Conj MkConj :: [Disj] -> Conj conj :: Conj -> [Disj] -- | A components is a conjunction of disjunctions, where -- MkComponentAll is the constructor that is associated with the -- logical False. data Component MkComponentAll :: Component MkComponent :: Conj -> Component component :: Component -> Conj -- | A component without any disjunctions or conjunctions. This component, -- conceptually corresponds to the label consisting of a single category -- containing all principals. Conceptually (in a closed-world system), -- emptyComponent = <{[P_1 ⋁ P_2 ⋁ ...]}>. Logically, of -- course, this is equivalent to True. emptyComponent :: Component -- | The dual of emptyComponent, allComponent consists of the -- conjunction of all possible disjunctions, i.e., it is the label that -- implies all other labels. Conceptually (in a closed-world system), -- allComponent = <{[P_1] ⋀ [P_2] ⋀ ...}> Logically, of -- course, this is equivalent to False. allComponent :: Component -- | Labels form 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 and components to unique label normal form -- (LNF), which corresponds to conjunctive normal form of principals. We -- use this class to overload the reduce function used by the -- Component, DCLabel, etc. class ToLNF a toLNF :: ToLNF a => a -> a -- | A DCLabel is a pair of secrecy and integrity category sets, -- i.e., a pair of Components. data DCLabel MkDCLabel :: Component -> Component -> DCLabel -- | Integrity category set. secrecy :: DCLabel -> Component -- | Secrecy category set. integrity :: DCLabel -> Component -- | Principal is a simple string representing a source of authority. Any -- piece of code can create principals, regarless of how untrusted it is. -- However, for principals to be used in integrity components or be -- ignoerd a corresponding privilege (TCBPriv) must be created (by -- trusted code) or delegated. newtype Principal MkPrincipal :: ByteString -> Principal name :: Principal -> ByteString -- | Generates a principal from an string. principal :: ByteString -> Principal -- | Privilege object is just a conjunction of disjunctions, i.e., -- Component. A trusted privileged object must be introduced by -- trusted code, after which trusted privileged objects can be created by -- delegation. data TCBPriv MkTCBPriv :: Component -> TCBPriv priv :: TCBPriv -> Component -- | Untrusted privileged object, which can be converted to a -- TCBPriv with delegatePriv. type Priv = Component -- | Class extending Lattice, by allowing for the more relaxed label -- comparison canflowto_p. class Lattice a => RelaxedLattice a 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 components, take the union of the disjunctions, i.e., simply -- perform an "and". Note the new component is not necessarily in LNF. and_component :: Component -> Component -> Component -- | Given two components, perform an "or". Note that the new component is -- not necessarily in LNF. or_component :: Component -> Component -> Component -- | Removes any duplicate principals from categories, and any duplicate -- categories from the component. To return a clean component, it sorts -- the component and removes empty disjunctions. cleanComponent :: Component -> Component -- | Determines if a component logically implies another component. In -- other words, d_1 ⋀ ... ⋀ d_n => d_1' ⋀ ... ⋀ d_n'. -- -- Properties: -- -- implies :: Component -> Component -> 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 component. listToComponent :: [Disj] -> Component -- | Given a component return a list of categories. componentToList :: Component -> [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 Component instance Read Component instance Eq DCLabel instance Show DCLabel instance Read DCLabel instance Eq TCBPriv instance Show TCBPriv instance Serialize DCLabel instance Serialize Component instance Serialize Conj instance Serialize Disj instance Serialize Principal instance DisjToFromList ByteString instance DisjToFromList String instance DisjToFromList Principal instance Owns Component 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 Component instance Eq Component -- | This module implements a `nano`, very simple, embedded domain -- specific language to create Components and Privilages -- from conjunctions of principal disjunctions. -- -- A 'Component'/'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 Components, 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 -> Component (./\.) :: ConjunctionOf a b => a -> b -> Component -- | Empty component (logically this is True). (<>) :: Component -- | All component (logically this is False). (><) :: Component singleton :: Singleton a => a -> Component 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 Component instance NewDC String String instance NewDC Component String instance NewDC String Component instance NewDC Principal Principal instance NewDC Component Principal instance NewDC Principal Component instance NewDC Component Component instance ConjunctionOf Disj String instance ConjunctionOf String Disj instance ConjunctionOf Disj Principal instance ConjunctionOf Principal Disj instance ConjunctionOf Component Disj instance ConjunctionOf Disj Component instance ConjunctionOf Disj Disj instance ConjunctionOf Component String instance ConjunctionOf String Component instance ConjunctionOf String String instance ConjunctionOf Component Component instance ConjunctionOf Component Principal instance ConjunctionOf Principal Component instance ConjunctionOf Principal Principal instance DisjunctionOf Component String instance DisjunctionOf String Component instance DisjunctionOf String String instance DisjunctionOf Component Component instance DisjunctionOf Component Principal instance DisjunctionOf Principal Component instance DisjunctionOf Principal Principal instance Singleton ByteString 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 -- | This module implements secrecy-only DC Labels. 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 -- | This module implements integrity-only DC Labels. 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, -- Components 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 Component instance PrettyShow Conj instance PrettyShow Disj -- | This module exports a safe-subset of DCLabel.Core, implementing -- Disjunction Category Components. The exported functions and -- constructors may be used by untrusted code, guaranteeing that they -- cannot perform anything unsafe. module DCLabel.Safe 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 components is a conjunction of disjunctions, where -- MkComponentAll is the constructor that is associated with the -- logical False. data Component MkComponentAll :: Component MkComponent :: Conj -> Component component :: Component -> Conj -- | A DCLabel is a pair of secrecy and integrity category sets, -- i.e., a pair of Components. data DCLabel MkDCLabel :: Component -> Component -> DCLabel -- | Integrity category set. secrecy :: DCLabel -> Component -- | Secrecy category set. integrity :: DCLabel -> Component -- | 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 ⋁ ...]} Logically '[]' -- = True. 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 components or be -- ignoerd a corresponding privilege (TCBPriv) must be created (by -- trusted code) or delegated. data Principal -- | Generates a principal from an string. principal :: ByteString -> Principal name :: Principal -> ByteString singleton :: Singleton a => a -> Component listToDisj :: DisjToFromList a => [a] -> Disj disjToList :: DisjToFromList a => Disj -> [a] -- | Given a list of categories, return a component. listToComponent :: [Disj] -> Component -- | Given a component return a list of categories. componentToList :: Component -> [Disj] (.\/.) :: DisjunctionOf a b => a -> b -> Component (./\.) :: ConjunctionOf a b => a -> b -> Component -- | Empty component (logically this is True). (<>) :: Component -- | All component (logically this is False). (><) :: Component newDC :: NewDC a b => a -> b -> DCLabel -- | Privilege object is just a conjunction of disjunctions, i.e., -- Component. A trusted privileged object must be introduced by -- trusted code, after which trusted privileged objects can be created by -- delegation. data TCBPriv -- | Untrusted privileged object, which can be converted to a -- TCBPriv with delegatePriv. type Priv = Component -- | 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