dclabel-eci11 0.1 → 0.2

raw patch · 15 files changed

+682/−645 lines, 15 filesdep +prettyPVP ok

version bump matches the API change (PVP)

Dependencies added: pretty

API changes (from Hackage documentation)

Files

• DCLabel/Core.hs +227/−272
• DCLabel/Integrity.hs +26/−0
• DCLabel/Lattice.hs +0/−10
• DCLabel/NanoEDSL.hs +138/−0
• DCLabel/PrettyShow.hs +38/−0
• DCLabel/QC_Core.hs +0/−137
• DCLabel/Safe.hs +35/−0
• DCLabel/Secrecy.hs +26/−0
• DCLabel/Trustworthy.hs +0/−81
• DCLabel/Untrustworthy.hs +0/−47
• Examples/Labels.hs +0/−24
• Examples/UsingEDSL.hs +33/−0
• GNUmakefile +0/−51
• Tests/Main.hs +148/−0
• dclabel-eci11.cabal +11/−23

@@ -1,342 +1,297 @@-{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+module DCLabel.Core ( -- * Constructors+                      Disj(..), Conj(..), Label(..)+                      -- * DC Labels+                    , Lattice(..), DCLabel(..)+                    , emptyLabel, allLabel+                      -- * Principals+                    , Principal(..), principal+                      -- * Priviliges+                    , TCBPriv(..), Priv+                    , RelaxedLattice(..)+                    , noPriv, rootPrivTCB+                    , delegatePriv, createPrivTCB+                    , CanActFor(..)+                      -- * Label/internal operations+                    , and_label, or_label, ToLNF(..), cleanLabel, implies+                    ) where -module DCLabel.Core where  import Data.List (nub, sort, (\\))-import DCLabel.Lattice+import Data.Maybe (fromJust) --- | It represents principals in the labels. -newtype Principal = MkPrincipal { name :: String } deriving (Eq, Ord)+--+-- Categories+-- --- | It generates a principal from an string. -principal :: String -> Principal -principal = MkPrincipal+-- | A disjunction of ordered elements.+-- The empty list '[]' corresponds to the disjunction of all principals.+-- In other words, conceptually, @[] =  [P_1 \/ P_2 \/ ...]@+newtype Disj = MkDisj { disj :: [Principal] }+        deriving (Eq, Ord, Show, Read) -instance Show Principal where-    show (MkPrincipal s) = show s -instance Read Principal where-    readsPrec d s = map (\(p, rest) -> (principal p, rest)) $ readsPrec d s---- | Data type to represent disjunctions. -newtype Disj a = MkDisj { disj :: [a] } deriving (Eq, Ord)+-- | A conjunction of ordered elements.+-- 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) -instance Show a => Show (Disj a) where-  show (MkDisj xs) = "[ " ++ showCat xs ++ " ]"-                     where showCat []     = ""-                           showCat [x]    = init $ tail $ show x -                           showCat (x:xs) = init (tail (show x)) ++ " \\/ " ++ showCat xs+--+-- Labels+-- --- | Data type to represent conjunctions-newtype Conj a = MkConj { conj :: [a] } deriving (Eq, Ord)+-- | (Bounded) Lattice definition +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  -instance Show a => Show (Conj a) where -  show (MkConj [])     = "None" -  show (MkConj [x])    = show x-  show (MkConj (x:xs))   = show x ++ " /\\ " ++ show (MkConj xs)  ---- | Data type to represent labels, i.e. conjunctions of disjunctions. -data  Label a =  MkLabelAll-               | MkLabel { label :: (Conj (Disj a)) } deriving (Ord)--instance Show a => Show (Label a) where -  show (MkLabelAll) = "All" -  show (MkLabel l)  = show l +-- | 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) -instance (Ord a, Eq a) => Eq (Label a) where+instance Eq Label where   (==) MkLabelAll MkLabelAll = True   (==) MkLabelAll _ = False   (==) _ MkLabelAll = False-  (==) l1 l2 = (label . reduceLabel $ l1) == (label . reduceLabel $ l2)---- | It takes two labels and makes the conjunction of them. -and_label :: Label a -> Label a -> Label a -and_label l1 l2   | isAllLabel l1 || isAllLabel l2 = MkLabelAll-                  | otherwise = MkLabel { label = MkConj $ conj (label l1)-                                                        ++ conj (label l2) }   ---{-| -It takes two labels and distributes the disjunction. For example, -->>> singleton "Alice" `or_label` ( "Bob" ./\. "Carla" )-[ Alice \/ Bob ] /\ [ Alice \/ Carla ]---}-or_label :: Ord a => Label a -> Label a -> Label a -or_label l1 l2 | isEmptyLabel l2 || isEmptyLabel l1 = 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) ] +  (==) l1 l2 = (label . toLNF $ l1) == (label . toLNF $ l2) -{--               where l1' = nubLabel l1   -- We need to remove the empty lists, otherwise it won't work: -                     l2' = nubLabel l2   -- I = [A] /\ [] /\ []   I = [B] .. the or_label would be -                                         -- I = [A \/ B] /\ [B] /\ [B], and then it reduces to [B]!--}-               --- | A label without any disjunctions or conjunctions.-emptyLabel :: Label a +-- | 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 \/ ...]}>@+emptyLabel :: Label emptyLabel = MkLabel (MkConj []) -allLabel :: Label a+-- | 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] /\ ...}>@+allLabel :: Label allLabel = MkLabelAll --- ^ Predicate function that returns @True@ if the label corresponds to+-- | Predicate function that returns @True@ if the label corresponds to -- the 'emptyLabel'.-isEmptyLabel :: Label a -> Bool+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+-- | Predicate function that retuns @True@ if the label corresponds to -- the 'allLabel'.-isAllLabel :: Label a -> Bool+isAllLabel :: Label -> Bool isAllLabel MkLabelAll = True isAllLabel _ = False  -{-| -   It 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.--} -impliesDisj :: Ord a => Label a -> Disj a -> Bool -impliesDisj l1 d | isAllLabel l1 = True   -- Asserts 1-                 | otherwise = or [ and [ e `elem` (disj d) | e <- disj d1 ]-                                  | d1 <- conj (label l1) ]+--+-- Helper functions+-- -{-| -   It determines if a label implies (in the logical sense) another label. -   In other words, d1 /\ ... /\ dn => d1' /\ ... /\ dn'.--}-implies :: Ord a => Label a -> Label a -> Bool -implies l1 l2   | isAllLabel l1 = True -- Asserts 1-                | isAllLabel l2 = False-                | otherwise = and [ impliesDisj l1 d | d <- conj (label (reduceLabel l2)) ]  +-- | 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)} --- | It removes extraneous disjunctions from a given label.-reduceLabel :: Ord a => Label a -> Label a -reduceLabel l@(MkLabelAll) = l -reduceLabel l = (MkLabel . MkConj) $-                conj (label l') \\ extraneous -                where l' = nubLabel l-                      extraneous = [ d2 | d1 <- conj (label l'), d2 <- conj (label l'), d1 /= d2, -                                     impliesDisj ((MkLabel . MkConj) [d1]) d2 ] +-- | 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]  --- | It removes repeated principals from a given label.-nubLabel :: Ord a => Label a -> Label a  -nubLabel l@(MkLabelAll) = l-nubLabel l@(MkLabel _)  = MkLabel $ -                             MkConj $ (sort.nub) [ MkDisj ( (sort.nub) (disj c) ) | c <- conj (label l), -                                                                                    not. null $ disj c ]+-- | 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.+--+-- Properties: 1. forall X, ALL `impliesDisj` X := True+--             2. forall X, X `impliesDisj` []  := True+--             3. forall X/=[],  [] `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, d1 /\ ... /\ dn => d1' /\ ... /\ dn'.+--+-- 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+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 ] --- | It represents privilege.-data Priv a = MkPriv { priv :: DCLabel a } deriving Eq -instance Show a => Show (Priv a) where -  show (MkPriv l) = "Privilege: " ++ show l  +-- | 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 LNF.+-- It is used to overload the reduce function used by the 'Label', 'SLabel',+-- 'ILabel', and 'DCLabel'.+class ToLNF a where+  toLNF :: a -> a --- | It represents disjunction category labels-data DCLabel a = MkDCLabel { secrecy   :: Label a-                           , integrity :: Label a-                           } deriving (Eq, Ord)+-- | 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+-- -instance Show a => Show (DCLabel a) where -     show dclabel = "S=" ++ show (secrecy dclabel) ++ " I=" ++ show (integrity dclabel) --- | It computes the canonical form of a 'DCLabel'.-reduceDC :: Ord a => DCLabel a -> DCLabel a-reduceDC l = let s = reduceLabel . secrecy $ l-                 i = reduceLabel . integrity $ l-             in MkDCLabel { secrecy = s, integrity = i }+--+-- DC Labels : (Secrecy, Integrity)+-- ---------------------------------------------- DC Labels are elements of a lattice-----------------------------------------+-- | A DC label for secrecy and integrity.+data DCLabel = MkDCLabel { secrecy :: Label+                         , integrity :: Label } +  deriving (Eq, Show, Read) --- | It defines that 'DCLabel' are elements of a lattice.-instance Ord a => Lattice (DCLabel a) where-  top = MkDCLabel { secrecy = MkLabelAll-                  , integrity = emptyLabel }-  bottom = MkDCLabel { secrecy = emptyLabel+instance ToLNF DCLabel where+  toLNF l = MkDCLabel { secrecy = toLNF (secrecy l)+                      , integrity = toLNF (integrity l)}++instance Lattice DCLabel where+  bottom = MkDCLabel { secrecy = MkLabel $ MkConj []                      , integrity = MkLabelAll }-  canflowto l1 l2 = let l1' = reduceDC l1-                        l2' = reduceDC l2-                    in ((secrecy l2') `implies` (secrecy l1')) &&-                       ((integrity l1') `implies` (integrity l2'))+  top = MkDCLabel { secrecy = MkLabelAll+                  , integrity = MkLabel $ MkConj [] }   join l1 l2 = let s3 = (secrecy l1) `and_label` (secrecy l2)                    i3 = (integrity l1) `or_label` (integrity l2)-               in reduceDC $ MkDCLabel s3 i3+               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 reduceDC $ MkDCLabel s3 i3-  +               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')) --- | It checks if a 'DCLabel' can flow to another 'DCLabel' given some privilege. -canflowto_p :: Lattice (DCLabel a) => Priv a -> DCLabel a -> DCLabel a -> Bool-canflowto_p p dcl1 dcl2 = let dcl2' = newDC (and_label ( secrecy (priv p) ) (secrecy dcl2))-                                            (integrity dcl2)-                              dcl1' = newDC (secrecy dcl1) -                                            (and_label ( integrity (priv p) ) (integrity dcl1)) -                          in canflowto dcl1' dcl2'   -----Tests-----a = MkDisj { disj = ["A"] } --aorb = MkDisj { disj = ["A", "B"] } -cord = MkDisj { disj = ["C", "D"] } -eorf = MkDisj { disj = ["E", "F"] } -gorh = MkDisj { disj = ["G", "H"] } --aorborc = MkDisj { disj = ["A", "B", "C", "A"] } --conjaorb = MkLabel $ MkConj { conj = [aorb] }---conjaorborc = MkLabel $ MkConj { conj = [aorborc, aorborc, aorb] }--t1 = impliesDisj conjaorborc aorb -- False-t2 = impliesDisj conjaorb aorborc -- True --t3 = implies conjaorb conjaorborc -- True -t4 = implies conjaorborc conjaorb -- False--aorbANDcord = MkLabel $ MkConj { conj = [aorb,cord] }-eorfANDgorh = MkLabel $ MkConj { conj = [eorf,gorh] }--t5 = aorbANDcord `or_label` eorfANDgorh ------{- (S=[ A ] /\ [ C \/ C ] /\ [  ] I=[ A ] /\ [ A \/ A ] /\ [  ],S=[ A ] /\ [  ] I=[ B ] /\ [  ] /\ [  ]) -}-+-- Principals --  ------------- Small DSL for working with labels. It is a simplified version of what David did------------ | Class that allows the creation of label which are just singletons.-class Singleton a b | a -> b where -      -- | It creates a singleton label, i.e. a label with only one principal.-      singleton :: a -> Label b --instance Singleton Principal Principal where -      singleton p = MkLabel $ MkConj [ MkDisj [p] ]+-- | Principal is a simple string.+newtype Principal = MkPrincipal { name :: String }+                  deriving (Eq, Ord, Show, Read) -instance Singleton String Principal where -      singleton s = MkLabel $ MkConj [ MkDisj [principal s] ]+-- | Generates a principal from an string. +principal :: String -> Principal +principal = MkPrincipal  -infixl 7 .\/.-infixl 6 ./\.---- | Class used to create disjunctions-class DisjunctionOf a b c | a b -> c  where-  (.\/.) :: a -> b -> c--instance DisjunctionOf Principal Principal (Label Principal) where - p1 .\/. p2 = MkLabel $ MkConj [ MkDisj [p1,p2] ]--instance DisjunctionOf Principal (Label Principal) (Label Principal) where - p .\/. l = (singleton p) `or_label` l --instance DisjunctionOf (Label Principal) Principal (Label Principal) where - l .\/. p = p .\/. l--instance DisjunctionOf (Label Principal) (Label Principal) (Label Principal) where - l1 .\/. l2 = l1 `or_label` l2+--+-- Priviliges+--  -instance DisjunctionOf String String (Label Principal) where - s1 .\/. s2 = singleton s1 .\/. singleton s2+-- | 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) -instance DisjunctionOf String (Label Principal) (Label Principal) where -  s .\/. l = singleton s .\/. l +-- | Untrusted privileged object, which can be converted to a 'TCBPriv' with+-- 'delegatePriv'.+type Priv = Label -instance DisjunctionOf (Label Principal) String (Label Principal) where -  l .\/. p = p .\/. l  +-- | 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  --- | Class used to create conjunctions-class ConjunctionOf a b c | a b -> c where-   (./\.) :: a -> b -> c--instance ConjunctionOf Principal Principal (Label Principal) where-   p1 ./\. p2 = MkLabel $ MkConj [ MkDisj [p1], MkDisj [p2] ] --instance ConjunctionOf Principal (Label Principal) (Label Principal) where-   p ./\. l = singleton p `and_label` l --instance ConjunctionOf (Label Principal) Principal (Label Principal) where-   l ./\. p = p ./\. l --instance ConjunctionOf (Label Principal) (Label Principal) (Label Principal) where-   l1 ./\. l2 = l1 `and_label` l2 ---- | Instances usng strings and not principals-instance ConjunctionOf String String (Label Principal) where-   s1 ./\. s2 = singleton s1 ./\. singleton s2 --instance ConjunctionOf String (Label Principal) (Label Principal) where-   s ./\. l = singleton s `and_label` l --instance ConjunctionOf (Label Principal) String (Label Principal) where-   l ./\. s = s ./\. l +instance RelaxedLattice DCLabel where+  canflowto_p p l1 l2 =+    let l1' =  MkDCLabel { secrecy = (secrecy l2)+                         , integrity = (and_label (priv p) (integrity l2)) }+        l2' =  MkDCLabel { secrecy = (and_label (priv p) (secrecy l2))+                         , integrity = (integrity l2) }+    in canflowto l1' l2'   -(<>) = emptyLabel------------- Generic API------------ | It checks that a principal appears in a label. -isPrincipal :: Principal -> Label Principal -> Bool-isPrincipal p l =  or [ name p `elem` ps' | ps <- labelToList l, let ps' = map name ps ]---- | It converts a label into a list. -labelToList :: Label Principal -> [ [Principal] ]-labelToList (MkLabel l) = [ [ d | d <- disj c ]  | c <- conj l ]+-- | Given trusted privilige and a \"desired\" untrusted privilege,+-- return a trusted version of the untrusted privilige, if the+-- provided (trusted) privilige 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 --- | It extracts the label corresponding to the secrecy component of a 'DCLabel'-secrecyDC :: DCLabel Principal -> Label Principal -secrecyDC dcl = secrecy dcl+-- | Privilege object corresponding to no privileges.+noPriv :: TCBPriv+noPriv = MkTCBPriv { priv = emptyLabel } --- | It extracts the label corresponding to the integrity component of a 'DCLabel'-integrityDC :: DCLabel Principal -> Label Principal -integrityDC dcl = integrity dcl+-- | Privilege object corresponding to the \"root\", or all privileges.+-- Any other privilige may be delegated using this privilege object and it must+-- therefore not be exported to untrusted code. +rootPrivTCB :: TCBPriv+rootPrivTCB = MkTCBPriv { priv = allLabel } --- | It creates a 'DCLabel' based on two labels.-newDC l1 l2 = MkDCLabel l1 l2 +-- | 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)+  		+-- | 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 --- | It checks if a privilege is owned-own :: Ord a => Priv a -> DCLabel a -> Bool -own p l = priv p `canflowto` l +instance CanActFor Priv Priv where+  canActFor p1 p2 = p1 `implies` p2 --- | It returns the privilege in the form of a label. -privToLabel :: Priv a -> DCLabel a -privToLabel = priv +instance CanActFor Priv TCBPriv where+  canActFor p1 p2 = p1 `implies` (priv p2) --- | It creates privileges. This functions must be used only by trustworthy code. -createPriv :: DCLabel a -> Priv a -createPriv = MkPriv +instance CanActFor TCBPriv Priv where+  canActFor p1 p2 = (priv p1) `implies` p2 +instance CanActFor TCBPriv TCBPriv where+  canActFor p1 p2 = (priv p1) `implies` (priv p2)

