lio 0.0.1 → 0.0.2
raw patch · 16 files changed
+691/−83 lines, 16 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- LIO.MonadCatch: instance MonadCatch IO
+ LIO.Base: LerrClearance :: LabelFault
+ LIO.Base: LerrHigh :: LabelFault
+ LIO.Base: LerrInval :: LabelFault
+ LIO.Base: LerrLow :: LabelFault
+ LIO.Base: LerrPriv :: LabelFault
+ LIO.Base: NoPrivs :: NoPrivs
+ LIO.Base: PEQ :: POrdering
+ LIO.Base: PGT :: POrdering
+ LIO.Base: PLT :: POrdering
+ LIO.Base: PNE :: POrdering
+ LIO.Base: aguard :: Label l => l -> LIO l s ()
+ LIO.Base: aguardP :: Priv l p => p -> l -> LIO l s ()
+ LIO.Base: bracketP :: Priv l p => p -> LIO l s a -> (a -> LIO l s c) -> (a -> LIO l s b) -> LIO l s b
+ LIO.Base: catchP :: (Label l, Exception e, Priv l p) => p -> LIO l s a -> (l -> e -> LIO l s a) -> LIO l s a
+ LIO.Base: class (POrd a, Show a, Read a, Typeable a) => Label a
+ LIO.Base: class Eq a => POrd a
+ LIO.Base: class (Label l, Monoid p, PrivTCB p) => Priv l p
+ LIO.Base: data Label l => LIO l s a
+ LIO.Base: data LabelFault
+ LIO.Base: data Label l => Labeled l t
+ LIO.Base: data NoPrivs
+ LIO.Base: data POrdering
+ LIO.Base: discard :: Label l => l -> LIO l s a -> LIO l s ()
+ LIO.Base: evalLIO :: Label l => LIO l s a -> s -> IO (a, l)
+ LIO.Base: evaluate :: Label l => a -> LIO l s a
+ LIO.Base: getClearance :: Label l => LIO l s l
+ LIO.Base: getLabel :: Label l => LIO l s l
+ LIO.Base: glb :: Label a => a -> a -> a
+ LIO.Base: handleP :: (Label l, Exception e, Priv l p) => p -> (l -> e -> LIO l s a) -> LIO l s a -> LIO l s a
+ LIO.Base: label :: Label l => l -> a -> LIO l s (Labeled l a)
+ LIO.Base: labelOf :: Label l => Labeled l a -> l
+ LIO.Base: labelP :: Priv l p => p -> l -> a -> LIO l s (Labeled l a)
+ LIO.Base: lbot :: Label a => a
+ LIO.Base: leq :: POrd a => a -> a -> Bool
+ LIO.Base: leqp :: Priv l p => p -> l -> l -> Bool
+ LIO.Base: lostar :: Priv l p => p -> l -> l -> l
+ LIO.Base: lowerClr :: Label l => l -> LIO l s ()
+ LIO.Base: lowerClrP :: Priv l p => p -> l -> LIO l s ()
+ LIO.Base: ltop :: Label a => a
+ LIO.Base: lub :: Label a => a -> a -> a
+ LIO.Base: o2po :: Ordering -> POrdering
+ LIO.Base: onExceptionP :: Priv l p => p -> LIO l s a -> LIO l s b -> LIO l s a
+ LIO.Base: pcompare :: POrd a => a -> a -> POrdering
+ LIO.Base: setLabelP :: Priv l p => p -> l -> LIO l s ()
+ LIO.Base: taint :: Label l => l -> LIO l s ()
+ LIO.Base: taintLabeled :: Label l => l -> Labeled l a -> LIO l s (Labeled l a)
+ LIO.Base: taintP :: Priv l p => p -> l -> LIO l s ()
+ LIO.Base: toLabeled :: Label l => l -> LIO l s a -> LIO l s (Labeled l a)
+ LIO.Base: toLabeledP :: Priv l p => p -> l -> LIO l s a -> LIO l s (Labeled l a)
+ LIO.Base: unlabel :: Label l => Labeled l a -> LIO l s a
+ LIO.Base: unlabelP :: Priv l p => p -> Labeled l a -> LIO l s a
+ LIO.Base: wguard :: Label l => l -> LIO l s ()
+ LIO.Base: wguardP :: Priv l p => p -> l -> LIO l s ()
+ LIO.Base: withClearance :: Label l => l -> LIO l s a -> LIO l s a
+ LIO.DCLabel: type DCLabeled a = Labeled DCLabel a
+ LIO.MonadCatch: instance [safe] MonadCatch IO
+ LIO.TCB: instance Label l => Functor (Labeled l)
Files
- Examples/LambdaChair/AliceCode.hs +27/−0
- Examples/LambdaChair/BobCode.hs +22/−0
- Examples/LambdaChair/LambdaChair.hs +417/−0
- Examples/LambdaChair/Main.hs +13/−7
- Examples/LambdaChair/Safe.hs +12/−0
- LIO/Base.hs +27/−19
- LIO/DCLabel.hs +28/−18
- LIO/Handle.hs +22/−1
- LIO/LIO.hs +19/−5
- LIO/LIORef.hs +10/−0
- LIO/LIORef/Safe.hs +13/−5
- LIO/LIORef/TCB.hs +14/−4
- LIO/MonadCatch.hs +12/−0
- LIO/MonadLIO.hs +11/−0
- LIO/TCB.hs +33/−4
- lio.cabal +11/−20
+ Examples/LambdaChair/AliceCode.hs view
@@ -0,0 +1,27 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Safe #-}+#else+#warning "This module is not using SafeHaskell"+#endif+module AliceCode ( mainReview ) where++import Safe++findPaper' s = do+ ep <- findPaper s+ case ep of+ Left e -> error $ "Failed with" ++ e+ Right p -> return p++mainReview = do+ p1 <- findPaper' "Flexible Dynamic"+ p2 <- findPaper' "A Static"++ readPaper p1++ appendToReview p1 "Interesting work!"++ readPaper p2+ readReview p2+ appendToReview p2 "What about adding new users?"
+ Examples/LambdaChair/BobCode.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Safe #-}+#else+#warning "This module is not using SafeHaskell"+#endif+module BobCode ( mainReview ) where++import Safe++findPaper' s = do+ ep <- findPaper s+ case ep of+ Left e -> error $ "Failed with" ++ e+ Right p -> return p++mainReview = do+ p1 <- findPaper' "Flexible Dynamic..."+ p2 <- findPaper' "A Static..."+ appendToReview p2 "Hmm, IFC.."+ readReview p2+ readReview p1
+ Examples/LambdaChair/LambdaChair.hs view
@@ -0,0 +1,417 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ScopedTypeVariables #-}+module LambdaChair ( evalReviewDC+ , addUser+ , addPaper+ , addConflict+ , addAssignment+ , asUser+ ---+ , findPaper+ , retrievePaper, readPaper+ , retrieveReview, readReview+ , appendToReview+ , reviewDCPutStrLn + -- TCB+ , printUsersTCB+ , printReviewsTCB+ , reviewDCPutStrLnTCB + , dcPutStrLnTCB + ) where++import Prelude hiding (catch)+import Control.Monad+import Control.Exception (SomeException, ErrorCall(..))+import Control.Monad.State+import Data.Maybe+import Data.List+import Data.Monoid++import LIO.TCB+import LIO.LIORef+import LIO.LIORef.TCB (readLIORefTCB)+import LIO.MonadLIO+import LIO.MonadCatch (throwIO)+import LIO.DCLabel+import DCLabel.Safe+import DCLabel.TCB (Disj(..), Conj(..), Label(..))+import DCLabel.PrettyShow+++type ErrorStr = String+type DCLabeled = Labeled DCLabel+type DCRef = LIORef DCLabel++-- ^ Clss to with sideffectful show+class DCShowTCB s where+ dcShowTCB :: s -> DC String++dcPutStrLnTCB :: String -> DC ()+dcPutStrLnTCB = ioTCB . putStrLn++dcGetLineTCB :: DC String+dcGetLineTCB = ioTCB getLine++type Name = String+type Password = String+type Content = String+type Reviews = String++type Id = Int+data Paper = Paper Content+data Review = Review Content++data User = User { name :: Name+ , password :: Password+ , conflicts :: [Id]+ , assignments :: [Id] }++instance Eq User where+ u1 == u2 = name u1 == name u2++instance DCShowTCB User where+ dcShowTCB u = do+ return $ "Name: " ++ (name u) ++ "\n"+ ++ "Password: " ++ (password u) ++ "\n"+ ++ "Conflicts: " ++ (show . conflicts $ u) ++ "\n"+ ++ "Assignments: " ++ (show . assignments $ u)++data ReviewEnt = ReviewEnt { paperId :: Id+ , paper :: DCRef Paper+ , review :: DCRef Review }++instance Eq ReviewEnt where+ r1 == r2 = paperId r1 == paperId r2++instance DCShowTCB ReviewEnt where+ dcShowTCB r = do+ (Paper pap) <- readLIORefTCB (paper r)+ (Review rev) <- readLIORefTCB (review r)+ return $ "ID:" ++ (show . paperId $ r)+ ++ "\nPaper:" ++ pap+ ++ "\nReviews:" ++ rev+++-- State related+data ReviewState = ReviewState { users :: [User]+ , reviewEntries :: [ReviewEnt]+ , curUser :: Maybe Name }++emptyReviewState :: ReviewState+emptyReviewState = ReviewState [] [] Nothing++newtype ReviewDC a = ReviewDC (StateT ReviewState DC a)+ deriving (Monad, MonadFix)++liftReviewDC :: DC a -> ReviewDC a+liftReviewDC = ReviewDC . liftLIO++get' :: ReviewDC ReviewState+get' = ReviewDC . StateT $ \s -> return (s,s)++put' :: ReviewState -> ReviewDC ()+put' s = ReviewDC . StateT $ \_ -> return ((),s)++runReviewDC :: ReviewDC a -> ReviewState -> DC (a, ReviewState)+runReviewDC (ReviewDC m) s = runStateT m s++evalReviewDC :: ReviewDC a -> IO (a, DCLabel)+evalReviewDC m = evalDC $ do+ (a, s') <- runReviewDC m emptyReviewState+ return a+--++-- ^ Get all users+getUsers :: ReviewDC [User]+getUsers = get' >>= return . users++-- ^ Get all review entries+getReviews :: ReviewDC [ReviewEnt]+getReviews = get' >>= return . reviewEntries++-- ^ Get priviliges+getCurUserName :: ReviewDC (Maybe Name)+getCurUserName = get' >>= return . curUser++-- ^ Get curren tuser name+getCurUser :: ReviewDC (Maybe User)+getCurUser = do+ n <- getCurUserName+ maybe (return Nothing) findUser n++-- ^ Get priviliges+getPrivs :: ReviewDC DCPrivTCB+getPrivs = do + u <- getCurUser+ return $ maybe mempty (genPrivTCB . name) u++-- ^ Write new users+putUsers :: [User] -> ReviewDC ()+putUsers us = do+ rs <- getReviews+ u <- getCurUserName+ put' $ ReviewState us rs u++-- ^ Write new reviews+putReviews :: [ReviewEnt] -> ReviewDC ()+putReviews rs = do+ us <- getUsers+ u <- getCurUserName+ put' $ ReviewState us rs u++-- ^ Write new privs+putCurUserName :: Name -> ReviewDC ()+putCurUserName u = do+ us <- getUsers+ rs <- getReviews+ put' $ ReviewState us rs (Just u)++-- ^ Clear user naem+clearCurUserName :: ReviewDC ()+clearCurUserName = do+ us <- getUsers+ rs <- getReviews+ put' $ ReviewState us rs Nothing++-- ^ Find review entry by id+findReview :: Id -> ReviewDC (Maybe ReviewEnt)+findReview pId = do+ reviews <- getReviews+ return $ find (\e -> paperId e == pId) reviews++-- ^ Find user by name+findUser :: Name -> ReviewDC (Maybe User)+findUser n = do+ users <- getUsers+ return $ find (\u -> name u == n) users ++-- ^ Add new (fresh) user+addUser :: Name -> Password -> ReviewDC ()+addUser n p = do+ u <- findUser n+ unless (isJust u) $ do+ let newUser = User { name = n+ , password = p+ , conflicts = []+ , assignments = [] }+ us <- getUsers+ putUsers (newUser:us)++-- ^ Add conflicting paper to user+addConflict :: Name -> Id -> ReviewDC ()+addConflict n i = do+ usr <- findUser n+ pap <- findReview i+ case (usr, pap) of+ (Just u, Just _) -> + if i `elem` (assignments u)+ then return ()+ else do let u' = u { conflicts = i : (conflicts u)}+ usrs <- getUsers+ putUsers $ u' : (filter (/= u) usrs)+ _ -> return ()++-- ^ Assign a paper for the user to review+addAssignment :: Name -> Id -> ReviewDC ()+addAssignment n i = do+ usr <- findUser n+ pap <- findReview i+ case (usr, pap) of+ (Just u, Just _) -> + if i `elem` (conflicts u)+ then return ()+ else do let u' = u { assignments = i : (assignments u)}+ usrs <- getUsers+ putUsers $ u' : (filter (/= u) usrs)+ _ -> return ()++-- ^ Print users+printUsersTCB :: ReviewDC ()+printUsersTCB = do+ users <- getUsers+ mapM (liftReviewDC . dcShowTCB) users >>=+ reviewDCPutStrLnTCB . (intercalate "\n--\n")++-- ^ Print papers and reviews+printReviewsTCB :: ReviewDC ()+printReviewsTCB = do+ reviews <- getReviews+ mapM (liftReviewDC . dcShowTCB) reviews >>=+ reviewDCPutStrLnTCB . (intercalate "\n--\n")++-- | Generate privilege from a string+genPrivTCB :: NewPriv a => a -> DCPrivTCB+genPrivTCB = mintTCB . newPriv ++-- ^ Create new paper given id and content+newReviewEnt :: Id -> Content -> ReviewDC ReviewEnt+newReviewEnt pId content = do+ let p1 = "Paper" ++ (show pId)+ r1 = "Review" ++ (show pId)+ pLabel = newDC (<>) p1 + rLabel = newDC r1 r1 + privs = genPrivTCB (p1 ./\. r1)+ liftReviewDC $ do+ rPaper <- newLIORefP privs pLabel (Paper content)+ rReview <- newLIORefP privs rLabel (Review "")+ return $ ReviewEnt pId rPaper rReview++-- ^ Adda new paper to be reviewed+addPaper :: Content -> ReviewDC Id+addPaper content = do+ reviews <- getReviews+ let pId = 1 + (length reviews)+ ent <- newReviewEnt pId content+ putReviews (ent:reviews)+ return pId+++-- ^ Given a paper number return the paper+retrievePaper :: Id -> ReviewDC (Either ErrorStr Content)+retrievePaper pId = do+ mu <- getCurUser+ case mu of+ Nothing -> return $ Left "Need to be logged in"+ Just u -> do+ mRev <- findReview pId + case mRev of + Nothing -> return $ Left "Invalid Id"+ Just rev -> let as = assignments u+ priv = genPrivTCB (listToLabel $ map id2cat as)+ in doReadPaper priv rev+ where doReadPaper priv rev = liftReviewDC $ do+ (Paper lPaper) <- readLIORefP priv (paper rev)+ return (Right lPaper)+ id2cat i = MkDisj [principal $ "Review"++(show i)]++-- ^ Given a paper number print the paper+-- NOTE: in the paper, the functionality of @readPaper@ corresponds to+-- that of @retrievePaper@; here, we print out the content.+readPaper :: Id -> ReviewDC ()+readPaper i = retrievePaper i >>= \r -> reviewDCPutStrLn $ show r+++-- ^ Given a paper/review number return the review, if the entry exists+retrieveReview :: Id -> ReviewDC (Either ErrorStr Content)+retrieveReview pId = do+ mRev <- findReview pId + case mRev of + Nothing -> return $ Left "Invalid Id"+ Just rev -> do mu <- getCurUser+ case mu of+ Nothing -> return $ Left "Must login first"+ Just u -> doReadReview rev+ where doReadReview rev = liftReviewDC $ do+ (Review r) <- readLIORef (review rev)+ return (Right r)++-- ^ Given a paper/review number print the review, if the entry exists+readReview :: Id -> ReviewDC ()+readReview i = retrieveReview i >>= \r -> reviewDCPutStrLn $ show r++-- ^ Computer the label of the output' channel+getOutputChLbl :: ReviewDC (DCLabel) +getOutputChLbl = do+ mu <- getCurUser+ case mu of+ Nothing -> liftReviewDC $ throwIO (ErrorCall "No user is logged in.")+ Just u -> do+ as <- getReviews >>= return . map paperId -- all reviews+ let cs = conflicts u -- conflicting reviews+ c_cat = map id2conf_cat (cs) -- conflicting categories+ nc_cat = map id2cat (as \\ cs) -- noconflicting categories+ return $ newDC (listToLabel $ c_cat ++ nc_cat) (<>)+ where id2cat i = MkDisj [ principal $ "Review"++(show i)]+ id2conf_cat i = MkDisj [ principal $ "Review" ++ (show i)+ , principal $ "CONFLICT" ]+ +-- ^ Print if the current label flows to the output channel label, i.e.,+-- there is no conflict of interest.+dcPutStrLn :: DCLabel -> Content -> DC ()+dcPutStrLn lo cont = do+ l <- getLabel+ if l `leq` lo+ then dcPutStrLnTCB cont+ else throwIO . ErrorCall $ "Trying to print conflicting review:\n" +++ (prettyShow l) ++ " [/= " ++ (prettyShow lo)++-- ^ Main printing function. Print to a labeled output channel.+reviewDCPutStrLn :: String -> ReviewDC ()+reviewDCPutStrLn s = do + l <- getOutputChLbl+ liftReviewDC $ dcPutStrLn l $ "-> "++ s++reviewDCPutStrLnTCB :: String -> ReviewDC ()+reviewDCPutStrLnTCB = liftReviewDC . dcPutStrLnTCB++-- ^ Given a paper number and review content append to the current review.+appendToReview :: Id -> Content -> ReviewDC (Either ErrorStr ())+appendToReview pId content = do+ mRev <- findReview pId + case mRev of + Nothing -> return $ Left "Invalid Id"+ Just rev -> do privs <- getPrivs+ doWriteReview privs rev content+ return $ Right ()+ where doWriteReview privs rev content = liftReviewDC $ do+ toLabeledP privs ltop $ do+ (Review rs) <- readLIORef (review rev)+ -- restrict writes: + writeLIORef (review rev) (Review (rs++content))++-- ^ Set the current label to the assignments+assign2curLabel :: [Id] -> ReviewDC() +assign2curLabel as = liftReviewDC $ do+ let l = newDC (<>) (listToLabel $ map id2cat as)+ setLabelTCB l+ where id2cat i = MkDisj [principal $ "Review"++(show i)]+ +-- ^ Safely execute untrusted code+safeExecTCB :: ReviewDC () -> ReviewDC ()+safeExecTCB m = do+ s <- get'+ s' <- liftReviewDC $ do+ cc <- getClearance+ cl <- getLabel+ (_, s') <- (runReviewDC m s) `catch` + (\(e::SomeException) -> do+ dcPutStrLnTCB "-> ERROR: IFC violated\n"+ return ((), s))+ lowerClrTCB cc+ setLabelTCB cl+ return s'+ put' s'++-- ^ Execute on behalf of user+asUser :: Name -> ReviewDC a -> ReviewDC ()+asUser n m = do+ putCurUserName n+ mu <- getCurUser+ case mu of+ Nothing -> return ()+ Just u -> do+ reviewDCPutStrLnTCB $ "| Hi, "++ (name u)++".\n| Password>"+ p <- liftReviewDC dcGetLineTCB+ if p /= (password u)+ then reviewDCPutStrLnTCB "| Failed, try again" >> asUser n m+ else do+ reviewDCPutStrLnTCB $ "| Executing on behalf of "++(name u)++"...\n"+ safeExecTCB $ assign2curLabel (assignments u) >> m >> return ()+ clearCurUserName++-- | Given a paper prefix return either an error string, if the paper cannot be+-- found or the paper id.+findPaper :: String -> ReviewDC (Either ErrorStr Id)+findPaper s = do+ revs <- getReviews+ res <- mapM (simpleMatch s) revs >>= return . find isJust+ case res of+ Nothing -> return . Left $ "Could not find paper"+ Just i -> return . Right $ fromJust i+ -- ^ Fing paper by checking for prefix+ where simpleMatch :: String -> ReviewEnt -> ReviewDC (Maybe Id)+ simpleMatch s ent = do+ (Paper pap) <- liftReviewDC $ readLIORefTCB (paper ent)+ if s `isPrefixOf` pap+ then return . Just $ paperId ent+ else return Nothing
Examples/LambdaChair/Main.hs view
@@ -1,17 +1,22 @@-import LIO.TCB-import LIO.DCLabel-import LIO.LIO+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE SafeImports #-}+#else+#warning "This module is not using SafeHaskell"+#endif import LambdaChair import DCLabel.PrettyShow-import DCLabel.Safe +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+import safe AliceCode as Alice+import safe BobCode as Bob+#else import AliceCode as Alice import BobCode as Bob+#endif -printL m = do- (_, l) <- m- putStrLn . prettyShow $ l +main :: IO () main = printL . evalReviewDC $ do addUser "Alice" "password" @@ -29,3 +34,4 @@ addConflict "Bob" p1 asUser "Bob" $ Bob.mainReview+ where printL m = m >>= (putStrLn . prettyShow . snd)
+ Examples/LambdaChair/Safe.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Trustworthy #-}+#else+#warning "This module is not using SafeHaskell"+#endif+module Safe ( module LambdaChair ) where+import LambdaChair ( findPaper+ , retrievePaper, readPaper+ , retrieveReview, readReview+ , appendToReview+ , reviewDCPutStrLn )
LIO/Base.hs view
@@ -1,10 +1,34 @@-{-# OPTIONS_HADDOCK ignore-exports #-}+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Trustworthy #-}+#else+#warning "This module is not using SafeHaskell"+#endif -- |This file exports the subset of symbols in the "LIO.TCB" module -- that are safe for untrusted code to access. See the "LIO.TCB" -- module for documentation.-module LIO.Base (- POrdering(..), POrd(..), o2po, Label(..)++module LIO.Base ( POrdering(..), POrd(..), o2po, Label(..)+ , Priv(..), NoPrivs(..)+ , LIO+ , getLabel, setLabelP+ , getClearance, lowerClr, lowerClrP, withClearance+ , taint, taintP+ , wguard, wguardP, aguard, aguardP+ , Labeled+ , label, labelP+ , unlabel, unlabelP+ , toLabeled, toLabeledP, discard+ , labelOf+ , taintLabeled+ , LabelFault(..)+ , catchP, onExceptionP, bracketP, handleP+ , evaluate+ , evalLIO+ ) where++import LIO.TCB ( POrdering(..), POrd(..), o2po, Label(..) , Priv(..), NoPrivs(..) , LIO , getLabel, setLabelP@@ -21,20 +45,4 @@ , catchP, onExceptionP, bracketP, handleP , evaluate , evalLIO- ) where--import LIO.TCB hiding ( - LIOstate(..)- , runLIO- --- , ShowTCB(..)- , ReadTCB(..)- , labelTCB- , PrivTCB, MintTCB(..)- , showTCB- , unlabelTCB, setLabelTCB, lowerClrTCB- , getTCB, putTCB- , ioTCB, rtioTCB- , rethrowTCB, OnExceptionTCB(..)- , newstate, LIOstate, runLIO )
LIO/DCLabel.hs view
@@ -1,7 +1,14 @@-{-| This module provides bindings for the "DCLabel" module, with some +{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Trustworthy #-}+#else+#warning "This module is not using SafeHaskell"+#endif++{-| This module provides bindings for the @DCLabel@ module, with some renaming to resolve name clashes. The delegation of privilege and other trusted code is not exported by this module and code wishing to-use this should import "DCLabel.TCB".+use this should import @DCLabel.TCB@. -} {-# LANGUAGE StandaloneDeriving #-}@@ -14,11 +21,16 @@ -- * Renamed privileges , DCPriv, DCPrivTCB -- * Useful aliases for the LIO Monad- , DC, evalDC+ , 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@@ -68,42 +80,40 @@ gives us @rs''@). Directly, @rs = rs' /\ rs''@. -} lostar p l g = - let (ls, li) = (secrecy l, integrity l)- (gs, gi) = (secrecy g, integrity g)- lp = DCL.priv p+ 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 $ newDC rs ri+ in DCL.toLNF $ simpleNewLabel p (newDC rs ri) where getCats = DCL.conj . DCL.label c2l = DCL.MkLabel . DCL.MkConj- {- OLD, BROKEN (was more elegant than above, so maybe use some ideas- when rewriting the above):- 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- -}+ simpleNewLabel p lr | p == DCL.rootPrivTCB = g + | p == DCL.noPriv = l `lub` g+ | otherwise = lr -- -- Renaming -- --- | A "DCLabel" category set.+-- | A @DCLabel@ category set. type DCCatSet = DCL.Label--- | A "DCLabel" (untrusted) privilege.+-- | A @DCLabel@ (untrusted) privilege. type DCPriv = DCL.Priv--- | A "DCLabel" privilege.+-- | A @DCLabel@ privilege. type DCPrivTCB = DCL.TCBPriv -- -- LIO aliases --++-- | The type for 'Labeled' values uinsg 'DCLabel' as the label.+type DCLabeled a = Labeled DCLabel a -- | The monad for LIO computations using 'DCLabel' as the label. type DC = LIO DCLabel ()
LIO/Handle.hs view
@@ -1,3 +1,9 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Trustworthy #-}+#else+#warning "This module is not using SafeHaskell"+#endif {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-}@@ -13,7 +19,7 @@ -- -- The actual storage of labeled files is handled by the "LIO.FS" -- module.-module LIO.Handle (DirectoryOps(..)+module LIO.Handle ( DirectoryOps(..) , CloseOps (..) , HandleOps (..) , LHandle@@ -28,12 +34,27 @@ import LIO.TCB import LIO.FS +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)++import safe Prelude hiding (readFile, writeFile)+import qualified Data.ByteString.Lazy as L+#warning "Did not safely import Data.ByteString.Lazy"+import qualified System.Directory as IO+#warning "Did not safely import System.Directory"+import safe System.IO (IOMode)+import safe qualified System.IO as IO+import safe qualified System.IO.Error as IO++#else+ import Prelude hiding (readFile, writeFile) import qualified Data.ByteString.Lazy as L import qualified System.Directory as IO import System.IO (IOMode) import qualified System.IO as IO import qualified System.IO.Error as IO++#endif class (Monad m) => DirectoryOps h m | m -> h where getDirectoryContents :: FilePath -> m [FilePath]
LIO/LIO.hs view
@@ -1,3 +1,10 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Safe #-}+#else+#warning "This module is not using SafeHaskell"+#endif+ {- | This is the main module to be included by code using the Labeled IO (LIO) library. The core of the library is documented in the "LIO.TCB" module. Note, however, that unprivileged code must not@@ -49,19 +56,26 @@ * Define new 'Ix' instances (which could produce out of bounds array references). - In general, pragmas and imports should be highly scrutinized. For- example, most of the "Foreign" class of modules are probably- dangerous. With GHC 7.2, we will use the SafeHaskell extension - to enforce these.+ In general, pragmas and imports should be highly scrutinized.+ For example, most of the "Foreign" class of modules are probably+ dangerous. With GHC 7.2, we use the SafeHaskell extension to enforce+ these. -}-module LIO.LIO (module LIO.Base+module LIO.LIO ( module LIO.Base , module LIO.Handle , module LIO.LIORef , module LIO.MonadLIO ) where +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) -- import Prelude hiding (readFile, writeFile, catch)+import safe LIO.Base+import safe LIO.Handle+import safe LIO.LIORef+import safe LIO.MonadLIO+#else import LIO.Base import LIO.Handle import LIO.LIORef import LIO.MonadLIO+#endif
LIO/LIORef.hs view
@@ -1,3 +1,9 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Safe #-}+#else+#warning "This module is not using SafeHaskell"+#endif -- |This module implements labeled IORefs. The interface is analogous -- to "Data.IORef", but the operations take place in the LIO monad. -- Moreover, reading the LIORef calls taint, while writing it calls@@ -5,4 +11,8 @@ -- "LIORef" module -- trusted code can import "LIO.LIORef.TCB". module LIO.LIORef ( module LIO.LIORef.Safe) where +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+import safe LIO.LIORef.Safe+#else import LIO.LIORef.Safe+#endif
LIO/LIORef/Safe.hs view
@@ -1,9 +1,17 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Trustworthy #-}+#else+#warning "This module is not using SafeHaskell"+#endif+ -- |This module exports the safe subset of the "LIO.LIORef.TCB" module. -- It is important that untrusted code be limited to this subset; information -- flow can easily be violated if the TCB functions are exported. module LIO.LIORef.Safe ( module LIO.LIORef.TCB ) where-import LIO.LIORef.TCB hiding ( newLIORefTCB- , readLIORefTCB- , writeLIORefTCB- , atomicModifyLIORefTCB- )+import LIO.LIORef.TCB ( LIORef+ , newLIORef, labelOfLIORef+ , readLIORef, writeLIORef, atomicModifyLIORef+ , newLIORefP+ , readLIORefP, writeLIORefP, atomicModifyLIORefP+ )
LIO/LIORef/TCB.hs view
@@ -1,3 +1,9 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE SafeImports #-}+#else+#warning "This module is not using SafeHaskell"+#endif -- |This module implements labeled IORefs. The interface is analogous -- to "Data.IORef", but the operations take place in the LIO monad. -- Moreover, reading the LIORef calls taint, while writing it calls@@ -14,8 +20,12 @@ ) where import LIO.TCB++#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+import safe Data.IORef+#else import Data.IORef-import Control.Monad (unless)+#endif data LIORef l a = LIORefTCB l (IORef a)@@ -52,7 +62,7 @@ readLIORef = readLIORefP NoPrivs readLIORefTCB :: (Label l) => LIORef l a -> LIO l s a-readLIORefTCB (LIORefTCB l r) = ioTCB $ readIORef r+readLIORefTCB (LIORefTCB _ r) = ioTCB $ readIORef r -- @@ -65,7 +75,7 @@ writeLIORef = writeLIORefP NoPrivs writeLIORefTCB :: (Label l) => LIORef l a -> a -> LIO l s ()-writeLIORefTCB (LIORefTCB l r) a = ioTCB $ writeIORef r a+writeLIORefTCB (LIORefTCB _ r) a = ioTCB $ writeIORef r a -- @@ -81,5 +91,5 @@ atomicModifyLIORefTCB :: (Label l) => LIORef l a -> (a -> (a, b)) -> LIO l s b-atomicModifyLIORefTCB (LIORefTCB l r) f = ioTCB $ atomicModifyIORef r f+atomicModifyLIORefTCB (LIORefTCB _ r) f = ioTCB $ atomicModifyIORef r f
LIO/MonadCatch.hs view
@@ -1,3 +1,9 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Safe #-}+#else+#warning "This module is not using SafeHaskell"+#endif {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-}@@ -7,9 +13,15 @@ -- Monads. module LIO.MonadCatch (MonadCatch(..), genericBracket) where +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+import safe Prelude hiding (catch)+import safe Control.Exception (Exception, SomeException)+import safe qualified Control.Exception as E+#else import Prelude hiding (catch) import Control.Exception (Exception, SomeException) import qualified Control.Exception as E+#endif -- | @MonadCatch@ is the class used to generalize the standard IO -- @catch@ and @throwIO@ functions to methods that can be defined in
LIO/MonadLIO.hs view
@@ -1,3 +1,9 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE Trustworthy #-}+#else+#warning "This module is not using SafeHaskell"+#endif {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-}@@ -12,7 +18,12 @@ import LIO.TCB +#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+#warning "Did not safely import Control.Monad.Trans" import Control.Monad.Trans (MonadTrans(..))+#else+import Control.Monad.Trans (MonadTrans(..))+#endif class (Monad m, Label l) => MonadLIO m l s | m -> l s where liftLIO :: LIO l s a -> m a
LIO/TCB.hs view
@@ -1,3 +1,9 @@+{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+{-# LANGUAGE SafeImports #-}+#else+#warning "This module is not using SafeHaskell"+#endif {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ExistentialQuantification #-}@@ -80,13 +86,28 @@ , getTCB, putTCB , ioTCB, rtioTCB , rethrowTCB, OnExceptionTCB(..)- -- ** Misc symbols useful for privileged code- , newstate, LIOstate, runLIO+ , newstate -- End TCB exports ) where---import Debug.Trace++#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)+import safe Prelude hiding (catch)+import Control.Monad.Error+#warning "Did not safely import Control.Monad.Error"+import Control.Monad.State.Lazy hiding (put, get)+#warning "Did not safely import Control.Monad.State.Lazy"+import safe Control.Exception hiding (catch, handle, throw, throwIO,+ onException, block, unblock, evaluate)+import safe qualified Control.Exception as E+import safe Data.Monoid+import safe Data.Typeable+import safe Data.Functor+import safe Text.Read (minPrec)++import safe LIO.MonadCatch++#else import Prelude hiding (catch)-import Control.Applicative import Control.Monad.Error import Control.Monad.State.Lazy hiding (put, get) import Control.Exception hiding (catch, handle, throw, throwIO,@@ -94,10 +115,13 @@ import qualified Control.Exception as E import Data.Monoid import Data.Typeable+import Data.Functor import Text.Read (minPrec) import LIO.MonadCatch +#endif+ -- -- We need a partial order and a Label --@@ -217,6 +241,11 @@ -- | @Labeled@ is a type representing labeled data. data (Label l) => Labeled l t = LabeledTCB l t++-- | To make programming easier with labeled values, we provide a functor+-- instance definition.+instance Label l => Functor (Labeled l) where+ fmap f (LabeledTCB l a) = LabeledTCB l (f a) -- | It would be a security issue to make certain objects a member of -- the 'Show' class, but nonetheless it is useful to be able to
lio.cabal view
@@ -1,16 +1,21 @@ Name: lio-Version: 0.0.1-Cabal-Version: >= 1.6+Version: 0.0.2 build-type: Simple License: GPL License-File: LICENSE Author: HAILS team+Maintainer: Deian Stefan <deian at cs dot stanford dot edu> Stability: experimental-Maintainer: http://www.scs.stanford.edu/~dm/addr/+Synopsis: Labeled IO Information Flow Control Library Category: Security-Synopsis: Labeled IO library+Cabal-Version: >= 1.6+ Extra-source-files:- Examples/LambdaChair/Main.hs+ Examples/LambdaChair/AliceCode.hs+ Examples/LambdaChair/BobCode.hs+ Examples/LambdaChair/LambdaChair.hs+ Examples/LambdaChair/Main.hs+ Examples/LambdaChair/Safe.hs Description: The /Labeled IO/ (LIO) library provides information flow@@ -28,10 +33,6 @@ is available here: <http://www.scs.stanford.edu/~deian/pubs/stefan:2011:flexible-ext.pdf>. - To obtain the latest experimental source code, run:-- @git clone http:\/\/www.scs.stanford.edu\/~deian\/lio.git@.- The library depends on the @DCLabel@ module. You can read more on DC Labels here: <http://www.scs.stanford.edu/~deian/dclabels/>.@@ -54,6 +55,7 @@ time >= 1.1.4 && < 2, dclabel >= 0.0.1 && < 2 + ghc-options: -Wall Exposed-modules: LIO.Armor, LIO.Base,@@ -69,14 +71,3 @@ LIO.MonadLIO, LIO.TCB, LIO.TmpFile-- Extensions:- DeriveDataTypeable,- ExistentialQuantification,- FlexibleContexts,- FlexibleInstances,- ForeignFunctionInterface,- FunctionalDependencies,- GeneralizedNewtypeDeriving,- MultiParamTypeClasses,- ScopedTypeVariables