dclabel 0.0.1 → 0.0.2

raw patch · 13 files changed

+148/−56 lines, 13 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• DCLabel/Core.hs +5/−4
• DCLabel/Integrity.hs +6/−0
• DCLabel/NanoEDSL.hs +10/−4
• DCLabel/PrettyShow.hs +6/−0
• DCLabel/Safe.hs +14/−12
• DCLabel/Secrecy.hs +6/−0
• Examples/ExamplesDCLabels.hs +1/−0
• Examples/Labels.hs +1/−0
• Examples/ListExamples.hs +45/−0
• Examples/UsingEDSL.hs +1/−0
• LICENSE +25/−21
• Tests/Main.hs +19/−6
• dclabel.cabal +9/−9

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

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

@@ -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 			  (.\/.), (./\.)                         , (<>), (><)

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

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

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

@@ -1,3 +1,4 @@+{-# LANGUAGE Trustworthy #-} module ExamplesDCLabels where   import DCLabel.TCB

@@ -1,3 +1,4 @@+{-# LANGUAGE Safe #-} module Labels where   import DCLabel.Safe

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

@@ -1,3 +1,4 @@+{-# LANGUAGE Safe #-} module UsingEDSL where   import DCLabel.Safe

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

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

@@ -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  <deian at cs dot stanford dot edu>,-		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  <deian at cs dot stanford dot edu> 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: