packages feed

lmonad (empty) → 0.1.0.0

raw patch · 9 files changed

+583/−0 lines, 9 filesdep +HUnitdep +basedep +containerssetup-changed

Dependencies added: HUnit, base, containers, exceptions, lmonad, monad-control, transformers, transformers-base

Files

+ LICENSE view
@@ -0,0 +1,7 @@+Copyright 2014 James Parker.++Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ lmonad.cabal view
@@ -0,0 +1,102 @@+-- Initial lmonad.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++-- The name of the package.+name:                lmonad++-- The package version.  See the Haskell package versioning policy (PVP) +-- for standards guiding when and how versions should be incremented.+-- http://www.haskell.org/haskellwiki/Package_versioning_policy+-- PVP summary:      +-+------- breaking API changes+--                   | | +----- non-breaking API additions+--                   | | | +--- code changes with no API change+version:             0.1.0.0++-- A short (one-line) description of the package.+synopsis:            LMonad is an Information Flow Control (IFC) framework for Haskell applications.++-- A longer description of the package.+description:         LMonad is an Information Flow Control (IFC) framework for Haskell applications. It can be used to enforce security properties like confidentiality and integrity. It is derived from [LIO](http://hackage.haskell.org/package/lio), but is more general in that it tracks information flow for any monad by using monad transformers.++-- The license under which the package is released.+license:             MIT++-- The file containing the license text.+license-file:        LICENSE++-- The package author(s).+author:              James Parker++-- An email address to which users can send suggestions, bug reports, and +-- patches.+maintainer:          dev@jamesparker.me++-- A copyright notice.+-- copyright:           ++category:            Security++build-type:          Simple++-- Constraint on the version of Cabal needed to build this package.+cabal-version:       >=1.8+++library+  -- Modules exported by the library.+  exposed-modules:+      LMonad+    , LMonad.Label.DisjunctionCategory+    , LMonad.Label.PowerSet+    , LMonad.TCB+  +  -- Modules included in this library but not exported.+  other-modules:+      LMonad.Label++  hs-source-dirs:+      src+  +  ghc-options:+      -Wall -fno-warn-name-shadowing++  extensions:+      DoAndIfThenElse+      MultiParamTypeClasses+      DatatypeContexts++  -- Other library packages from which modules are imported.+  build-depends:+      base < 5+    , containers+    , exceptions+    , monad-control >= 1.0.0.0+    , transformers+    , transformers-base+  +Test-Suite test-lmonad+  type:+      exitcode-stdio-1.0+  hs-source-dirs:+      test+    , src+  main-is:+      Main.hs+  build-depends:+      base+    , containers+    , exceptions+    , HUnit+    , lmonad+    , monad-control+    , transformers+    , transformers-base+  extensions:+      DoAndIfThenElse+      MultiParamTypeClasses+  ghc-options:+      -Wall++source-repository head+  type:              git+  location:          https://github.com/jprider63/LMonad
+ src/LMonad.hs view
@@ -0,0 +1,31 @@+-- | A generalization of LIO's core components to work for any monad, instead of just IO. ++module LMonad (module LMonad) where++import LMonad.TCB as LMonad ( +        Label (..)+      , LMonad (..)+      , LMonadT+      , runLMonad+      , lLift+      , getCurrentLabel+      , getClearance+      , lubCurrentLabel+      , canSetLabel+      , setLabel+      , taintLabel+      , setClearance+      , Labeled+      , label+      , unlabel+      , canUnlabel+      , labelOf+      , ToLabel(..)+      , swapBase+    )++-- most code should import LMonad+-- trusted code can import LMonad.TCB+--+-- You will also need to import a LMonad.Label.* module or create an instance of Label.+
+ src/LMonad/Label.hs view
@@ -0,0 +1,11 @@+module LMonad.Label where++import Prelude++class Label l where+    -- Join+    lub :: l -> l -> l+    -- Meet+    glb :: l -> l -> l+    canFlowTo :: l -> l -> Bool+    bottom :: l
+ src/LMonad/Label/DisjunctionCategory.hs view
@@ -0,0 +1,95 @@+-- Some work derived from [LIO](http://hackage.haskell.org/package/lio-eci11), copyrighted under GPL.+--+-- Modifications by James Parker in 2014.++module LMonad.Label.DisjunctionCategory where++import Data.Set (Set)+import qualified Data.Set as Set+import Prelude++import LMonad++-- TODO: Add bloom filter?? It's probably not worth it with principals usually on the order of 10.+-- data Ord p => Disjunction p = Disjunction (Set p)+type Disjunction p = Set p+type Conjunction p = Set (Disjunction p)++-- | Disjunction category label of principals in conjunction normal form. +data Ord p => DCLabel p = DCLabel {+        dcConfidentiality :: Conjunction p+      , dcIntegrity :: Conjunction p+    }++    deriving (Eq, Show)++-- | Convenience function to convert a principal to confidentiality and integrity DCLabel.+dcSingleton :: Ord p => p -> DCLabel p+dcSingleton p = +    let conj = Set.singleton (Set.singleton p) in+    DCLabel conj conj++-- | Convenience function to convert a principal to confidentiality DCLabel.+dcConfidentialitySingleton :: Ord p => p -> DCLabel p+dcConfidentialitySingleton p = DCLabel (Set.singleton (Set.singleton p)) $ Set.singleton Set.empty++-- | Convenience function to convert a principal to integrity DCLabel.+dcIntegritySingleton :: Ord p => p -> DCLabel p+dcIntegritySingleton p = DCLabel Set.empty (Set.singleton (Set.singleton p))++-- O(n)+forall :: (a -> Bool) -> Set a -> Bool+forall pred = Set.foldl' (\acc el -> acc && (pred el)) True++-- O(n)+exists :: (a -> Bool) -> Set a -> Bool+exists pred = Set.foldl' (\acc el -> acc || (pred el)) False++-- Equivalent to implies for disjunctions. O(n + m)+-- TODO: Add bloom filters here??? Would reduce to O(1) for most lookups. +subset :: Ord p => Disjunction p -> Disjunction p -> Bool+subset = Set.isSubsetOf++-- | Computes logical implies. Assumes CNF. O(n * m * (n' + m'))+implies :: Ord p => Conjunction p -> Conjunction p -> Bool+implies a b = +    -- forall b. exists a. a is a subset of b+    forall (\elB -> exists (\elA -> subset elA elB) a) b++-- O(n * (n' + m))+conjunctionInsertDisjunction :: Ord p => Conjunction p -> Disjunction p -> Conjunction p+conjunctionInsertDisjunction conj disj =+    -- Check if any element in acc implies disjunction.+    if exists (`subset` disj) conj then+        conj+    else+        -- Remove any elements in acc where that element is implied by the disjunction, and insert disjunction.+        Set.insert disj $ Set.filter (\el -> not (disj `subset` el)) conj++-- O(m * n * (n' + m')) ??+conjunctionAnd :: Ord p => Conjunction p -> Conjunction p -> Conjunction p+conjunctionAnd = Set.foldl' conjunctionInsertDisjunction++-- O(m * n * ()) ???+-- TODO: Optimize this more??? XXX+conjunctionOr :: Ord p => Conjunction p -> Conjunction p -> Conjunction p+conjunctionOr conj1 = Set.foldl' (\acc disj2 -> Set.foldl' (\acc disj1 ->+        conjunctionInsertDisjunction acc (Set.union disj1 disj2)+    ) acc conj1) Set.empty ++instance Ord p => Label (DCLabel p) where+    -- Meet+    glb (DCLabel c1 i1) (DCLabel c2 i2) = +        DCLabel (c1 `conjunctionOr` c2) (i1 `conjunctionAnd` i2)++    -- Join+    lub (DCLabel c1 i1) (DCLabel c2 i2) = +        DCLabel (c1 `conjunctionAnd` c2) (i1 `conjunctionOr` i2)++    -- Flow to+    canFlowTo (DCLabel c1 i1) (DCLabel c2 i2) = +        c2 `implies` c1 && i1 `implies` i2++    -- Bottom+    bottom = DCLabel Set.empty $ Set.singleton Set.empty+
+ src/LMonad/Label/PowerSet.hs view
@@ -0,0 +1,56 @@+module LMonad.Label.PowerSet where++import Data.Set (Set)+import qualified Data.Set as Set+import Prelude++import LMonad++-- | Power set label made of all combinations of the principals. +data Ord p => PSLabel p = PSLabel {+        psLabelConfidentiality :: Set p+      , psLabelIntegrity :: Set p+    }+        deriving Show++-- | Convenience function to convert a principal to confidentiality and integrity PSLabel.+psSingleton :: Ord p => p -> PSLabel p+psSingleton p = +    let p' = Set.singleton p in+    PSLabel p' p'++-- | Convenience function to convert a principal to confidentiality PSLabel.+psConfidentialitySingleton :: Ord p => p -> PSLabel p+psConfidentialitySingleton p = +    let p' = Set.singleton p in+    PSLabel p' Set.empty++-- | Convenience function to convert a principal to integrity PSLabel.+psIntegritySingleton :: Ord p => p -> PSLabel p+psIntegritySingleton p =+    let p' = Set.singleton p in+    PSLabel Set.empty p'++instance Ord p => Label (PSLabel p) where+    -- Meet+    glb (PSLabel c1 i1) (PSLabel c2 i2) =   +        let c = Set.intersection c1 c2 in+        let i = Set.intersection i1 i2 in+        PSLabel c i++    -- Join+    lub (PSLabel c1 i1) (PSLabel c2 i2) =   +        let c = Set.union c1 c2 in+        let i = Set.union i1 i2 in+        PSLabel c i++    -- Flow to+    canFlowTo (PSLabel c1 i1) (PSLabel c2 i2) =+        (Set.isSubsetOf c1 c2) && (Set.isSubsetOf i1 i2)++    -- Bottom+    bottom = +        PSLabel Set.empty Set.empty++-- | Type alias for labeled power sets.+type PSLabeled p = Labeled (PSLabel p)
+ src/LMonad/TCB.hs view
@@ -0,0 +1,262 @@+-- Some work derived from [LIO](http://hackage.haskell.org/package/lio-eci11), copyrighted under GPL.+--+-- Modifications by James Parker in 2014.++{-# LANGUAGE FlexibleInstances, FlexibleContexts, TypeFamilies #-}++-- Only trusted code should import this module. ++module LMonad.TCB (+        module Export+      , LMonad (..)+      , LMonadT+      , runLMonad+      , lLift+      , getCurrentLabel+      , getClearance+      , lubCurrentLabel+      , canSetLabel+      , setLabel+      , taintLabel+      , setClearance+      , raiseClearanceTCB+      , lowerLabelTCB+      , Labeled+      , label+      , unlabel+      , canUnlabel+      , labelOf+      , toLabeledTCB+      , ToLabel(..)+      , swapBase+    ) where++import Control.Applicative+import Control.Monad+import Control.Monad.Base+import Control.Monad.Catch+import Control.Monad.IO.Class+import Control.Monad.Trans.Class+import Control.Monad.Trans.Control+import Control.Monad.Trans.State+import Data.Monoid+import Prelude++import LMonad.Label as Export++class Monad m => LMonad m where+    lFail :: m a+    lAllowLift :: m Bool+    -- lLift???++data Label l => LState l = LState {+        lStateLabel :: !l+      , lStateClearance :: !l+    }++-- | Type class to convert a given type to a given label.+class ToLabel t l where+    toConfidentialityLabel :: t -> l+    toIntegrityLabel :: t -> l++-- Transformer monad that wraps the underlying monad and keeps track of information flow. +data (Label l, Monad m, LMonad m) => LMonadT l m a = LMonadT {+        lMonadTState :: (StateT (LState l) m a)+    }++instance (Label l, LMonad m) => Monad (LMonadT l m) where+    (LMonadT ma) >>= f = +        LMonadT $ ma >>= (lMonadTState . f)+        -- LMonadT $ do+        -- a <- ma+        -- let (LMonadT mb) = f a+        -- mb+    return = LMonadT . return+    fail _ = LMonadT $ lift lFail++instance (Label l, LMonad m, Functor m) => Functor (LMonadT l m) where+    fmap f (LMonadT ma) = LMonadT $ fmap f ma++instance (Label l, LMonad m, Functor m) => Applicative (LMonadT l m) where+    pure = return+    (<*>) = ap+    +instance (Label l, LMonad m, MonadIO m) => MonadIO (LMonadT l m) where+    liftIO ma = lLift $ liftIO ma++instance (LMonad m, Label l, Functor m, MonadBase IO m) => MonadBase IO (LMonadT l m) where+    liftBase = lLift . liftBase++instance (Label l, LMonad m, MonadThrow m) => MonadThrow (LMonadT l m) where+    throwM = lLift . throwM++newtype StMT l m a = StMT {unStMT :: StM (StateT (LState l) m) a}++-- TODO: This allows replay attacks. Ie, malicious code could reset the current label or clearance to a previous value. +--     This is needed for Database.Persist.runPool+instance (LMonad m, Label l, MonadBaseControl IO m) => MonadBaseControl IO (LMonadT l m) where+    -- newtype StM (LMonadT l m) a = StMT {unStMT :: StM (StateT (LState l) m) a}+    type StM (LMonadT l m) a = StMT l m a+    liftBaseWith f = LMonadT $ liftBaseWith $ \run -> f $ liftM StMT . run . lMonadTState+    restoreM = LMonadT . restoreM . unStMT++instance (LMonad m, Label l, Monoid (m a)) => Monoid (LMonadT l m a) where+    mempty = lLift mempty+    mappend a b = a >> b +--    do+--        a' <- a +--        b' <- b+--        return $ mappend a b+    +-- Runs the LMonad with bottom as the initial label and clearance. +runLMonad :: (Label l, LMonad m) => LMonadT l m a -> m a+runLMonad (LMonadT lm) = +    let s = LState bottom bottom in+    evalStateT lm s++-- class LMonadTrans t where +--     lift :: (LMonad m) => m a -> t m a+-- instance (Label l) => MonadTrans (LMonadT l) where+--     -- lift :: (Monad m, LMonad m) => m a -> LMonadT l m a+--     lift m = LMonadT $ lift m++lLift :: (Label l, LMonad m) => m a -> LMonadT l m a+lLift ma = LMonadT $ do+    allow <- lift lAllowLift+    if allow then+        lift ma+    else+        lift lFail++getCurrentLabel :: (Label l, LMonad m) => LMonadT l m l+getCurrentLabel = LMonadT $ do+    (LState label _) <- get+    return label++lubCurrentLabel :: (Label l, LMonad m) => l -> LMonadT l m l+lubCurrentLabel l = do+    getCurrentLabel >>= (return . (lub l))++getClearance :: (Label l, LMonad m) => LMonadT l m l+getClearance = LMonadT $ do+    (LState _ clearance) <- get+    return clearance++canAlloc :: (Label l, LMonad m) => l -> StateT (LState l) m Bool+canAlloc l = do+    (LState label clearance) <- get+    return $ canFlowTo label l && canFlowTo l clearance++guardAlloc :: (Label l, LMonad m) => l -> StateT (LState l) m ()+guardAlloc l = do+    guard <- canAlloc l+    unless guard $ +        lift lFail++canSetLabel :: (Label l, LMonad m) => l -> LMonadT l m Bool+canSetLabel = LMonadT . canAlloc++setLabel :: (Label l, LMonad m) => l -> LMonadT l m ()+setLabel l = do+    LMonadT $ guardAlloc l+    setLabelTCB l++setLabelTCB :: (Label l, LMonad m) => l -> LMonadT l m ()+setLabelTCB l = LMonadT $ do+    (LState _ clearance) <- get+    put $ LState l clearance++taintLabel :: (Label l, LMonad m) => l -> LMonadT l m ()+taintLabel l = do+    lM' <- taintHelper l+    case lM' of+        Nothing ->+            LMonadT $ lift lFail+        Just l' -> do+            setLabelTCB l'++    -- lubCurrentLabel l >>= setLabel++-- canTaintLabel :: (Label l, LMonad m) => l -> LMonadT l m Bool+-- canTaintLabel l = do+--     lubCurrentLabel l >>= (LMonadT . canAlloc)++setClearance :: (Label l, LMonad m) => l -> LMonadT l m ()+setClearance c = LMonadT $ do+    guardAlloc c+    (LState label _) <- get+    put $ LState label c++-- TODO: Does this diverge from LIO's formalism?+-- Sets the current clearance to the join of the old clearance and the given clearance.+raiseClearanceTCB :: (Label l, LMonad m) => l -> LMonadT l m ()+raiseClearanceTCB c = LMonadT $ do+    (LState label clearance) <- get+    put $ LState label $ lub clearance c++-- TODO: I think this does diverge from LIO+-- Sets the current label to the meet of the old label and the given label.+lowerLabelTCB :: (Label l, LMonad m) => l -> LMonadT l m ()+lowerLabelTCB l = LMonadT $ do+    (LState label clearance) <- get+    put $ LState (glb label l) clearance++-- Labeled values.+data Label l => Labeled l a = Labeled {+        labeledLabel :: l+      , labeledValue :: a+    }++label :: (Label l, LMonad m) => l -> a -> LMonadT l m (Labeled l a)+label l a = LMonadT $ do+    guardAlloc l+    return $ Labeled l a++-- | Join the given label with the current label. +-- Return the result if it can flow to the clearance.+taintHelper :: (Label l, LMonad m) => l -> LMonadT l m (Maybe l)+taintHelper l = do+    (LState label clearance) <- LMonadT get+    let l' = label `lub` l+    if l' `canFlowTo` clearance then+        return $ Just l'+    else+        return Nothing+        +unlabel :: (Label l, LMonad m) => Labeled l a -> LMonadT l m a+unlabel l = do+    taintLabel $ labelOf l+    return $ labeledValue l++    -- setLabel $ labelOf l+    -- return $ labeledValue l++canUnlabel :: (Label l, LMonad m) => Labeled l a -> LMonadT l m Bool+canUnlabel l = do+    fmap (maybe False $ const True) $ taintHelper $ labelOf l++    -- clearance <- getClearance+    -- return $ canFlowTo (labelOf l) clearance++labelOf :: Label l => Labeled l a -> l+labelOf = labeledLabel++-- TODO: I'm pretty sure this also differs from their semantics+-- Should this also be TCB? Could potentially leak via side channel since lifting might be allowed. +toLabeledTCB :: (Label l, LMonad m) => l -> LMonadT l m a -> LMonadT l m (Labeled l a)+toLabeledTCB l ma = do+    oldLabel <- getCurrentLabel+    oldClearance <- getClearance+    raiseClearanceTCB l+    a <- ma+    la <- label l a+    lowerLabelTCB oldLabel+    setClearance oldClearance+    return la++swapBase :: (Label l, LMonad m, LMonad n) => (m (a,LState l) -> n (b,LState l)) -> LMonadT l m a -> LMonadT l n b+swapBase f (LMonadT m) = LMonadT $ do+    prev <- get+    ( res, new) <- lift $ f $ (runStateT m) prev+    put new+    return res
+ test/Main.hs view
@@ -0,0 +1,17 @@+module Main (main) where++import System.Exit (exitFailure)+import Test.HUnit++import qualified DCLabelTest++tests :: Test+tests = TestList [ DCLabelTest.tests]++main :: IO ()+main = do +    Counts _ _ errC failC <- runTestTT $ tests+    if errC + failC == 0 then+        return ()+    else+        exitFailure