@@ -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 }

@@ -1,10 +0,0 @@-module DCLabel.Lattice where-  -class Ord a => Lattice a where -  top :: a -  bottom :: a -  canflowto :: a -> a -> Bool-  join :: a -> a -> a -  meet :: a -> a -> a --

@@ -0,0 +1,138 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+module DCLabel.NanoEDSL ( -- * Operators+			  (.\/.), (./\.)+                        , (<>), (><)+                          -- * DCLabel creation+                        , newDC+                          -- * Privilege object creation+                        , 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++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 ++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 usng 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 +++-- | 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 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

@@ -0,0 +1,38 @@+module DCLabel.PrettyShow (PrettyShow(..), prettyShow) where++import DCLabel.Core+import Text.PrettyPrint++++-- ^ Class used to create a 'Doc' type of DCLabel-related types+class PrettyShow a where+	pShow :: a -> 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)

@@ -1,137 +0,0 @@-{-# LANGUAGE FlexibleInstances #-}-module DCLabel.QC_Core where---import Test.QuickCheck hiding (label) -import Control.Monad (liftM)-import DCLabel.Core-import DCLabel.Lattice -import Data.List--instance Arbitrary Principal where -     arbitrary = do p <- oneof $ map return ["A", "B", "C"]-                    return $ principal p---instance Arbitrary a => Arbitrary (Disj a) 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)     -     shrink (MkDisj ls) = [MkDisj l | l <- tails ls]---instance Arbitrary a => Arbitrary (Conj (Disj a)) 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 a => Arbitrary (Label a) where-  arbitrary = mkArbLbl arbitrary-    where mkArbLbl :: Gen (Conj (Disj a)) -> Gen (Label a)-          mkArbLbl = liftM MkLabel-          -instance Arbitrary a => Arbitrary (DCLabel a) where-  arbitrary = do s <- arbitrary-                 i <- arbitrary -                 return $ MkDCLabel { secrecy = s, integrity = i }----- nubLabel does not modify the semantics of the label -prop_nubLabel :: Ord a => Label a -> Bool-prop_nubLabel l = let l' = nubLabel l -                  in l `implies` l' && l' `implies` l----  Reduce does not modify the semantics of the label---  Ale: I will keep the original label as it is, without nubLabel.-prop_reduce :: Ord a => Label a -> Bool-prop_reduce l = let l' = reduceLabel l -                in  l `implies` l' && l' `implies` l ---                   let l1 = nubLabel ul1---                       l2  = reduceLabel l1---                   in l1 `implies` l2 && l2 `implies` l1--prop_reduce_idem :: Ord a => Label a -> Bool -prop_reduce_idem l = let l'  = reduceLabel l -                         l'' = reduceLabel l' -                     in l' == l''---- Partial order for DCLabels-prop_dc_porder :: Ord a => (DCLabel a, DCLabel a) -> Bool-prop_dc_porder (l1,l2) = let l1' = reduceDC l1-                             l2' = reduceDC 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 :: Ord a => (DCLabel a, DCLabel a) -> 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--- Ale: we need to fix this since it is difficult to satisfy the hypothesis. Need to think about it.-prop_dc_join_lub :: (Ord a, Show a, Arbitrary a)-                 => (DCLabel a, DCLabel a) -> Property-prop_dc_join_lub (l1,l2) = forAll (gen l1) $ \l3' ->- (l1 `canflowto` l3') && (l2 `canflowto` l3') ==> (l1 `join` l2) `canflowto` l3'-    where gen :: Arbitrary a => DCLabel a -> Gen (DCLabel a)-          gen _ = arbitrary-                  ---- Check that meet flows to the labels making it, for DCLabels-prop_dc_meet :: Ord a => (DCLabel a, DCLabel a) -> 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 :: (Ord a, Show a, Arbitrary a)-                 => (DCLabel a, DCLabel a) -> Property-prop_dc_meet_glb (l1,l2) = forAll (gen l1) $ \l3' ->- (l3' `canflowto` l1) && (l3' `canflowto` l2) ==> l3' `canflowto` (l1 `meet` l2)-    where gen :: Arbitrary a => DCLabel a -> Gen (DCLabel a)-          gen _ = arbitrary---type DCLabelPair a = (DCLabel a, DCLabel a)-checks n = do -  let args = stdArgs { maxSuccess = n, maxSize = n, maxDiscard = 10000}-  putStrLn "Checking function nubLabel..."-  quickCheckWith args (prop_nubLabel :: Label Principal -> Bool)-  putStrLn "Checking function reduce..."-  quickCheckWith args (prop_reduce :: Label Principal -> Bool)-  putStrLn "Checking idempotence of function reduce..."-  quickCheckWith args (prop_reduce_idem :: Label Principal -> Bool)-  putStrLn "Checking the join operation..."-  quickCheckWith args (prop_DC_join ::  DCLabelPair Principal -> Bool)-  putStrLn "Checking the join operation is indeed the least upper bound..."-  quickCheckWith args (prop_dc_join_lub :: DCLabelPair Principal -> Property)-  putStrLn "Checking the meet operation..."-  quickCheckWith args (prop_dc_meet :: DCLabelPair Principal -> Bool)-  putStrLn "Checking the meet operation is indeed the greatest lower bound..."-  quickCheckWith args (prop_dc_meet_glb :: DCLabelPair Principal -> Property)-  putStrLn "Checking DC labels form a partial order..."-  quickCheckWith args (prop_dc_porder :: DCLabelPair Principal -> Bool)---l1 = MkDCLabel {secrecy = MkLabel {label = MkConj {conj = [MkDisj {disj = [MkPrincipal {name = "B"}]},MkDisj {disj = []},MkDisj {disj = []}]}}, integrity = MkLabel {label = MkConj {conj = [MkDisj {disj = [MkPrincipal {name = "A"}]},MkDisj {disj = []},MkDisj {disj = []}]}}}-l2 = MkDCLabel {secrecy = MkLabel {label = MkConj {conj = [MkDisj {disj = [MkPrincipal {name = "C"}]},MkDisj {disj = []}]}}, integrity = MkLabel {label = MkConj {conj = [MkDisj {disj = [MkPrincipal {name = "B"}]}]}}}---

@@ -0,0 +1,35 @@+{-|+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+                    , (.\/.), (./\.)+                    , (<>), (><)+                    , newDC+                      -- * Priviligies +                    , TCBPriv, Priv+                    , canflowto_p+                    , delegatePriv+                    , canActFor+                    , newPriv, newTCBPriv+                    ) where++import DCLabel.Core+import DCLabel.NanoEDSL+++++++++

@@ -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 }

