diff --git a/LIO/Labeled.hs b/LIO/Labeled.hs --- a/LIO/Labeled.hs +++ b/LIO/Labeled.hs @@ -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 = +-- +-- Note that the current label is 'bottom' (which in DCLabels is +-- @@), 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 diff --git a/examples/LambdaChair/AliceCode.hs b/examples/LambdaChair/AliceCode.hs new file mode 100644 --- /dev/null +++ b/examples/LambdaChair/AliceCode.hs @@ -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?" diff --git a/examples/LambdaChair/BobCode.hs b/examples/LambdaChair/BobCode.hs new file mode 100644 --- /dev/null +++ b/examples/LambdaChair/BobCode.hs @@ -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 diff --git a/examples/LambdaChair/LambdaChair.hs b/examples/LambdaChair/LambdaChair.hs new file mode 100644 --- /dev/null +++ b/examples/LambdaChair/LambdaChair.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE Trustworthy #-} +{- | + +Safe version of "LambdaChair.TCB". + +-} + +module LambdaChair ( + findPaper + , retrievePaper, readPaper + , retrieveReview, readReview + , appendToReview + , reviewDCPutStrLn + ) where +import LambdaChair.TCB diff --git a/examples/LambdaChair/LambdaChair/TCB.hs b/examples/LambdaChair/LambdaChair/TCB.hs new file mode 100644 --- /dev/null +++ b/examples/LambdaChair/LambdaChair/TCB.hs @@ -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 diff --git a/examples/LambdaChair/Main.hs b/examples/LambdaChair/Main.hs new file mode 100644 --- /dev/null +++ b/examples/LambdaChair/Main.hs @@ -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) diff --git a/lio.cabal b/lio.cabal --- a/lio.cabal +++ b/lio.cabal @@ -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 +Author: Hails team +Maintainer: Hails team 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