module SecLib.Declassification
(
Open
, Close
, Authority
, hatch
, ntimes
, flock
, dlm
, certify
)
where
import SecLib.Sec ( Sec (), reveal, unSecType )
import SecLib.SecIO
import Data.IORef
import SecLib.Lattice ( Less (less) )
type Open s = SecIO s ()
type Close s = SecIO s ()
data Authority s = forall s'. Authority (Open s') (Close s')
hatch :: Less sl sh => (a -> b) -> Sec sh a -> SecIO s (Sec sl b)
hatch f sec_sh = less sl sh `seq` return sec_sl
where
sec_sl = return $ f $ reveal sec_sh
sh = unSecType sec_sh
sl = unSecType sec_sl
ntimes :: Int -> (Sec sh a -> SecIO s (Sec sl b))
-> IO (Sec sh a -> SecIO s (Sec sl b))
ntimes n f = do ref <- newIORef n
return $ \sa ->
MkSecIO $
do k <- readIORef ref
let MkSecIO m = f sa
if k <= 0
then error "ntimes failed!"
else do writeIORef ref (k1)
m
flock :: (Sec sh a -> SecIO s (Sec sl b))
-> IO (Sec sh a -> SecIO s (Sec sl b), Open s, Close s)
flock f = do ref <- newIORef False
return (\sa -> MkSecIO $
do b <- readIORef ref
let MkSecIO m = f sa
if b then m
else error "flock fails!"
, MkSecIO $ writeIORef ref True >> return (return ())
, MkSecIO $ writeIORef ref False >> return (return ())
)
dlm :: (Sec sh a -> SecIO s (Sec sl b))
-> IO (Sec sh a -> SecIO s (Sec sl b), Authority sh)
dlm f = do (whof, open, close) <- flock f
return (whof, Authority open close)
certify :: sh -> Authority sh -> SecIO s a -> SecIO s a
certify sh (Authority open close) sec_io =
sh `seq` do MkSecIO $ run open >> return (return ())
a <- sec_io
MkSecIO $ run close >> return (return ())
return a