@@ -1,81 +0,0 @@-{-|--This module implements Disjunction Category labels.--A label consists on conjunctions of disjunctions of -principals. Labels can be simply created by using the -function 'singleton' (it creates a label with only one -principal). Functions '(.\\\/.)' and '(.\/\\.)' create disjunction -and conjunction of principals, respectively. To illustrate-the use of this functions, we have the following examples. -->>> singleton "Alice"-[ Alice ]-->>> "Alice" .\/. "Bob"-[ Alice \/ Bob ]-->>> "Alice" .\/. ("Bob" ./\. "Carla")-[ Alice \/ Bob ] /\ [ Alice \/ Carla ]--A 'DCLabel' is simple two labels, one for confidentiality ('secrecy') -and another one for integrity ('integrity'). DCLabels are created by -function 'newDC', where the first argument is for secrecy and the second-one for integrity. -->>> newDC (singleton "Alice") ("Bob" .\/. "Alice") -S=[ Alice ] I=[ Bob \/ Alice ]--Given two 'DCLabel' it is possible to precisely compute the join -and the meet by calling functions 'join' and 'meet', respectively. -->>> join ( newDC (singleton "Alice") (singleton "Carla") ) (  newDC (singleton "Bob") (emptyLabel) ) -S=[ Alice ] /\ [ Bob ] I=True-->>> meet ( newDC (singleton "Alice") (singleton "Bob") ) (  newDC (singleton "Carla") (singleton "Carla") )-S=[ Alice \/ Carla ] I=[ Bob ] /\ [ Carla ]--It is possible to compare if a 'DCLabel' is more restrictive than another one by-calling the function 'canflowto'. For instance,-->>> canflowto ( newDC (singleton "Bob") (emptyLabel) ) (newDC ("Alice" ./\. "Bob") (singleton "Carla"))-False-->>> canflowto ( newDC (singleton "Bob") (singleton "Carla") ) (newDC ("Alice" ./\. "Bob") (emptyLabel))-True---}--module DCLabel.Trustworthy --       ( -- Lattice-           Lattice (join, meet, top, bottom, canflowto)-         -- Label -         , Label () -         , Principal ()-         , principal-         , isPrincipal-         , labelToList-         -- DSL -         , DisjunctionOf ( (.\/.) )  -         , ConjunctionOf ( (./\.) )-         , (<>)-         , singleton-         -- DC Label -         , DCLabel()-         , integrityDC -         , secrecyDC -         , newDC-         -- Priviligies -         , Priv() -         , canflowto_p-         , own -         , privToLabel-         , createPriv   -- Becareful where it is used-       )--where--import DCLabel.Lattice-import DCLabel.Core-

