#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)
#else
#warning "This module is not using SafeHaskell"
#endif
module LIO.DCLabel (
module DCLabel.Safe
, DCCatSet
, DCPriv, DCPrivTCB
, DCLabeled, DC, evalDC
)where
import LIO.TCB
#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)
import safe Data.Typeable
#else
import Data.Typeable
#endif
import DCLabel.Safe hiding ( Label
, Priv
, bottom
, top
, join
, meet)
import qualified DCLabel.Core as DCL
deriving instance Typeable DCL.Disj
deriving instance Typeable DCL.Conj
deriving instance Typeable DCL.Label
deriving instance Typeable DCL.DCLabel
instance POrd DCLabel where
leq = DCL.canflowto
instance Label DCLabel where
lbot = DCL.bottom
ltop = DCL.top
lub = DCL.join
glb = DCL.meet
instance PrivTCB DCL.TCBPriv
instance MintTCB DCL.TCBPriv DCL.Priv where
mintTCB = DCL.createPrivTCB
instance MintTCB DCL.TCBPriv DCL.Principal where
mintTCB p = DCL.createPrivTCB (newPriv p)
instance Priv DCLabel DCL.TCBPriv where
leqp = DCL.canflowto_p
lostar p l g =
let (ls, li) = (DCL.toLNF . secrecy $ l, DCL.toLNF . integrity $ l)
(gs, gi) = (DCL.toLNF . secrecy $ g, DCL.toLNF . integrity $ g)
lp = DCL.toLNF . DCL.priv $ p
rs' = c2l [c | c <- getCats ls
, not (lp `DCL.implies` (c2l [c]))]
rs'' = c2l [c | c <- getCats gs
, not (rs' `DCL.implies` (c2l [c]))]
rs = rs' `DCL.and_label` rs''
ri = (li `DCL.and_label` lp) `DCL.or_label` gi
in DCL.toLNF $ simpleNewLabel p (newDC rs ri)
where getCats = DCL.conj . DCL.label
c2l = DCL.MkLabel . DCL.MkConj
simpleNewLabel p lr | p == DCL.rootPrivTCB = g
| p == DCL.noPriv = l `lub` g
| otherwise = lr
type DCCatSet = DCL.Label
type DCPriv = DCL.Priv
type DCPrivTCB = DCL.TCBPriv
type DCLabeled a = Labeled DCLabel a
type DC = LIO DCLabel ()
evalDC :: DC a -> IO (a, DCLabel)
evalDC m = evalLIO m ()