dclabel-eci11 (empty) → 0.1
raw patch · 10 files changed
+763/−0 lines, 10 filesdep +QuickCheckdep +basesetup-changed
Dependencies added: QuickCheck, base
Files
- DCLabel/Core.hs +342/−0
- DCLabel/Lattice.hs +10/−0
- DCLabel/QC_Core.hs +137/−0
- DCLabel/Trustworthy.hs +81/−0
- DCLabel/Untrustworthy.hs +47/−0
- Examples/Labels.hs +24/−0
- GNUmakefile +51/−0
- LICENSE +25/−0
- Setup.hs +3/−0
- dclabel-eci11.cabal +43/−0
+ DCLabel/Core.hs view
@@ -0,0 +1,342 @@+{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FunctionalDependencies #-}++module DCLabel.Core where++import Data.List (nub, sort, (\\))+import DCLabel.Lattice++-- | It represents principals in the labels. +newtype Principal = MkPrincipal { name :: String } deriving (Eq, Ord)++-- | It generates a principal from an string. +principal :: String -> Principal +principal = MkPrincipal++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)++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++-- | Data type to represent conjunctions+newtype Conj a = MkConj { conj :: [a] } deriving (Eq, Ord)+++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 ++instance (Ord a, Eq a) => Eq (Label a) 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) ] ++{-+ 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 +emptyLabel = MkLabel (MkConj [])++allLabel :: Label a+allLabel = MkLabelAll++-- ^ Predicate function that returns @True@ if the label corresponds to+-- the 'emptyLabel'.+isEmptyLabel :: Label a -> Bool+isEmptyLabel MkLabelAll = False+isEmptyLabel l = and [ null (disj d) | d <- conj (label l) ]++-- ^ Predicate function that retuns @True@ if the label corresponds to+-- the 'allLabel'.+isAllLabel :: Label a -> 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) ]++{-| + 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)) ] +++-- | 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 ] ++-- | 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 ]+++-- | 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 ++-- | It represents disjunction category labels+data DCLabel a = MkDCLabel { secrecy :: Label a+ , integrity :: Label a+ } deriving (Eq, Ord)+++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 are elements of a lattice+----------------------------------------++-- | 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+ , integrity = MkLabelAll }+ canflowto l1 l2 = let l1' = reduceDC l1+ l2' = reduceDC l2+ in ((secrecy l2') `implies` (secrecy l1')) &&+ ((integrity l1') `implies` (integrity l2'))+ join l1 l2 = let s3 = (secrecy l1) `and_label` (secrecy l2)+ i3 = (integrity l1) `or_label` (integrity l2)+ in reduceDC $ MkDCLabel s3 i3+ meet l1 l2 = let s3 = (secrecy l1) `or_label` (secrecy l2)+ i3 = (integrity l1) `and_label` (integrity l2)+ in reduceDC $ MkDCLabel s3 i3+ ++-- | 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 ] /\ [ ] /\ [ ]) -}++-- +++---+---+--- 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] ]++instance Singleton String Principal where + singleton s = MkLabel $ MkConj [ MkDisj [principal s] ]+++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++instance DisjunctionOf String String (Label Principal) where + s1 .\/. s2 = singleton s1 .\/. singleton s2++instance DisjunctionOf String (Label Principal) (Label Principal) where + s .\/. l = singleton s .\/. l ++instance DisjunctionOf (Label Principal) String (Label Principal) where + l .\/. p = p .\/. l +++-- | 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 +++(<>) = 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 ]++-- | It extracts the label corresponding to the secrecy component of a 'DCLabel'+secrecyDC :: DCLabel Principal -> Label Principal +secrecyDC dcl = secrecy dcl++-- | It extracts the label corresponding to the integrity component of a 'DCLabel'+integrityDC :: DCLabel Principal -> Label Principal +integrityDC dcl = integrity dcl++-- | It creates a 'DCLabel' based on two labels.+newDC l1 l2 = MkDCLabel l1 l2 ++-- | It checks if a privilege is owned+own :: Ord a => Priv a -> DCLabel a -> Bool +own p l = priv p `canflowto` l ++-- | It returns the privilege in the form of a label. +privToLabel :: Priv a -> DCLabel a +privToLabel = priv ++-- | It creates privileges. This functions must be used only by trustworthy code. +createPriv :: DCLabel a -> Priv a +createPriv = MkPriv +
+ DCLabel/Lattice.hs view
@@ -0,0 +1,10 @@+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 ++
+ DCLabel/QC_Core.hs view
@@ -0,0 +1,137 @@+{-# 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"}]}]}}}+++
+ DCLabel/Trustworthy.hs view
@@ -0,0 +1,81 @@+{-|++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+
+ DCLabel/Untrustworthy.hs view
@@ -0,0 +1,47 @@+{-|+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)+++++++++
+ Examples/Labels.hs view
@@ -0,0 +1,24 @@+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") +
+ GNUmakefile view
@@ -0,0 +1,51 @@++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 --
+ LICENSE view
@@ -0,0 +1,25 @@+Disjunction Category Labels +Copyright (C) 2011, Deian Stefan, Alejandro Russo, and David Mazieres+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:+ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+ * Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.+ * Neither the name of the <organization> nor the+ names of its contributors may be used to endorse or promote products+ derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,3 @@+import Distribution.Simple+main :: IO ()+main = defaultMain
+ dclabel-eci11.cabal view
@@ -0,0 +1,43 @@+Name: dclabel-eci11+Version: 0.1+build-type: Simple+License: BSD3+License-File: LICENSE+Copyright: (c) 2011 Deian Stefan, David Mazieres, Alejandro Russo+Author: Deain Stefan, David Mazieres, Alejandro Russo+Maintainer: Alejandro Russo < russo at chalmers dot se >+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.++Source-repository head+ Type: git+ Location: gitosis@csmisc17.cs.chalmers.se:dclabels-eci11++Library + Build-depends: base >= 4 && < 5, + QuickCheck >= 2.1++ ghc-options: ++ Exposed-modules:+ DCLabel.Untrustworthy, + DCLabel.Trustworthy ++ Other-modules:+ DCLabel.Lattice, + DCLabel.Core, + DCLabel.QC_Core + + Extensions:+ MultiParamTypeClasses,+ FlexibleInstances, + FlexibleContexts, + TypeSynonymInstances, + FunctionalDependencies