@@ -1,47 +0,0 @@-{-|-This module implements Disjunction Category labels. -It is designed to be used by untrustworthy code. -Technically, the module exports the same interface as -"DCLabel.Trustworthy" except for the function -'createPriv'. --}---module DCLabel.Untrustworthy -       ( -- Lattice-           Lattice (join, meet, top, bottom, canflowto)-         -- Label -         , Label () -         , Principal () -         , principal-         , isPrincipal-         , labelToList-         -- DSL -         , DisjunctionOf ( (.\/.) )  -         , ConjunctionOf ( (./\.) )-         , (<>)-         , singleton-         -- DC Label -         , DCLabel()-         , integrityDC -         , secrecyDC -         , newDC-         -- Priviligies -         , Priv() -         , canflowto_p-         , own -         , privToLabel-       )-         -where--import DCLabel.Trustworthy hiding (createPriv)---------

@@ -1,24 +0,0 @@-module Labels where --import DCLabel.Untrustworthy ---- Creating categories-c1 = singleton "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 (singleton "Deain") (singleton "Alice") -

@@ -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+  

@@ -1,51 +0,0 @@--PKG = $(basename $(wildcard *.cabal))-HSCS := $(patsubst %.hsc,%.hs,$(shell find . -name '*.hsc' -print))-HSCCLEAN = $(patsubst %.hs,%_hsc.[ch],$(HSCS))--all: $(HSCS)--.PHONY: all clean build dist doc browse install hsc--GHC = ghc $(WALL)-WALL = -Wall -Werror-LIBS = -lz--Setup: Setup.hs-	$(GHC) --make Setup.hs--dist/setup-config: Setup $(PKG).cabal-	./Setup configure --user--build: dist/setup-config-	./Setup build--doc: dist/setup-config-	./Setup haddock --hyperlink-source--dist: dist/setup-config-	./Setup sdist--INDEXDOC = cd $(HOME)/.cabal/share/doc \-    && find . -name '*.haddock' -print \-	| sed -e 's/\.\/\(.*\)\/[^\/]*\.haddock/--read-interface=\1,&/' \-	| xargs -t haddock --gen-contents --gen-index --odir=.--install: build doc-	./Setup install-	$(INDEXDOC)--uninstall: dist/setup-config-	./Setup unregister --user-	rm -rf $(HOME)/.cabal/lib/$(PKG)-[0-9]*-	rm -rf $(HOME)/.cabal/share/doc/$(PKG)-[0-9]*-	$(INDEXDOC)--browse: doc-	xdg-open dist/doc/html/$(PKG)/index.html--clean:-	rm -rf dist-	rm -f Setup $(HSCS) $(HSCCLEAN)-	find . \( -name '*~' -o -name '*.hi' -o -name '*.o' \) -print0 \-		| xargs -0 rm -f --

