module LIO.DCLabel (
module DCLabel.Safe
, DCCatSet
, DCPriv, DCPrivTCB
, DC, evalDC
)where
import LIO.TCB
import Data.Typeable
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 li lg =
let lip = newDC (DCL.secrecy li) ((DCL.integrity li) ./\. lp)
lgp = newDC ((DCL.secrecy lg) ./\. lp) (DCL.integrity lg)
lp = DCL.priv p
in DCL.join lip lgp
type DCCatSet = DCL.Label
type DCPriv = DCL.Priv
type DCPrivTCB = DCL.TCBPriv
type DC = LIO DCLabel ()
evalDC :: DC a -> IO (a, DCLabel)
evalDC m = evalLIO m ()