diff --git a/DCLabel/Core.hs b/DCLabel/Core.hs --- a/DCLabel/Core.hs +++ b/DCLabel/Core.hs @@ -1,3 +1,7 @@ +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} + {-| This module implements Disjunction Category labels. @@ -48,9 +52,6 @@ -} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} module DCLabel.Core ( -- * Labels -- $labels Disj(..), Conj(..), Label(..) @@ -228,7 +229,7 @@ implies :: Label -> Label -> Bool implies l1 l2 | isAllLabel l1 = True -- Asserts 1 | isAllLabel l2 = False -- Asserts 2 - | otherwise = and [ impliesDisj l1 d + | otherwise = and [ impliesDisj (toLNF l1) d | d <- conj . label . toLNF $ l2 ] diff --git a/DCLabel/Integrity.hs b/DCLabel/Integrity.hs --- a/DCLabel/Integrity.hs +++ b/DCLabel/Integrity.hs @@ -1,3 +1,9 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +{-# LANGUAGE Trustworthy #-} +#else +#warning "This module is not using SafeHaskell" +#endif {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} module DCLabel.Integrity ( ILabel(..) ) where diff --git a/DCLabel/NanoEDSL.hs b/DCLabel/NanoEDSL.hs --- a/DCLabel/NanoEDSL.hs +++ b/DCLabel/NanoEDSL.hs @@ -1,3 +1,13 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +{-# LANGUAGE Trustworthy #-} +#else +#warning "This module is not using SafeHaskell" +#endif +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} + {-| This module implements a ``nano``, very simple, embedded domain specific language to create 'Label's and 'Priv'ilages from conjunctions of principal disjunctions. @@ -54,10 +64,6 @@ -} - -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} module DCLabel.NanoEDSL ( -- * Operators (.\/.), (./\.) , (<>), (><) diff --git a/DCLabel/PrettyShow.hs b/DCLabel/PrettyShow.hs --- a/DCLabel/PrettyShow.hs +++ b/DCLabel/PrettyShow.hs @@ -1,3 +1,9 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +{-# LANGUAGE Trustworthy #-} +#else +#warning "This module is not using SafeHaskell" +#endif {-| This module exports a function 'prettyShow' that pretty prints 'Principal's, 'Disj'unctions, 'Conj'unctions, 'Label's and 'DCLabel's. -} diff --git a/DCLabel/Safe.hs b/DCLabel/Safe.hs --- a/DCLabel/Safe.hs +++ b/DCLabel/Safe.hs @@ -1,3 +1,9 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +{-# LANGUAGE Trustworthy #-} +#else +#warning "This module is not using SafeHaskell" +#endif {-| This module exports a safe-subset of "DCLabel.Core", implementing Disjunction Category Labels. @@ -9,8 +15,8 @@ module DCLabel.Safe ( -- * DC Labels with EDSL join, meet, top, bottom, canflowto - , Label, DCLabel, secrecy, integrity - , principal, singleton + , Label(..), DCLabel(..), Disj(..), Conj(..) + , Principal, principal, name, singleton , listToDisj, disjToList , listToLabel, labelToList , (.\/.), (./\.) @@ -21,17 +27,13 @@ , canflowto_p , delegatePriv , canDelegate, owns - , newPriv, NewPriv, newTCBPriv + , newPriv, NewPriv, newTCBPriv, noPriv ) where import DCLabel.Core -import DCLabel.NanoEDSL - - - - - - - - +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +import safe DCLabel.NanoEDSL +#else +import DCLabel.NanoEDSL +#endif diff --git a/DCLabel/Secrecy.hs b/DCLabel/Secrecy.hs --- a/DCLabel/Secrecy.hs +++ b/DCLabel/Secrecy.hs @@ -1,3 +1,9 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) +{-# LANGUAGE Trustworthy #-} +#else +#warning "This module is not using SafeHaskell" +#endif {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} module DCLabel.Secrecy ( SLabel(..) ) where diff --git a/Examples/ExamplesDCLabels.hs b/Examples/ExamplesDCLabels.hs --- a/Examples/ExamplesDCLabels.hs +++ b/Examples/ExamplesDCLabels.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE Trustworthy #-} module ExamplesDCLabels where import DCLabel.TCB diff --git a/Examples/Labels.hs b/Examples/Labels.hs --- a/Examples/Labels.hs +++ b/Examples/Labels.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE Safe #-} module Labels where import DCLabel.Safe diff --git a/Examples/ListExamples.hs b/Examples/ListExamples.hs new file mode 100644 --- /dev/null +++ b/Examples/ListExamples.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE Safe #-} +module ListExamples where + +import DCLabel.Safe +import DCLabel.PrettyShow + +c1 = listToDisj [principal "Alice"] + +c2 = listToDisj ["Alice", "Bob"] + +c3 = (<>) + +-- Labels, i.e. conjunctions of disjunctions +-- Observe the precedence of .\/. is higher than ./\. + +l1 = c2 ./\. "Carla" + +l2 = "Alice" ./\. "Carla" + +-- DCLabels + +dc1 = newDC l1 l2 + +dc2 = newDC ("Deian") ("Alice") + +main = do + putStrLn . prettyShow $ dc1 + putStrLn . prettyShow $ dc2 + putStrLn . prettyShow $ join dc1 dc2 + putStrLn . prettyShow $ meet dc1 dc2 + + putStrLn . prettyShow $ dc1 + putStrLn . prettyShow $ join dc1 top + putStrLn . show $ canflowto dc1 top + putStrLn . show $ canflowto bottom dc1 +{- +<{["Alice" \/ "Bob"] /\ ["Carla"]} , {["Alice"] /\ ["Carla"]}> +<{["Deain"]} , {["Alice"]}> +<{["Alice" \/ "Bob"] /\ ["Carla"] /\ ["Deain"]} , {["Alice"]}> +<{["Alice" \/ "Bob" \/ "Deain"] /\ ["Carla" \/ "Deain"]} , {["Alice"] /\ ["Carla"]}> +<{["Alice" \/ "Bob"] /\ ["Carla"]} , {["Alice"] /\ ["Carla"]}> +<{ALL} , {}> +True +True +-} diff --git a/Examples/UsingEDSL.hs b/Examples/UsingEDSL.hs --- a/Examples/UsingEDSL.hs +++ b/Examples/UsingEDSL.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE Safe #-} module UsingEDSL where import DCLabel.Safe diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,25 +1,29 @@ -Disjunction Category Labels -Copyright (C) 2011, Deian Stefan, Alejandro Russo, and David Mazieres -All rights reserved. +Copyright (c) 2011 Deian Stefan, Alejandro Russo, John C. Mitchell, David Mazieres 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 nor the - names of its contributors may be used to endorse or promote products - derived from this software without specific prior written permission. +modification, are permitted provided that the following conditions are +met: -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 + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions, and the following disclaimer. + + 2. 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. + + 3. The name of the author may not be used to endorse or promote + products derived from this software without specific prior + written permission. + +THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``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 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. +DISCLAIMED. IN NO EVENT SHALL THE AUTHOR 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. diff --git a/Tests/Main.hs b/Tests/Main.hs --- a/Tests/Main.hs +++ b/Tests/Main.hs @@ -7,7 +7,7 @@ import DCLabel.Secrecy import DCLabel.Integrity import Data.List (tails) -import System (getArgs) +import System.Environment (getArgs) instance Arbitrary Principal where arbitrary = do p <- oneof $ map return ["A", "B", "C"] @@ -125,11 +125,24 @@ -- LIO's lostar lostar :: TCBPriv -> DCLabel -> DCLabel -> DCLabel -lostar p li lg = - let lip = newDC (secrecy li) ((integrity li) ./\. lp) - lgp = newDC ((secrecy lg) ./\. lp) (integrity lg) - lp = priv p - in join lip lgp +lostar p l g = + let (ls, li) = (toLNF . secrecy $ l, toLNF . integrity $ l) + (gs, gi) = (toLNF . secrecy $ g, toLNF . integrity $ g) + lp = toLNF $ priv p + rs' = c2l [c | c <- getCats ls + , not (lp `implies` (c2l [c]))] + rs'' = c2l [c | c <- getCats gs + , not (rs' `implies` (c2l [c]))] + rs = if ls == allLabel || gs == allLabel + then allLabel + else rs' `and_label` rs'' + ri = (li `and_label` lp) `or_label` gi + in toLNF $ simpleNewLabel p (newDC rs ri) + where getCats = conj . label + c2l = MkLabel . MkConj + simpleNewLabel p lr | p == rootPrivTCB = g + | p == noPriv = l `join` g + | otherwise = lr {- lr = lostar p li lg satisfies: diff --git a/dclabel.cabal b/dclabel.cabal --- a/dclabel.cabal +++ b/dclabel.cabal @@ -1,21 +1,21 @@ Name: dclabel -Version: 0.0.1 +Version: 0.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: Deian Stefan , - Alejandro Russo < russo at chalmers dot se >, +Copyright: (c) 2011 Deian Stefan, Alejandro Russo, John C. Mitchell, David Mazieres +Author: Deian Stefan, Alejandro Russo +Maintainer: Deian Stefan Stability: experimental -Synopsis: The Disjunction Category Label Format. +Synopsis: The Disjunction Category Label Format Category: Security Cabal-Version: >=1.6 Extra-source-files: - Examples/UsingEDSL.hs, - Examples/Labels.hs, - Examples/ExamplesDCLabels.hs, + Examples/ExamplesDCLabels.hs + Examples/Labels.hs + Examples/ListExamples.hs + Examples/UsingEDSL.hs Tests/Main.hs Description: