lio 0.9.0.0 → 0.9.0.1
raw patch · 7 files changed
+749/−16 lines, 7 filesdep ~bytestringdep ~cerealdep ~containersPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: bytestring, cereal, containers, directory, filepath, transformers, xattr, zlib
API changes (from Hackage documentation)
Files
- LIO/Labeled.hs +185/−1
- examples/LambdaChair/AliceCode.hs +22/−0
- examples/LambdaChair/BobCode.hs +17/−0
- examples/LambdaChair/LambdaChair.hs +15/−0
- examples/LambdaChair/LambdaChair/TCB.hs +445/−0
- examples/LambdaChair/Main.hs +32/−0
- lio.cabal +33/−15
LIO/Labeled.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE Trustworthy #-}-{-# LANGUAGE ConstraintKinds,+{-# LANGUAGE CPP,+ ConstraintKinds, FlexibleContexts #-} {- |@@ -37,14 +38,25 @@ -- * Labeled functor -- $functor , LabeledFunctor(..)+#ifdef TO_LABELED+ -- * Executing sensitive computation+ -- $toLabeled+ , toLabeled, toLabeledP+ , discard, discardP+#endif ) where +import LIO.TCB import LIO.Label import LIO.Core import LIO.Privs import LIO.Labeled.TCB import Control.Monad +#ifdef TO_LABELED+import qualified Control.Exception as E+#endif+ -- | Returns label of a 'Labeled' type. instance LabelOf Labeled where labelOf = labelOfLabeled@@ -175,6 +187,7 @@ created value is in the 'LIO' monad and secondly each label format implementation must produce their own definition of 'lFmap' such that the end label protects the computation result accordingly.+ -} -- | IFC-aware functor instance. Since certain label formats may contain@@ -185,3 +198,174 @@ -- | 'fmap'-like funciton that is aware of the current label and -- clearance. lFmap :: MonadLIO l m => Labeled l a -> (a -> b) -> m (Labeled l b)++#ifdef TO_LABELED++{- $toLabeled++LIO provides a means for executing a sensitive computation without+raising the current label. This is done with the function 'toLabeled'.+The semantics of the function is as follows:++1. Execute whatever action is supplied. This action may raise the+current label or lower the current clearance.++2. Take the result of the computation and wrap it in a 'Labeled'+value. The label of the value is provided as an argument to+'toLabeled'. Hence, the computation should not observe anything more+sensitive than this.++3. Restore the current label and clearance to that of step 1. Return+the 'Labeled' value created in step 2, if the end current label is not+above the value's label. Otherwise raise an exception to indicate that+the computation read data more sensitive than the set bound.++Note that if the executed computation raises an exception, 'toLabeled'+hides the exception -- this exception is only propagated when the+'Labeled' value is 'unlabel'ed.++NOTE:+As indicated by the warnings, 'toLabeled' is not safe with respect to+/termination sensitive non-interference/. This means that a malicious+computation can carry out an attack that leaks information by not+terminating in a 'toLabeled' block. Similarly an attacker can leverage+timing to do the same. Your version of LIO has been compiled with the+@toLabeled@ flag, and thus susceptible to such attacks. If this was+not by choice, recompile the package (by default, 'toLabeled' is not+included) and use the primitives in "LIO.Concurrent" to implement a+similarly-behaving program.++-}++-- | @toLabeled@ is the dual of 'unlabel'. It allows one to invoke+-- computations that would raise the current label, but without+-- actually raising the label. Instead, the result of the+-- computation is packaged into a 'Labeled' with a supplied+-- label. (Of couse, the computation executed by @toLabeled@ must+-- most observe any data whose label exceeds the supplied label.)+--+-- To get at the result of the computation one will have to call+-- 'unlabel' and raise the label, but this can be postponed, or+-- done inside some other call to 'toLabeled'. This suggests that+-- the provided label must be above the current label and below+-- the current clearance. --+-- Note that @toLabeled@ always restores the clearance to whatever+-- it was when it was invoked, regardless of what occurred in the+-- computation producing the value of the 'Labeled'. This highlights+-- one main use of clearance: to ensure that a @Labeled@ computed+-- does not exceed a particular label.+--+-- If an exception is thrown within a @toLabeled@ block, such that+-- the outer context is withing a 'catch', which is further within+-- a @toLabeled@ block, infromation can be leaked. Consider the+-- following program that uses 'DCLabel's. (Note that 'discard' is+-- simply @toLabeled@ that throws throws the result away.)+--+-- > main = evalDC' $ do+-- > lRef <- newLIORef bottom ""+-- > hRef <- newLIORef top "secret"+-- > -- brute force:+-- > forM_ ["fun", "secret"] $ \guess -> do+-- > stash <- readLIORef lRef+-- > writeLIORef lRef $ stash ++ "\n" ++ guess ++ ":"+-- > discard top $ do+-- > catch ( discard top $ do+-- > secret <- readLIORef hRef+-- > when (secret == guess) $ throwIO . userError $ "got it!"+-- > ) (\(e :: IOError) -> return ())+-- > l <- getLabel+-- > when (l == bottom) $ do stash <- readLIORef lRef+-- > writeLIORef lRef $ stash ++ "no!"+-- > readLIORef lRef+-- > where evalDC' act = do (r,l) <- runDC act+-- > putStrLn r+-- > putStrLn $ "label = " ++ prettyShow l+--+-- The output of the program is:+--+-- > $ ./new+-- >+-- > fun:no!+-- > secret:+-- > label = <True , False>+--+-- Note that the current label is 'bottom' (which in DCLabels is+-- @<True , False>@), and the secret is leaked. The fundamental issue+-- is that the outer 'discard' allows for the current label to remain+-- low even though the 'catch' raised the current label when the+-- secret was found (and thus exception was throw). As a consequence,+-- 'toLabeled' catches all exceptions, and returns a 'Labeled'+-- value that may have a labeled exception as wrapped by @throw@.+-- All exceptions within the outer computation, including+-- IFC violation attempts, are essentially rethrown when performing+-- an 'unlabel'.+--+toLabeled :: Label l+ => l -- ^ Label of result and upper bound on+ -- inner-computations' observation+ -> LIO l a -- ^ Inner computation+ -> LIO l (Labeled l a)+toLabeled = toLabeledP NoPrivs+{-# WARNING toLabeled "toLabeled is susceptible to termination attacks" #-}++-- | Same as 'toLabeled' but allows one to supply a privilege object+-- when comparing the initial and final label of the computation.+--+toLabeledP :: Priv l p+ => p -> l -> LIO l a -> LIO l (Labeled l a)+toLabeledP p l act = do+ -- Check that the supplied upper bound is bounded+ guardAllocP p l+ -- Get current state:+ save_s <- getLIOStateTCB+ -- Execute action, catching any exceptions:+ res <- (liftM Right act) `catchTCB` (return . Left . lubErr l)+ -- Get the new state:+ s <- getLIOStateTCB+ let lastL = lioLabel s+ -- Restore state+ putLIOStateTCB save_s+ return . labelTCB l $+ if canFlowToP p lastL l+ -- If the result was an exception, rethrow it when unlabel+ -- otherwise just return the result+ then either E.throw id res+ -- Violated the upper bound:+ else let l1 = lastL `upperBound` l+ -- Join of exception label (if any) and l1+ l2 = either (upperBound l1 . getErrLabel) (const l1) res+ -- Throw pure exception with label l1+ in E.throw $ LabeledExceptionTCB l2 $ E.toException $ + VMonitorFailure { monitorFailure = CanFlowToViolation+ , monitorMessage = errMsg }+ where lubErr lnew (LabeledExceptionTCB le e) =+ LabeledExceptionTCB (le `lub` lnew) e+ --+ getErrLabel (LabeledExceptionTCB le _) = le+ --+ errMsg = "Computation read data more sensitive than bound."+{-# WARNING toLabeledP "toLabeledP is susceptible to termination attacks" #-}+++-- | Executes a computation that would raise the current label, but+-- discards the result so as to keep the label the same. Used when+-- one only cares about the side effects of a computation. For+-- instance, if @log_handle@ is an 'LHandle' with a high label, one+-- can execute+--+-- @+-- discard top $ 'hputStrLn' log_handle \"Log message\"+-- @+--+-- to create a log message without affecting the current label.+--+discard :: Label l => l -> LIO l a -> LIO l ()+discard = discardP NoPrivs+{-# WARNING discard "discard is susceptible to termination attacks" #-}++-- | Same as 'discard', but uses privileges when comparing initial and+-- final label of the computation.+discardP :: Priv l p => p -> l -> LIO l a -> LIO l ()+discardP p l act = void $ toLabeledP p l act+{-# WARNING discardP "discardP is susceptible to termination attacks" #-}+#endif
+ examples/LambdaChair/AliceCode.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE Safe #-}+module AliceCode ( mainReview ) where++import LambdaChair++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,17 @@+{-# LANGUAGE Safe #-}+module BobCode ( mainReview ) where++import LambdaChair++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,15 @@+{-# LANGUAGE Trustworthy #-}+{- | ++Safe version of "LambdaChair.TCB".++-}++module LambdaChair ( + findPaper+ , retrievePaper, readPaper+ , retrieveReview, readReview+ , appendToReview+ , reviewDCPutStrLn+ ) where+import LambdaChair.TCB
+ examples/LambdaChair/LambdaChair/TCB.hs view
@@ -0,0 +1,445 @@+{-# LANGUAGE Unsafe #-}+{-# LANGUAGE OverloadedStrings,+ MultiParamTypeClasses,+ GeneralizedNewtypeDeriving,+ ScopedTypeVariables #-}++{- | ++Basic review system API.++Must compile LIO with @--flags="toLabeled"@.++This is a prototype/toy implementation. A more serious implementation+will be implemented using the Hails framework.++-}++module LambdaChair.TCB (+ --- * Admin actions+ runReviewDC+ , emptyReviewState+ , addUser+ , addPaper+ , addConflict+ , addAssignment+ , asUser+ --- * User actions+ , 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.Trans.Class+import Control.Monad.Trans.State+import Data.Maybe+import Data.List++import LIO+import LIO.TCB+import LIO.Privs.TCB+import LIO.LIORef+import LIO.LIORef.TCB (readLIORefTCB)+import LIO.DCLabel+import LIO.DCLabel.Privs.TCB++import qualified Data.ByteString.Char8 as C+++type ErrorStr = String++-- | Class with sideffectful show+class DCShowTCB s where+ dcShowTCB :: s -> DC String++-- | Print to standard output+dcPutStrLnTCB :: String -> DC ()+dcPutStrLnTCB = ioTCB . putStrLn++-- | Read from standard input+dcGetLineTCB :: DC String+dcGetLineTCB = ioTCB getLine++-- | A name+type Name = String+-- | A password+type Password = String+-- | Paper/Rewview content+type Content = String+-- | A review log+type ReviewLog = String++-- | Paper id+type Id = Int+-- | A paper is just a wrapper for its contents+data Paper = Paper Content+-- | A review is just a wrapper for its contents+data Review = Review ReviewLog++-- | A user contains a name, password a list of conflicting papers and+-- list of papers to review (i.e., assignments).+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)++-- | Areview entry contains the paper id, paper contents and review+-- log.+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+++-- Internal state of the 'ReviewDC' monad.+data ReviewState = ReviewState { users :: [User]+ , reviewEntries :: [ReviewEnt]+ , curUser :: Maybe Name }++-- | Emtpy state.+emptyReviewState :: ReviewState+emptyReviewState = ReviewState [] [] Nothing++-- | Monad in which all review actions are executed.+newtype ReviewDC a = ReviewDC (StateT ReviewState DC a)+ deriving (Monad)++-- | Lift a 'DC' into thew 'ReviewDC' monad.+instance MonadLIO DCLabel ReviewDC where+ liftLIO = ReviewDC . lift++-- | Get internal state+get' :: ReviewDC ReviewState+get' = ReviewDC . StateT $ \s -> return (s,s)++-- | Update internal state+put' :: ReviewState -> ReviewDC ()+put' s = ReviewDC . StateT $ \_ -> return ((),s)++-- | Execute a review action+runReviewDC :: ReviewDC a -> ReviewState -> DC (a, ReviewState)+runReviewDC (ReviewDC m) s = runStateT m s++--++-- | Get all users+getUsers :: ReviewDC [User]+getUsers = users `liftM` get'++-- | Get all review entries+getReviews :: ReviewDC [ReviewEnt]+getReviews = reviewEntries `liftM` get'++-- | Get priviliges+getCurUserName :: ReviewDC (Maybe Name)+getCurUserName = curUser `liftM` get'++-- | Get current user name+getCurUser :: ReviewDC (Maybe User)+getCurUser = do+ n <- getCurUserName+ maybe (return Nothing) findUser n++-- | Get priviliges of the user executing the action+getPrivs :: ReviewDC DCPriv+getPrivs = do + u <- getCurUser+ return $ maybe noPriv (mintTCB . dcPrivDesc . name) u++-- | Updat users+putUsers :: [User] -> ReviewDC ()+putUsers us = do+ rs <- getReviews+ u <- getCurUserName+ put' $ ReviewState us rs u++-- | Update reviews+putReviews :: [ReviewEnt] -> ReviewDC ()+putReviews rs = do+ us <- getUsers+ u <- getCurUserName+ put' $ ReviewState us rs u++-- | Set current user+putCurUserName :: Name -> ReviewDC ()+putCurUserName u = do+ us <- getUsers+ rs <- getReviews+ put' $ ReviewState us rs (Just u)++-- | Remove current user+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+ us <- getUsers+ return $ find (\u -> name u == n) us++-- | 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+ us <- getUsers+ mapM (liftLIO . dcShowTCB) us >>=+ reviewDCPutStrLnTCB . (intercalate "\n--\n")++-- ^ Print papers and reviews+printReviewsTCB :: ReviewDC ()+printReviewsTCB = do+ reviews <- getReviews+ mapM (liftLIO . dcShowTCB) reviews >>=+ reviewDCPutStrLnTCB . (intercalate "\n--\n")++-- ^ Create new paper given id and content+newReviewEnt :: Id -> Content -> ReviewDC ReviewEnt+newReviewEnt pId content = do+ let p1 = toComponent $ "Paper" ++ (show pId)+ r1 = toComponent $ "Review" ++ (show pId)+ pLabel = dcLabel dcTrue p1 + rLabel = dcLabel r1 r1 + privs = mintTCB $ dcPrivDesc (p1 /\ r1)+ liftLIO $ 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 = mintTCB . fromList $ map id2cat as+ in doReadPaper priv rev+ where doReadPaper priv rev = liftLIO $ do+ (Paper lPaper) <- readLIORefP priv (paper rev)+ return (Right lPaper)+ id2cat i = [principal . C.pack $ "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 _ -> doReadReview rev+ where doReadReview rev = liftLIO $ 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 -> liftLIO $ throwLIO (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 $ dcLabel (fromList $ c_cat ++ nc_cat) dcTrue+ where id2cat i = [ principal . C.pack $ "Review"++(show i)]+ id2conf_cat i = [ principal . C.pack $ "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 `canFlowTo` lo+ then dcPutStrLnTCB cont+ else throwLIO . ErrorCall $ "Trying to print conflicting review:\n" +++ (show l) ++ " [/= " ++ (show lo)++-- ^ Main printing function. Print to a labeled output channel.+reviewDCPutStrLn :: String -> ReviewDC ()+reviewDCPutStrLn s = do + l <- getOutputChLbl+ liftLIO $ dcPutStrLn l $ "-> "++ s++-- | Print line to standard output+reviewDCPutStrLnTCB :: String -> ReviewDC ()+reviewDCPutStrLnTCB = liftLIO . 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+ return $ Right ()+ where doWriteReview privs rev = liftLIO $ do+ toLabeledP privs top $ 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 = liftLIO $ do+ let l = dcLabel dcTrue (fromList $ map id2cat as)+ setLabelP allPrivTCB l+ where id2cat i = [principal . C.pack $ "Review"++(show i)]+ +-- ^ Safely execute untrusted code+safeExecTCB :: ReviewDC () -> ReviewDC ()+safeExecTCB m = do+ s <- get'+ s' <- liftLIO $ do+ cc <- getClearance+ cl <- getLabel+ (_, s') <- (runReviewDC m s) `catchLIO` + (\(_::SomeException) -> do+ dcPutStrLnTCB "-> ERROR: IFC violated\n"+ return ((), s))+ setClearanceP allPrivTCB cc+ setLabelP allPrivTCB 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 <- liftLIO 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 m ent = do+ (Paper pap) <- liftLIO $ readLIORefTCB (paper ent)+ if m `isPrefixOf` pap+ then return . Just $ paperId ent+ else return Nothing
+ examples/LambdaChair/Main.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE Unsafe #-}++module Main (main) where++import LIO.DCLabel+import LambdaChair.TCB++import safe AliceCode as Alice+import safe BobCode as Bob+++main :: IO ()+main = printL . runReviewDC' $ do+ addUser "Alice" "password"+ + p1 <- addPaper "Flexible Dynamic..."+ p2 <- addPaper "A Static..."+ + addAssignment "Alice" p1+ addAssignment "Alice" p2+ + asUser "Alice" $ Alice.mainReview+ + addUser "Bob" "password"+ + addAssignment "Bob" p2+ addConflict "Bob" p1++ asUser "Bob" $ Bob.mainReview+ where printL m = m >>= (putStrLn . show . snd)+ runReviewDC' act = + runDC $ runReviewDC act (emptyReviewState)
lio.cabal view
@@ -1,11 +1,11 @@ Name: lio-Version: 0.9.0.0+Version: 0.9.0.1 Cabal-Version: >= 1.8 Build-type: Simple License: GPL License-File: LICENSE-Author: HAILS team-Maintainer: HAILS team <hails at scs dot stanford dot edu>+Author: Hails team+Maintainer: Hails team <hails at scs dot stanford dot edu> Synopsis: Labeled IO Information Flow Control Library Category: Security Description:@@ -52,23 +52,41 @@ examples/gate.hs examples/waitAndCatch.hs examples/fsExample.hs+ examples/LambdaChair/LambdaChair.hs+ examples/LambdaChair/LambdaChair/TCB.hs+ examples/LambdaChair/AliceCode.hs+ examples/LambdaChair/BobCode.hs+ examples/LambdaChair/Main.hs ++Source-repository head+ Type: git+ Location: http://www.gitstar.com/scs/lio.git++Flag toLabeled+ Description:+ Enable toLabeled primitive. This is NOT+ termination-sensitive non-interferant so use with care.+ Default: False+ Library Build-Depends:- base >= 4.5 && < 5.0,- transformers >= 0.2.2 && < 1.0,- containers >= 0.4.2.1 && < 0.5,- bytestring >= 0.9.2.1 && < 1.0,- cereal >= 0.3.5.1 && < 0.4,- filepath >= 1.3.0.0 && < 1.4,- directory >= 1.1.0.2 && < 1.2,- xattr >= 0.6.1 && < 1.0,- zlib >= 0.5.3.1 && < 0.6,- SHA >= 1.5.0.0 && < 1.6,- time >= 1.2.0.5 && < 1.5+ base >= 4.5 && < 5.0+ ,transformers >= 0.2.2+ ,containers >= 0.4.2+ ,bytestring >= 0.9+ ,cereal >= 0.3.5.1+ ,filepath >= 1.3.0.0+ ,directory >= 1.1.0.2+ ,xattr >= 0.6.1+ ,zlib >= 0.5.3.1+ ,SHA >= 1.5.0.0 && < 1.6+ ,time >= 1.2.0.5 && < 1.5 + GHC-options: -Wall -fno-warn-orphans - Ghc-options: -Wall -fno-warn-orphans+ if flag(toLabeled)+ CPP-options: -DTO_LABELED Exposed-modules: -- * Top-level exporter