@@ -0,0 +1,148 @@+module Main (main) where++import Test.QuickCheck hiding (label) +import Control.Monad (liftM)+import DCLabel.Core+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 }+++-- 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++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)+++

@@ -1,43 +1,31 @@ Name:           dclabel-eci11-Version:        0.1+Version:        0.2 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 >+Maintainer:     Alejandro Russo < russo at chalmers dot se >, Deian Stefan  <deian at cs dot stanford dot edu> Stability:      experimental Synopsis:       Dynamic labels to assign confidentiality and integrity levels in scenarios of mutual distrust  Category:       Security Cabal-Version:  >=1.6  Extra-source-files:-     Examples/Labels.hs, GNUmakefile--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) <http://www.dc.uba.ar/events/eci/2011/index_html>. Please, refer to the official release of dclabels if you plan to use it for other purposes.+     Examples/UsingEDSL.hs,+     Tests/Main.hs -Source-repository head-  Type:     git-  Location: gitosis@csmisc17.cs.chalmers.se:dclabels-eci11+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) <http://www.dc.uba.ar/events/eci/2011/index_html>. Please, refer to the official release of dclabels if you plan to use it for other purposes.  Library     Build-depends: base >= 4 && < 5, +                  pretty > 1.0.1 && < 2,                   QuickCheck >= 2.1 -   ghc-options:  -    Exposed-modules:-       DCLabel.Untrustworthy, -       DCLabel.Trustworthy --   Other-modules:-       DCLabel.Lattice,  +       DCLabel.Safe,        DCLabel.Core, -       DCLabel.QC_Core - -   Extensions:-       MultiParamTypeClasses,-       FlexibleInstances, -       FlexibleContexts, -       TypeSynonymInstances,  -       FunctionalDependencies +       DCLabel.NanoEDSL,+       DCLabel.PrettyShow,+       DCLabel.Secrecy,+       DCLabel.Integrity