content: {-# LANGUAGE Trustworthy #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {- | This module exports a class 'Groups' that policy modules
  must define an instance of to define groups, or mappings
  between a group 'Principal'and the principals in the group.
  
  An app may then relabel a labeled value by using 'labelRewrite'.
  
  
  -}
  module Hails.PolicyModule.Groups ( Groups(..)
                                   , labelRewrite ) where
  
  import           Data.Monoid
  import qualified Data.Set as Set
  import qualified Data.Map as Map
  
  import           Control.Monad
  
  import           LIO
  import           LIO.DCLabel
  
  import           Hails.Database
  import           Hails.Database.TCB (dbActionPriv, getActionStateTCB)
  import           Hails.PolicyModule
  
  
  class PolicyModule pm => Groups pm where
    -- | Typically, the action should expand a principal such as @#group@ to
    -- list of group members @[alice, bob]@.
    groups :: pm                   -- ^ Unused type-enforcing param
           -> DCPriv               -- ^ Policy module privs
           -> Principal            -- ^ Group
           -> DBAction [Principal] -- ^ (Policy module, group members)
    -- | Endorse the implementation of this instance. Note that this is
    -- reduced to WHNF to catch invalid instances that use 'undefined'.
    --
    -- Example implementation:
    --
    -- > groupsInstanceEndorse _ = MyPolicyModuleTCB {- Leave other values undefined -}
    groupsInstanceEndorse :: pm
  
  -- | Given the policy module (which is used to invoke the right
  -- 'groups' function) and labeled value, relabel the value according
  -- to the 'Groups' of the policy module. Note that the first argument
  -- may be bottom since it is solely used for typing purposes.
  labelRewrite :: forall unused_pm a. Groups unused_pm
               => unused_pm
               -- ^ Policy module
               -> DCLabeled a
               -- ^ Label
               -> DBAction (DCLabeled a)
  labelRewrite pm lx = withDBContext "labelRewrite" $ do
    -- Make sure that 'groupsInstanceEndorse' is not bottom
    _ <- liftLIO $ evaluate (groupsInstanceEndorse :: unused_pm)
    pmPriv <- getPMPriv
  
    -- Build map from principals to list of princpals
    pMap <- Set.fold (\p act -> act >>= \m -> do
              ps <- groups pm pmPriv p
              return (Map.insert p ps m)) (return Map.empty) principals
    -- Apply map to all principals in the label
    let lnew = (expandPrincipals pMap s) %% (expandPrincipals pMap i)
    -- Relabel labeled value
    liftLIO $ withPMClearanceP pmPriv $ relabelLabeledP pmPriv lnew lx
      where getPMPriv = do
              pmPriv <- dbActionPriv `liftM` getActionStateTCB
              -- Make sure that the underlying policy module
              -- and one named in the first parameter are the same
              case Map.lookup (policyModuleTypeName pm) availablePolicyModules of
                Nothing -> return mempty
                Just (p,_,_) -> return $ if toCNF p == privDesc pmPriv
                                         then pmPriv
                                         else mempty
            -- Modify label by expanding principals according to the map
            expandPrincipals pMap origPrincipals =
                  -- Function to fold over disjunctions in a CNF, expanding each
                  -- principal with the groups map
              let cFoldF :: Disjunction -> CNF -> CNF
                  cFoldF disj accm =
                    (Set.foldr expandOne cFalse $ dToSet disj) /\ accm
                  -- Inner fold function, expands a single principal and adds
                  -- to a CNF (that represents a Disjunction
                  expandOne :: Principal -> CNF -> CNF
                  expandOne princ accm =
                    (dFromList $ pMap Map.! princ) \/ accm
              in Set.foldr cFoldF cTrue $ cToSet origPrincipals
            -- Label components
            s = dcSecrecy $ labelOf lx
            i = dcIntegrity $ labelOf lx
            -- All unique principals in the labe
            principals = getPrincipals s <> getPrincipals i
            -- Get principals form component
            getPrincipals = mconcat . (map dToSet) . Set.elems . cToSet
  
  