#if __GLASGOW_HASKELL__ >= 702
#endif
module LIO.DCLabel (
module DCLabel.Safe
, DCCatSet
, DCPriv, DCPrivTCB
, DCLabeled, DC, evalDC, evalDCWithRoot
)where
import LIO.TCB
import LIO.Handle (evalWithRoot)
#if __GLASGOW_HASKELL__ >= 702
import safe Data.Typeable
#else
import Data.Typeable
#endif
import DCLabel.Safe hiding ( 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.Component
deriving instance Typeable DCL.DCLabel
instance Label DCLabel where
lbot = DCL.bottom
ltop = DCL.top
lub = DCL.join
glb = DCL.meet
leq = DCL.canflowto
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_component` rs''
ri = (li `DCL.and_component` lp) `DCL.or_component` gi
in DCL.toLNF $ simpleNewLabel p (newDC rs ri)
where getCats = DCL.conj . DCL.component
c2l = DCL.MkComponent . DCL.MkConj
simpleNewLabel pr lr | pr == DCL.rootPrivTCB = g
| pr == DCL.noPriv = l `lub` g
| otherwise = lr
type DCCatSet = DCL.Component
type DCPriv = DCL.Priv
type DCPrivTCB = DCL.TCBPriv
instance LabelState DCLabel DCPrivTCB () where
type DCLabeled a = Labeled DCLabel a
type DC = LIO DCLabel DCPrivTCB ()
evalDC :: DC a -> IO (a, DCLabel)
evalDC m = evalLIO m ()
evalDCWithRoot :: FilePath -> Maybe DCLabel -> DC a -> IO (a, DCLabel)
evalDCWithRoot path ml act = evalWithRoot path ml act ()