lio-eci11 (empty) → 0.1
raw patch · 16 files changed
+2512/−0 lines, 16 filesdep +SHAdep +arraydep +basesetup-changed
Dependencies added: SHA, array, base, bytestring, containers, dclabel-eci11, directory, filepath, mtl, old-time, time, unix
Files
- Examples/LambdaChair/Main.hs +23/−0
- LICENSE +17/−0
- LIO/Armor.hs +71/−0
- LIO/Base.hs +40/−0
- LIO/DCLabel.hs +84/−0
- LIO/FS.hs +583/−0
- LIO/Handle.hs +200/−0
- LIO/HiStar.hs +151/−0
- LIO/LIO.hs +67/−0
- LIO/LIORef.hs +85/−0
- LIO/MonadCatch.hs +47/−0
- LIO/MonadLIO.hs +26/−0
- LIO/TCB.hs +894/−0
- LIO/TmpFile.hs +146/−0
- Setup.hs +3/−0
- lio-eci11.cabal +75/−0
+ Examples/LambdaChair/Main.hs view
@@ -0,0 +1,23 @@+import LIO.LIO+import LambdaChair++import AliceCode as Alice+import BobCode as Bob++main = evalReviewDC $ 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
+ LICENSE view
@@ -0,0 +1,17 @@+This program is free software; you can redistribute it and/or+modify it under the terms of the GNU General Public License as+published by the Free Software Foundation; either version 2, or (at+your option) any later version.++This program is distributed in the hope that it will be useful, but+WITHOUT ANY WARRANTY; without even the implied warranty of+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU+General Public License for more details.++You can obtain copies of permitted licenses from these URLs:++ http://www.gnu.org/licenses/old-licenses/gpl-2.0.txt+ http://www.gnu.org/licenses/gpl-3.0.txt++or by writing to the Free Software Foundation, Inc., 59 Temple Place,+Suite 330, Boston, MA 02111-1307 USA
+ LIO/Armor.hs view
@@ -0,0 +1,71 @@+-- | These functions support a simple base-32 encoding of binary data,+-- in which 5 bytes of binary data are mapped onto 8 characters from+-- the set {a, ..., k, m, n, p, ..., z, 2, ..., 9} (i.e., all+-- lower-case letters and digits except for l, o, 0, and 9).+--+-- The 'armor32' function encodes binary using this base-32 encoding,+-- while 'dearmor32' reverses the encoding.+--+-- Binary data is assumed to come from the "Data.ByteString.Lazy" type.+module LIO.Armor (armor32, dearmor32, a2b, b2a, a32Valid) where++import Control.Monad+import Data.Array.Unboxed+import Data.Bits+import qualified Data.ByteString.Lazy as L+-- import qualified Data.ByteString.Lazy.Char8 as LC+import Data.Char+import Data.Word++a2b :: UArray Word8 Char+a2b = listArray (0, 31) $ do c <- ['a'..'z'] ++ ['0' .. '9']+ guard $ not $ elem c "lo01"+ return c++armor32 :: L.ByteString -> String+armor32 str = doit 0 $ L.unpack str+ where+ doit _ [] = []+ doit skip s@(c1:s1) =+ let hi = shift c1 (skip - 3) .&. 0x1f+ lo = if skip <= 3 || s1 == []+ then 0+ else shift (head s1) (skip - 11)+ c = a2b ! (hi .|. lo)+ in if skip >= 3+ then c : doit (skip - 3) s1+ else c : doit (skip + 5) s++inval :: Word8+inval = -1+b2a :: UArray Char Word8+b2a = accumArray (\_ b -> b) inval (chr 0, chr 255)+ $ [(y, x) | (x, y) <- assocs a2b]+ -- ++ [(toUpper y, x) | (x, y) <- assocs a2b]++dearmor32 :: String -> L.ByteString+dearmor32 str = doit 0 0 str+ where+ doit _ _ [] = L.empty+ doit carryVal carrySize (c1:s) =+ let v = b2a ! c1+ in if v == inval+ then L.empty+ else let needbits = 8 - carrySize+ nextCarrySize = 5 - needbits+ b = carryVal .|. (shift v (negate nextCarrySize))+ nextCarry = shift v (8 - nextCarrySize)+ in if nextCarrySize < 0+ then doit b (nextCarrySize + 8) s+ else L.cons b $ doit nextCarry nextCarrySize s++-- | Return 'True' iff the caracter could have been in the output of+-- 'armor32'.+a32Valid :: Char -> Bool+a32Valid c = b2a ! c /= inval ++{-+mask n = complement $ shift (fromInteger $ -1) n+pack s = LC.pack s+-}+
+ LIO/Base.hs view
@@ -0,0 +1,40 @@+{-# OPTIONS_HADDOCK ignore-exports #-}++-- |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(..)+ , 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 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
@@ -0,0 +1,84 @@+{-| 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".+-}++{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE DeriveDataTypeable #-}+module LIO.DCLabel ( -- * DCLabel export+ module DCLabel.Safe+ , DCCatSet+ -- * Renamed privileges+ , DCPriv, DCPrivTCB+ -- * Useful aliases for the LIO Monad+ , 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++--+-- Renaming+--++-- | A "DCLabel" category set.+type DCCatSet = DCL.Label+-- | A "DCLabel" (untrusted) privilege.+type DCPriv = DCL.Priv+-- | A "DCLabel" privilege.+type DCPrivTCB = DCL.TCBPriv+++--+-- LIO aliases+--++-- | The monad for LIO computations using 'DCLabel' as the label.+type DC = LIO DCLabel ()++-- | Runs a computation in the LIO Monad, returning both the+-- computation's result and the label of the result.+evalDC :: DC a -> IO (a, DCLabel)+evalDC m = evalLIO m ()
+ LIO/FS.hs view
@@ -0,0 +1,583 @@+{-# LANGUAGE DeriveDataTypeable #-}++{- |This module manages a file store in which a label is associated+ with every file and directory. The file store is grouped into+ directories by label. Files are stored under names like:++ > LabelHash/OpaqueName++ where LabelHash is a SHA-224 hash of the label, and OpaqueName is+ either a regular file (containing contents) or a directory+ populated exclusively by symbolic links pointing back into+ LabelHash directories. Each LabelHash directory also has a file+ called++ > LabelHash/LABEL++ which actually contains the label of all the files in that directory.++ There is also a symbolic link @root@, pointing to the root+ directory. For efficiency, @LabelHash@ actually consists of+ multiple directories.++ There are two externally-visible abstractions. The first is+ 'Name', which refers to a file name in a user directory, of the+ form:++ > LabelHash/OpaqueName/UserName++ There is also a special 'Name', 'rootDir', which refers to the+ root directory. Untrusted user code has access to the 'rootDir'+ 'Name', and can walk the tree from there using the 'lookupName'+ function. The "LIO.Handle" module contains functions 'mkDir' and+ 'mkLHandle' which permit untrusted code to make new 'Name's as+ well as to do handle-based IO on protected files.++ The second is 'Node', which refers to one of the @OpaqueName@s+ that 'Name's point to. Currently, any functions that operate on+ 'Node's are in the IO Monad so as not to be executable by+ untrusted code. This is important because in order to use a file,+ someone must have the right to know know that the file exists, and+ this requires read permission on the file's 'Name'. It would be+ insecure if untrusted code could execute openNode in the LIO+ Monad.++ Note that if a machine crashes, the code in this module could+ leave the filesystem in an inconsistent state. However, the code+ tries to maitain the invariant that any inconsistencies will+ either be:++ 1. temporary files or directories whose names end with the+ \"@~@\" character, or++ 2. dangling symbolic links.++ Both of these inconsistencies can be checked and cleaned up+ locally without examining the whole file system. The code tries+ to fix up these inconsistencies on-the-fly as it encounters them.+ However, it could possibly lieave some stranded temporary+ @LABEL...~@ files. You could also end up with some weirdness like+ a file that shows up in getDirectoryContents, but that you can't+ open for reading.++ To keep from having to examine the whole file system to fix+ errors, the code tries to maintain the invariant that if a+ 'Node'\'s file name doesn't end with @~@, then there must be a+ link pointing to it somewhere. This is why the code uses a+ separate 'NewNode' type to represent a 'Node' whose name ends @~@.+ The function 'linkNode' renames the 'NewNode' to a name without a+ trailing @~@ only after creating a 'Name' that points to the+ permenent 'Node' path.++ Assuming a file system that preserves the order of metadata+ operations, the code should mostly be okay to recover from any+ crashes. If using soft updates, which can re-order metadata+ operations, you could end up with symbolic links that point+ nowhere.++ In the worst case scenario if inconsistencies develop, you can+ manually fix up the file system by deleting all danglinng symbolic+ links and all files and directories ending @~@. Make sure no+ application is concurrently accessing the file system, however.++-}++module LIO.FS ( -- * The opaque name object+ Name -- Do not Export constructor! Names are TRUSTED+ , rootDir+ , getRootDir, mkRootDir+ , lookupName, mkTmpDirL+ -- * Initializing the file system+ , initFS+ -- * Internal data structures+ , Node+ -- * Helper functions in the IO Monad+ , labelOfName, labelOfNode, nodeOfName+ , mkNode, mkNodeDir, mkNodeReg, linkNode+ , lookupNode, openNode, getDirectoryContentsNode+ -- * Misc. utility functions+ , tryPred+ ) where++import LIO.Armor+import LIO.TCB+import LIO.TmpFile++import Prelude hiding (catch)++import Control.Exception hiding (throwIO, catch, onException)+import Control.Monad+import qualified Data.ByteString.Lazy.Char8 as LC+import Data.Typeable+-- import qualified GHC+import qualified GHC.IO.Exception as GHC (IOErrorType(..))+import System.Directory+import System.FilePath+import System.IO+import System.IO.Error hiding (catch, try)+-- import System.FilePath+import System.Posix.Files+import System.Posix.Process++import Data.Digest.Pure.SHA+++--+-- Utility functions+--++strictReadFile :: FilePath -> IO LC.ByteString+strictReadFile f = withFile f ReadMode readit+ where readit h = do+ size <- hFileSize h+ LC.hGet h $ fromInteger size++catchIO :: IO a -> IO a -> IO a+catchIO a h = catch a ((const :: a -> IOException -> a) h)++catchPred :: Exception e => (e -> Bool) -> IO a -> IO a -> IO a+catchPred predicate a h = catchJust test a runh+ where+ test e = if predicate e then Just () else Nothing+ runh () = h++tryPred :: Exception e => (e -> Bool) -> IO a -> IO (Either e a)+tryPred predicate a = tryJust test a+ where+ test e = if predicate e then Just e else Nothing++ignoreErr :: IO () -> IO ()+ignoreErr m = catch m ((\_ -> return ()) :: IOException -> IO ())++-- |Delete a name whether it's a file or directory, by trying both.+-- This is slow, but only used for error conditions when performance+-- shouldn't matter.+clean :: FilePath -> IO ()+clean path =+ removeFile path `catchIO` (removeDirectory path `catchIO` return ())++--+-- Exceptions thrown by this module+--++data FSErr+ = FSCorruptLabel FilePath -- ^ File Containing Label is Corrupt+ deriving (Show, Typeable)+instance Exception FSErr++--+-- LDir functions+--++prefix :: FilePath+prefix = "ls"++-- | File name in which labels are stored in 'LDir's.+labelFile :: FilePath+labelFile = "LABEL"++-- | File name of root directory for each label+rootFile :: FilePath+rootFile = "ROOT"++-- | Type containing the pathname of a @LabelHash@ directory (which+-- must contain a file named 'labelFile').+newtype LDir = LDir FilePath deriving (Show)++-- | The subdirectory depth of 'LDir's. Because many file systems+-- have linear lookup time in large directories, it is better to use+-- the first few characters of the hash of a label as subdirectories.+-- Putting all hash values into one huge directory would get slow.+lDirNdirs :: Int+lDirNdirs = 3++-- | Hash a label down to the directory storing all 'Node's with that+-- label.+lDirOfLabel :: (Label l) => l -> LDir+lDirOfLabel l =+ LDir $ doit lDirNdirs prefix hash+ where+ hash = armor32 $ bytestringDigest $ sha224 $ LC.pack $ show l+ doit 0 out h = out </> h+ doit n out (c:h) = doit (n - 1) (out </> [c]) h+ doit _ _ _ = error "lDirOfLabel bad sha"++{-+-- | Minimally validate that an LDir is in the right part of the file+-- system, or throw 'FSIllegalPath'.+checkLDir :: LDir -> IO ()+checkLDir (LDir path) = do+ dirlist <- liftM splitDirectories $ checkpref path+ unless (length dirlist == 1 + lDirNdirs && all (all a32Valid) dirlist) bad+ where+ bad = throwIO $ FSIllegalPath path+ checkpref p = case stripPrefix prefix p of+ Just (c:r) | isPathSeparator c -> return r+ _ -> bad+-}++-- | 'LDir' that contains a 'Node'+lDirOfNode :: Node -> LDir+lDirOfNode (NodeTCB n) = LDir $ takeDirectory n++-- | 'LDir' that contains the directory that contains a file name.+lDirOfName :: (Label l) => Name l -> LDir+lDirOfName (NameTCB n) = LDir $ takeDirectory $ takeDirectory n+lDirOfName (RootDir l) = lDirOfLabel l++-- |Takes an LDir and returns the label stored in 'labelFile' in that+-- directory. May throw 'FSCorruptLabel'.+labelOfLDir :: (Label l) => LDir -> IO l+labelOfLDir (LDir p) = do+ s <- strictReadFile target `catch` diagnose+ parseit s+ where+ target = (p </> labelFile)+ parseit s = case reads $ LC.unpack s of+ (l, "\n"):_ -> return l+ _ -> throwIO $ FSCorruptLabel target+ diagnose e | isDoesNotExistError e = do+ exists <- doesDirectoryExist p+ if exists+ then throwIO $ FSCorruptLabel target+ else throwIO e+ | otherwise = throwIO e++-- |Gets the LDir for a particular label. Creates it if it does not+-- exist. May throw 'FSCorruptLabel'.+getLDir :: Label l => l -> IO LDir+getLDir l = try (labelOfLDir ldir) >>= handler+ where+ ldir@(LDir dir) = lDirOfLabel l+ handler (Right l')+ | l' == l = return ldir+ | otherwise = dumplabel >> throwIO (FSCorruptLabel dir)+ handler (Left e) =+ case fromException e of+ Just e' | isDoesNotExistError e' -> makedir+ _ -> dumplabel >> throwIO e+ makelabel path = withFile path WriteMode $ \h -> do+ hPutStr h $ shows l "\n"+ hSync h+ -- Mostly unnecessary paranoia here, but one thread could create+ -- the label file, then another thread could overwrite it as the+ -- first thread is renaming the LDir~ -> LDir. If after that+ -- there's a power failure, then the label file could be+ -- corrupted. This way we ensure that once the LABEL file is in+ -- place, it never gets overwritten.+ makesafelabel path = do+ pid <- getProcessID+ tmp <- tmpName+ let tpath = path ++ "." ++ show pid ++ "." ++ tmp ++ newNodeExt+ makelabel tpath+ flip finally (ignoreErr $ removeLink tpath) $+ catch (createLink tpath path) $+ \e -> unless (isAlreadyExistsError e) (throwIO e)+ makedir = do+ let tdir = dir ++ newNodeExt+ createDirectoryIfMissing True tdir+ makesafelabel $ tdir </> labelFile+ rename tdir dir+ return ldir+ dumplabel = ignoreErr $ makelabel $ dir </> (labelFile ++ ".correct")++--+-- Node functions+--++-- |The @Node@ type represents filenames of the form+-- @LabelHash\/OpaqueName@. These names must always point to regular+-- files or directories (not symbolic links). There must always exist+-- a file @LabalHash\/LABEL@ specifying the label of a @Node@.+newtype Node = NodeTCB FilePath deriving (Show)++-- |When a @Node@ is first created, it has a file name with a \'~\'+-- character at the end. This is so that in the case of a crash, a+-- node that was not linked to can be easily recognized and deleted.+-- The @NewNode@ type wrapper represents a node that is not yet linked+-- to.+newtype NewNode = NewNode Node deriving (Show)++-- |String that gets appended to new file names. After a crash these+-- may need to be garbage collected.+newNodeExt :: String+newNodeExt = "~"++-- |Label protecting the contents of a node.+labelOfNode :: (Label l) => Node -> IO l+labelOfNode = labelOfLDir . lDirOfNode++-- | Create new Node in the appropriate directory for a given label.+-- The node gets created with an extra ~ appended, and wrapped in the+-- type 'NewNode' to reflect this fact.+mkNode :: (Label l) => l+ -- ^Label for the new node+ -> (FilePath -> String -> IO (a, FilePath))+ -- ^Either 'mkTmpDir' or 'mkTmpFile' with curried 'IOMode'+ -> IO (a, NewNode)+ -- ^Returns file handle or () and destination path+mkNode l f = do+ (LDir d) <- getLDir l+ (a, p) <- f d newNodeExt+ -- We are done, except if we got really unlucky someone else may+ -- have created a node with the same name at the same time. (The+ -- node creation is exclusive, but we append newNodeExt, so someone+ -- might have renamed it before we created the newNodeExt file+ -- exclusively.) We simply start over if someone claimed the name+ -- in the mean time.+ let p' = take (length p - length newNodeExt) p+ exists <- catchIO (getFileStatus p' >> return True) (return False)+ if not exists+ then return (a, NewNode $ NodeTCB p')+ else do+ hPutStrLn stderr $ "mkNode: file " ++ p' ++ " already exists." -- XXX+ clean p+ mkNode l f++-- |Wrapper around mkNode to create a directory.+mkNodeDir :: (Label l) => l -> IO NewNode+mkNodeDir l = liftM snd (mkNode l mkTmpDir)++-- |Wrapper around mkNode to create a regular file.+mkNodeReg :: (Label l) => IOMode -> l -> IO (Handle, NewNode)+mkNodeReg m l = mkNode l (mkTmpFile m)++-- | Used when creating a symbolic link named @src@ that points to+-- @dst@. If both @src@ and @dst@ are relative to the current working+-- directory and in subdirectories, then the contents of the symbolic+-- link cannot just be @dst@, instead it is @makeRelativeTo dst src@.+makeRelativeTo :: FilePath -- ^ Destination of symbolic link+ -> FilePath -- ^ Name of symbolic link+ -> FilePath -- ^ Returns contents to put in symbolic link+makeRelativeTo dest src =+ doit (splitDirectories dest) (init $ splitDirectories src)+ where+ doit [] [] = "."+ doit (d1:ds) (s1:ss) | d1 == s1 = doit ds ss+ doit d s = joinPath (replicate (length s) ('.':'.':pathSeparator:[]) ++ d)++-- | Assign a 'Name' to a 'NewNode', turning it into a 'Node'. Note+-- that unlike the Unix file system, only a single link may be created+-- to each node.+linkNode :: (Label l) => NewNode -> Name l -> IO Node+linkNode (NewNode (NodeTCB path)) name' = do+ let name = pathOfName name'+ tpath = path ++ newNodeExt+ createSymbolicLink (path `makeRelativeTo` name) name `onException` clean tpath+ -- The next line really shouldn't fail except for some catastrophic+ -- IO error. See the comment in mkNode.+ rename tpath path `onException` removeFile name+ return $ NodeTCB path++-- | It's possible that either a program crashed before renaming a+-- 'NewNode' into a 'Node', or that another thread is calling+-- 'linkNode' and for some reason is being slow betweeen the+-- 'createSymbolicLink' and 'rename' calls. Either way it should be+-- fine for us just to 'rename' the 'NewNode', because the 'Name'+-- would not exist if the 'NewNode' were not ready to be renamed.+fixNode :: Node -> (FilePath -> IO a) -> IO a+fixNode (NodeTCB file) action = action file `catch` fixup+ where+ fixup e | isDoesNotExistError e = do+ ignoreErr $ rename (file ++ newNodeExt) file+ action file+ fixup e = throwIO e++-- | Thie function just calls 'openFile' on the filename in a 'Node'.+-- However, on the off chance that the file system is in an+-- inconsistent state (e.g., because of a crash during a call to+-- 'linkNode'), it tries to finish creating a partially created+-- 'Node'.+openNode :: Node -> IOMode -> IO Handle+openNode node mode = fixNode node $ flip openFile mode++-- | Thie function is a wrapper around 'getDirectoryContents' that+-- tries to fixup errors analogously to 'openNode'.+getDirectoryContentsNode :: Node -> IO [FilePath]+getDirectoryContentsNode node = fixNode node getDirectoryContents++--+-- Name functions+--+ +-- |The @Name@ type represents user-chosen (non-opaque) filenames of+-- symbolic links, either @\"root\"@ or pathnames of the form+-- @LabelHash\/OpaqueName\/filename@. Intermediary components of the+-- file name must not be symbolic links.+data Name l = NameTCB FilePath+ | RootDir l+ deriving (Show)++-- |Label protecting the name of a file. Note that this is the label+-- of the directory containing the file name, not the label of the+-- Node that the file name designates.+labelOfName :: (Label l) => Name l -> IO l+labelOfName (RootDir l) = return l+labelOfName n = labelOfLDir $ lDirOfName n++{-+unlinkName :: (FilePath -> IO ()) -> Name -> IO ()+unlinkName f (NameTCB name) = do+ (Node node) <- nodeOfName (NameTCB name)+ f node+ removeFile name++-- |Remove a directory by name.+unlinkNameDir = unlinkName removeDirectory++-- |Remove a regular file by name.+unlinkNameReg = unlinkName removeFile+-}+ +-- | This function reads the contents of a symbolic link and returns+-- the pathname of its destination, relative to the current working+-- directory. It elides ".." components at the begining of the+-- symbolic link contents, so that if the link @foo\/bar -> ..\/baz@+-- exists, @expandLink \"foo\/bar\"@ will return @\"foo\/baz\"@.+--+-- /Warning:/ This function assumes no itermediary components of the+-- path to the symbolic link are also symbolic links.+expandLink :: FilePath -> IO FilePath+expandLink path = do+ suffix <- catchPred (\e -> ioeGetErrorType e == GHC.InvalidArgument)+ (readSymbolicLink path) (return "")+ return $ if (isAbsolute suffix)+ then suffix+ else domerge (takeDirectory path) suffix+ where+ domerge [] suffix = suffix+ domerge p [] = p+ domerge p ('.':'.':ps:suffix) | ps == pathSeparator =+ domerge (takeDirectory p) suffix+ domerge p suffix = p </> suffix++pathOfName :: (Label l) => Name l -> FilePath+pathOfName (NameTCB n) = n+pathOfName (RootDir l) = case lDirOfLabel l of (LDir ldir) -> ldir </> rootFile++-- | 'Node' that a 'Name' is pointing to.+nodeOfName :: (Label l) => Name l -> IO Node+nodeOfName n = liftM NodeTCB $ expandLink $ pathOfName n++-- | Gives the 'Name' of a directory entry in a directory 'Node'.+nodeEntry :: (Label l) => Node -> FilePath -> Name l+nodeEntry (NodeTCB node) name = NameTCB (node </> name)+++mkRootDirIO :: (Label l) => l -> IO (Name l)+mkRootDirIO label = do+ let name = RootDir label+ exists <- doesDirectoryExist $ pathOfName name+ unless exists $ do+ new <- mkNodeDir label+ linkNode new name >> return ()+ return name++defRoot :: FilePath+defRoot = prefix </> rootFile++initFS :: (Label l) => l -> IO ()+initFS l = do+ name <- mkRootDirIO l+ (NodeTCB node) <- nodeOfName name+ let root = node `makeRelativeTo` defRoot+ root' <- catchIO (readSymbolicLink defRoot) $+ createSymbolicLink root defRoot >> return root+ when (root' /= root) $ error "default root doesn't match requested label"+ ++--+-- LIO Monad function+--++-- | Return the root directory for the default root label. (There is+-- a root directory for each label, but only one label is the+-- default.)+rootDir :: (Label l) => LIO l s (Name l)+rootDir = return $ NameTCB $ defRoot++-- | Get the root directory for a particular label.+getRootDir :: (Label l) => l -> Name l+getRootDir l = RootDir l++-- | Creates a root directory for a particular label.+mkRootDir :: (Priv l p) => p -> l -> LIO l s (Name l)+mkRootDir priv label = do+ wguardP priv label+ name <- rtioTCB $ mkRootDirIO label+ return name++-- | Looks up a FilePath, turning it into a 'Name', and raising to+-- current label to reflect all directories traversed. Note that this+-- only looks up a 'Name'; it does not ensure the 'Name' actually+-- exists. The intent is that you call @lookupName@ before creating+-- or opening files.+--+-- Note that this function will touch bad parts of the file system if+-- it is supplied with a malicous 'Name'. Thus, it is important to+-- keep the constructor of 'Name' private, so that the only way for+-- user code to generate names is to start with 'rootDir' and call+-- @lookupName@.+lookupName :: (Priv l p) =>+ p -- ^ Privileges to limit tainting+ -> Name l -- ^ Start point+ -> FilePath -- ^ Name to look up+ -> LIO l s (Name l)+lookupName priv start path = + dolookup start (stripslash $ splitDirectories path)+ where+ stripslash ((c:_):t) | c == pathSeparator = t+ stripslash t = t+ dolookup name [] = return name+ dolookup name (".":rest) = dolookup name rest+ dolookup _ ("..":_) = throwIO $ mkIOError doesNotExistErrorType+ "illegal filename" Nothing (Just ".." )+ dolookup name@(RootDir label) (cn:rest) = do+ taintP priv label+ node <- rtioTCB $ nodeOfName name+ dolookup (nodeEntry node cn) rest+ dolookup name (cn:rest) = do+ -- XXX next thing should deal with partially created nodes+ node <- rtioTCB $ nodeOfName name -- Could fail if name deleted+ label <- ioTCB $ labelOfNode node -- Shouldn't fail+ taintP priv label+ dolookup (nodeEntry node cn) rest++lookupNode :: (Priv l p) =>+ p -- ^ Privileges to limit tainting+ -> Name l -- ^ Start point (e.g., 'rootDir')+ -> FilePath -- ^ Name to look up+ -> Bool -- ^ True if you want to write it+ -> LIO l s Node+lookupNode priv start path write = do+ name <- lookupName priv start path+ node <- rtioTCB $ nodeOfName name+ label <- ioTCB $ labelOfNode node+ if write then wguardP priv label else taintP priv label+ return node++-- | Creates a temporary directory in an existing directory (or+-- label-specific root directory, if the 'Name' argument comes from+-- 'getRootDir').+mkTmpDirL :: (Priv l p) =>+ p -- ^ Privileges to minimize tainting+ -> l -- ^ Label for the new directory+ -> Name l -- ^ 'Name' of dir in which to create directory+ -> String -- ^ Suffix for name of directory+ -> LIO l s (FilePath, Name l)+ -- ^ Returns both name in directory and 'Name' of new directory+mkTmpDirL priv label name suffix = do+ aguard label+ ensureRoot name+ (NodeTCB node) <- lookupNode priv name "" True+ aguard label+ (NewNode (NodeTCB new)) <- rtioTCB $ mkNodeDir label+ let tnew = new ++ newNodeExt+ target = new `makeRelativeTo` (node </> "x")+ (_, tname) <- rtioTCB $ mkTmp (createSymbolicLink target) node suffix+ `onExceptionTCB` clean tnew+ rtioTCB $ rename tnew new `onExceptionTCB` removeFile tname+ return $ (takeFileName tname, NameTCB tname)+ where+ ensureRoot (RootDir l) = mkRootDir priv l >> return ()+ ensureRoot _ = return ()
+ LIO/Handle.hs view
@@ -0,0 +1,200 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FunctionalDependencies #-}++-- |This module abstracts the basic 'FileHandle' methods provided by+-- the system library, and provides an 'LHandle' (Labeled Handle) type+-- that can be manipulated from within the 'LIO' Monad. Two lower+-- level functions, 'mkDir' and 'mkLHandle' may be useful for+-- functions that wish to open file names that are not relative to+-- 'rootDir'. (There is no notion of changeable current working+-- directory in the 'LIO' Monad.)+--+-- The actual storage of labeled files is handled by the "LIO.FS"+-- module.+module LIO.Handle (DirectoryOps(..)+ , CloseOps (..)+ , HandleOps (..)+ , LHandle+ , hlabelOf+ , mkDir, mkLHandle+ , readFile, writeFile+ , createDirectoryPR, openFilePR, writeFilePR+ , createDirectoryP, openFileP, writeFileP+ , IOMode(..)+ ) where++import LIO.TCB+import LIO.FS++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++class (Monad m) => DirectoryOps h m | m -> h where+ getDirectoryContents :: FilePath -> m [FilePath]+ createDirectory :: FilePath -> m ()+ openFile :: FilePath -> IO.IOMode -> m h++class (Monad m) => CloseOps h m where+ hClose :: h -> m ()+ hFlush :: h -> m ()++class (CloseOps h m) => HandleOps h b m where+ hGet :: h -> Int -> m b+ hGetNonBlocking :: h -> Int -> m b+ hGetContents :: h -> m b+ hPut :: h -> b -> m ()+ hPutStrLn :: h -> b -> m ()++instance DirectoryOps IO.Handle IO where+ getDirectoryContents = IO.getDirectoryContents+ createDirectory = IO.createDirectory+ openFile = IO.openBinaryFile++instance CloseOps IO.Handle IO where+ hClose = IO.hClose+ hFlush = IO.hFlush++instance HandleOps IO.Handle L.ByteString IO where+ hGet = L.hGet+ hGetNonBlocking = L.hGetNonBlocking+ hGetContents = L.hGetContents+ hPut = L.hPut+ hPutStrLn h s = L.hPut h $ L.append s $ L.singleton 0xa++data LHandle l h = LHandleTCB l h++instance (Label l) => MintTCB (LHandle l IO.Handle) (IO.Handle, l) where+ mintTCB (h, l) = LHandleTCB l h++instance (Label l) => DirectoryOps (LHandle l IO.Handle) (LIO l s) where+ getDirectoryContents d = do+ root <- rootDir+ node <- lookupNode NoPrivs root d False+ rtioTCB $ getDirectoryContentsNode node+ createDirectory path = do+ root <- rootDir+ l <- getLabel+ mkDir NoPrivs l root path+ openFile path mode = do+ root <- rootDir+ l <- getLabel+ mkLHandle NoPrivs l root path mode++instance (Label l) => CloseOps (LHandle l IO.Handle) (LIO l s) where+ hClose (LHandleTCB l h) = wguard l >> rtioTCB (hClose h)+ hFlush (LHandleTCB l h) = wguard l >> rtioTCB (hFlush h)++instance (Label l, CloseOps (LHandle l h) (LIO l s), HandleOps h b IO)+ => HandleOps (LHandle l h) b (LIO l s) where+ hGet (LHandleTCB l h) n = wguard l >> rtioTCB (hGet h n)+ hGetNonBlocking (LHandleTCB l h) n =+ wguard l >> rtioTCB (hGetNonBlocking h n)+ hGetContents (LHandleTCB l h) = wguard l >> rtioTCB (hGetContents h)+ hPut (LHandleTCB l h) s = wguard l >> rtioTCB (hPut h s)+ hPutStrLn (LHandleTCB l h) s = wguard l >> rtioTCB (hPutStrLn h s)+++hlabelOf :: (Label l) => LHandle l h -> l+hlabelOf (LHandleTCB l _) = l++++mkDir :: (Priv l p) =>+ p -- ^Privileges+ -> l -- ^Label for the new directory+ -> Name l -- ^Start point+ -> FilePath -- ^Name to create+ -> LIO l s () +mkDir priv l start path = do+ -- No privs when checking clearance, as we assume it was lowered for a reason+ aguard l + name <- lookupName priv start path+ dirlabel <- ioTCB $ labelOfName name+ wguardP priv dirlabel+ new <- ioTCB $ mkNodeDir l+ _ <- rtioTCB $ linkNode new name+ return ()++mkLHandle :: (Priv l p) =>+ p -- ^Privileges to minimize taint+ -> l -- ^Label if new file is created+ -> Name l -- ^Starting point of pathname+ -> FilePath -- ^Path of file relative to prev+ -> IO.IOMode -- ^Mode of handle+ -> LIO l s (LHandle l IO.Handle)+mkLHandle priv l start path mode = do+ aguard l+ name <- lookupName priv start path+ dirlabel <- ioTCB $ labelOfName name+ taintP priv dirlabel+ newl <- getLabel+ mnode <- ioTCB $ tryPred IO.isDoesNotExistError (nodeOfName name)+ case (mnode, mode) of+ (Right node, _) ->+ do nodel <- ioTCB $ labelOfNode node+ let hl = if mode == IO.ReadMode+ then l `lub` newl `lub` nodel+ else nodel+ aguard hl+ h <- rtioTCB $ openNode node mode+ return $ LHandleTCB hl h+ (Left e, IO.ReadMode) -> throwIO e+ _ -> do wguardP priv dirlabel+ aguard l -- lookupName may have changed label+ (h, new) <- rtioTCB $ mkNodeReg mode l+ mn <- rtioTCB $ tryPred IO.isAlreadyExistsError+ (linkNode new name `onException` hClose h)+ case mn of+ Right _ -> return $ LHandleTCB l h+ Left _ -> mkLHandle priv l name "" mode++readFile :: (DirectoryOps h m, HandleOps h b m) => FilePath -> m b+readFile path = openFile path IO.ReadMode >>= hGetContents++writeFile :: (DirectoryOps h m, HandleOps h b m,+ OnExceptionTCB m) => FilePath -> b -> m ()+writeFile path contents = bracketTCB (openFile path IO.WriteMode) hClose+ (flip hPut contents)++createDirectoryPR :: (Priv l p) => p -> Name l -> FilePath -> LIO l s ()+createDirectoryPR privs start path = do+ l <- getLabel+ mkDir privs l start path++writeFilePR :: (Priv l p, HandleOps IO.Handle b IO) =>+ p -> Name l -> FilePath -> b -> LIO l s ()+writeFilePR privs start path contents =+ bracketTCB (openFilePR privs start path IO.WriteMode) hClose+ (flip hPut contents)++openFilePR :: (Priv l p) =>+ p -> Name l -> FilePath -> IOMode -> LIO l s (LHandle l IO.Handle)+openFilePR privs start path mode = do+ l <- getLabel+ mkLHandle privs l start path mode++createDirectoryP :: (Priv l p) => p -> FilePath -> LIO l s ()+createDirectoryP privs path = do+ root <- rootDir+ l <- getLabel+ mkDir privs l root path++writeFileP :: (Priv l p, HandleOps IO.Handle b IO) =>+ p -> FilePath -> b -> LIO l s ()+writeFileP privs path contents =+ bracketTCB (openFileP privs path IO.WriteMode) hClose+ (flip hPut contents)++openFileP :: (Priv l p) =>+ p -> FilePath -> IOMode -> LIO l s (LHandle l IO.Handle)+openFileP privs path mode = do+ root <- rootDir+ l <- getLabel+ mkLHandle privs l root path mode+
+ LIO/HiStar.hs view
@@ -0,0 +1,151 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE DeriveDataTypeable #-}++module LIO.HiStar ( module LIO.HiStar+ , module LIO.Base+ ) where++import LIO.TCB+import LIO.Base++import Data.IORef+import Data.List+import Data.Monoid+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Typeable++--+-- Some generic code+--++withDefaults :: a -> a -> (a -> a -> b) -> Maybe a -> Maybe a+ -> b+withDefaults d1 d2 f a1 a2 = f (unJust d1 a1) (unJust d2 a2)+ where+ unJust :: a -> Maybe a -> a+ unJust _ (Just v) = v+ unJust def Nothing = def++assocs2 :: Ord k => (Map k v1) -> (Map k v2) -> [(k, Maybe v1, Maybe v2)]+assocs2 m1 m2 = merge (Map.assocs m1) (Map.assocs m2)+ where+ merge [] [] = []+ merge ((kx, vx):xs) [] = (kx, Just vx, Nothing) : merge xs []+ merge [] ((ky, vy):ys) = (ky, Nothing, Just vy) : merge [] ys+ merge x@((kx, vx):xs) y@((ky, vy):ys) =+ case compare kx ky of+ EQ -> (kx, Just vx, Just vy) : merge xs ys+ LT -> (kx, Just vx, Nothing) : merge xs y+ GT -> (ky, Nothing, Just vy) : merge x ys++mergeWith :: Ord k =>+ (Maybe a -> Maybe b -> Maybe c) -> Map k a -> Map k b+ -> Map k c+mergeWith f m1 m2 = domerge Map.empty $ assocs2 m1 m2+ where+ domerge m [] = m+ domerge m ((k, v1, v2):as) = domerge (action k (f v1 v2) m) as+ action k Nothing m = m+ action k (Just v) m = Map.insert k v m+++--+-- Now for the HSLabel Label+--++-- XXX Note HSC should be TCB as # of categories allocated leaks info+newtype HSCategory = HSC Integer deriving (Eq, Ord, Read, Show)++{-+instance Enum HSCategory where+ toEnum i = HSC i+ fromEnum (HSC i) = i+-}++data HSLevel = L0 | L1 | L2 | L3 deriving (Eq, Ord, Enum, Read, Show)++instance POrd HSLevel where+ pcompare a b = o2po $ compare a b++-- Second component of HSLabel is the default level for categories not+-- in the map. Invariant: Map must not contain any entries mapping+-- categories to the default level.+data HSLabel = HSL (Map HSCategory HSLevel) HSLevel+ deriving (Read, Show, Typeable)++instance Eq HSLabel where+ a == b = pcompare a b == PEQ++instance POrd HSLabel where+ pcompare (HSL m1 d1) (HSL m2 d2) = foldl each mempty (assocs2 m1 m2)+ where+ each r (k, v1, v2) = r `mappend` comp v1 v2+ comp = withDefaults d1 d2 pcompare+ +combineLabel :: (HSLevel -> HSLevel -> HSLevel)+ -> HSLabel -> HSLabel -> HSLabel+combineLabel fn (HSL m1 d1) (HSL m2 d2) =+ HSL (mergeWith combiner m1 m2) d+ where+ d = fn d1 d2+ no_d v | v == d = Nothing+ | otherwise = Just v+ combiner v1 v2 = no_d $ withDefaults d1 d2 fn v1 v2++instance Label HSLabel where + lbot = HSL Map.empty L1+ ltop = HSL Map.empty L3+ lub = combineLabel max+ glb = combineLabel min+++--+-- Functions for manipulating labels+--++lupdate :: HSLabel -> HSCategory -> HSLevel -> HSLabel+lupdate (HSL m d) cat lev = HSL m' d+ where+ m' = if lev == d then Map.delete cat m else Map.insert cat lev m++lupdates :: HSLabel -> [HSCategory] -> HSLevel -> HSLabel+lupdates lab cats lev = foldl (\lab' cat -> lupdate lab' cat lev) lab cats+ +lapply :: HSLabel -> HSCategory -> HSLevel+lapply (HSL m d) cat = Map.findWithDefault d cat m++lcat L0 c = HSL (Map.singleton c L0) L3+lcat L2 c = HSL (Map.singleton c L2) L0+lcat L3 c = HSL (Map.singleton c L3) L0++newtype HSPrivs = HSPrivs [HSCategory]+data HSState = HSState { nextCat :: IORef HSCategory } deriving Typeable+type HS a = LIO HSLabel HSState a++instance Monoid HSPrivs where+ mempty = HSPrivs []+ mappend (HSPrivs a) (HSPrivs b) = HSPrivs $ union a b++instance PrivTCB HSPrivs+instance Priv HSLabel HSPrivs where+ lostar (HSPrivs p) l min = lupdates l p L0 `lub` min+ leqp (HSPrivs p) a b = lupdates a p L0 `leq` b++noprivs = mempty :: HSPrivs++newcat :: HSLevel -> HS (HSPrivs, HSLabel)+newcat lev = do ls <- getTCB+ cat <- ioTCB $ atomicModifyIORef (nextCat ls) bumpcat+ return (HSPrivs [cat], lcat lev cat)+ where+ bumpcat (HSC c) = (HSC $ c + 1, HSC c)++newHS = do+ ref <- newIORef $ HSC 1000+ return HSState { nextCat = ref }++evalHS :: HS t -> IO (t, HSLabel)+evalHS m = newHS >>= evalLIO m++
+ LIO/LIO.hs view
@@ -0,0 +1,67 @@+{- | 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+ be allowed to import "LIO.TCB"--instead, a module "LIO.Base"+ exports just the safe symbols from "LIO.TCB". This module,+ "LIO.LIO", re-exports "LIO.Base" as well as a few other handy+ modules. For many modules it should be the only import necessary.++ Certain symbols in the LIO library supersede variants in the+ standard Haskell libraries. Thus, depending on the modules+ imported and functions used, you may wish to import LIO with+ commands like these:++ @+ import Prelude hiding ('readFile', 'writeFile', 'catch')+ import Control.Exception hiding ('throwIO', 'catch', 'handle', 'onException'+ , 'bracket', 'block', 'unblock')+ import LIO.LIO+ @++ The LIO variants of the system functions hidden in the above import+ commands are designed to work in both the IO and LIO monads, making+ it easier to have both types of code in the same module.+++ Warning: For security, at a minimum untrusted code must not be+ allowed to do any of the following:++ * Import "LIO.TCB",++ * Use any symbols with names ending @...TCB@,++ * Use the @foreign@ keyword,++ * Use functions such as 'unsafePerformIO', 'unsafeInterleaveIO',+ 'inlinePerformIO',++ * Use language extensions such as Generalized Newtype+ Deriving and Stand-alone Deriving to extend LIO types+ (such as by deriving an instance of @'Show'@ for 'Lref',+ or deriving an instance of the @'MonadTrans'@ class for+ 'LIO', which would allow untrusted code to bypass all+ security with 'lift'),++ * Manually define @typeOf@ methods (as this would cause the+ supposedly safe 'cast' method to make usafe casts); automatically+ deriving @Typeable@ should be safe.++ * 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.+-}+module LIO.LIO (module LIO.Base+ , module LIO.Handle+ , module LIO.LIORef+ , module LIO.MonadLIO+ ) where++-- import Prelude hiding (readFile, writeFile, catch)+import LIO.Base+import LIO.Handle+import LIO.LIORef+import LIO.MonadLIO
+ LIO/LIORef.hs view
@@ -0,0 +1,85 @@+-- |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+-- wguard.+module LIO.LIORef (LIORef+ , newLIORef, labelOfLIORef+ , readLIORef, writeLIORef, atomicModifyLIORef+ -- * With privileges+ , newLIORefP+ , readLIORefP, writeLIORefP, atomicModifyLIORefP+ -- * TCB+ , newLIORefTCB+ , readLIORefTCB, writeLIORefTCB, atomicModifyLIORefTCB+ ) where++import LIO.TCB+import Data.IORef+import Control.Monad (unless)+++data LIORef l a = LIORefTCB l (IORef a)+++newLIORefP :: (Priv l p) => p -> l -> a -> LIO l s (LIORef l a)+newLIORefP p l a = do+ aguardP p l+ ior <- ioTCB $ newIORef a+ return $ LIORefTCB l ior++newLIORef :: (Label l) => l -> a -> LIO l s (LIORef l a)+newLIORef = newLIORefP NoPrivs++newLIORefTCB :: (Label l) => l -> a -> LIO l s (LIORef l a)+newLIORefTCB l a = do+ ior <- ioTCB $ newIORef a+ return $ LIORefTCB l ior++--++labelOfLIORef :: (Label l) => LIORef l a -> l+labelOfLIORef (LIORefTCB l _) = l++--++readLIORefP :: (Priv l p) => p -> LIORef l a -> LIO l s a+readLIORefP p (LIORefTCB l r) = do+ taintP p l+ val <- ioTCB $ readIORef r+ return val++readLIORef :: (Label l) => LIORef l a -> LIO l s a+readLIORef = readLIORefP NoPrivs++readLIORefTCB :: (Label l) => LIORef l a -> LIO l s a+readLIORefTCB (LIORefTCB l r) = ioTCB $ readIORef r++--++writeLIORefP :: (Priv l p) => p -> LIORef l a -> a -> LIO l s ()+writeLIORefP p (LIORefTCB l r) a = do+ aguardP p l+ ioTCB $ writeIORef r a++writeLIORef :: (Label l) => LIORef l a -> a -> LIO l s ()+writeLIORef = writeLIORefP NoPrivs ++writeLIORefTCB :: (Label l) => LIORef l a -> a -> LIO l s ()+writeLIORefTCB (LIORefTCB l r) a = ioTCB $ writeIORef r a++--++atomicModifyLIORefP :: (Priv l p) =>+ p -> LIORef l a -> (a -> (a, b)) -> LIO l s b+atomicModifyLIORefP p (LIORefTCB l r) f = do+ aguardP p l+ ioTCB $ atomicModifyIORef r f++atomicModifyLIORef :: (Label l) =>+ LIORef l a -> (a -> (a, b)) -> LIO l s b+atomicModifyLIORef = atomicModifyLIORefP NoPrivs++atomicModifyLIORefTCB :: (Label l) =>+ LIORef l a -> (a -> (a, b)) -> LIO l s b+atomicModifyLIORefTCB (LIORefTCB l r) f = ioTCB $ atomicModifyIORef r f+
+ LIO/MonadCatch.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}++-- | This module generalizes 'throw' and 'catch' (from+-- "Control.Exception") to methods that can be defined on multiple+-- Monads.+module LIO.MonadCatch (MonadCatch(..), genericBracket) where++import Prelude hiding (catch)+import Control.Exception (Exception, SomeException)+import qualified Control.Exception as E++-- | @MonadCatch@ is the class used to generalize the standard IO+-- @catch@ and @throwIO@ functions to methods that can be defined in+-- multiple monads.+class (Monad m) => MonadCatch m where+ block :: m a -> m a+ unblock :: m a -> m a+ throwIO :: (Exception e) => e -> m a+ catch :: (Exception e) => m a -> (e -> m a) -> m a+ handle :: (Exception e) => (e -> m a) -> m a -> m a+ handle = flip catch+ onException :: m a -> m b -> m a+ onException io h = io `catch` \e -> h >> throwIO (e :: SomeException)+ bracket :: m b -> (b -> m c) -> (b -> m a) -> m a+ bracket = genericBracket onException++instance MonadCatch IO where+ block = E.block+ unblock = E.unblock+ throwIO = E.throwIO+ catch = E.catch+ onException = E.onException+ bracket = E.bracket++genericBracket :: (MonadCatch m) =>+ (m b -> m c -> m b) -- ^ On exception function+ -> m a -- ^ Action to perform before+ -> (a -> m c) -- ^ Action for afterwards+ -> (a -> m b) -- ^ Main (in between) action+ -> m b -- ^ Result of main action+genericBracket myOnException before after between =+ block $ do+ a <- before+ b <- unblock (between a) `myOnException` after a+ after a >> return b
+ LIO/MonadLIO.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE OverlappingInstances #-}++-- | This module provides a function 'liftLIO' for executing 'LIO'+-- computations from transformed versions of the 'LIO' monad. There+-- is also a method @liftIO@, which is a synonym for 'liftLIO', to+-- help with porting code that expects to run in the 'IO' monad.+module LIO.MonadLIO where++import LIO.TCB++import Control.Monad.Trans (MonadTrans(..))++class (Monad m, Label l) => MonadLIO m l s | m -> l s where+ liftLIO :: LIO l s a -> m a+ liftIO :: LIO l s a -> m a -- Might want to hide this one+ liftIO = liftLIO++instance (Label l) => MonadLIO (LIO l s) l s where+ liftLIO = id++instance (MonadLIO m l s, MonadTrans t, Monad (t m)) => MonadLIO (t m) l s where+ liftLIO = lift . liftLIO
+ LIO/TCB.hs view
@@ -0,0 +1,894 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- | This module implements the core of the Labeled IO library for+-- information flow control in Haskell. It provides a monad, 'LIO',+-- that is intended to be used as a replacement for the IO monad in+-- untrusted code. The idea is for untrusted code to provide a+-- computation in the 'LIO' monad, which trusted code can then safely+-- execute through the 'evalLIO' function. (Though usually a wrapper+-- function is employed depending on the type of labels used by an+-- application. For example, with "LIO.DCLabel", you would use+-- 'evalDC' to execute an untrusted computation, and with "LIO.HiStar"+-- labels, the function is 'evalHS'. There are also abbreviations for+-- the 'LIO' monad type of a particular label--for instance 'DC' or+-- 'HS'.)+--+-- A data structure 'Labeled' (labeled value) protects access to pure+-- values. Without the appropriate privileges, one cannot produce a+-- pure value that depends on a secret 'Labeled', or conversely produce a+-- high-integrity 'Labeled' based on pure data. The function 'toLabeled'+-- allows one to seal off the results of an LIO computation inside an+-- 'Labeled' without tainting the current flow of execution. 'unlabel'+-- conversely allows one to use the value stored within a 'Labeled'.+-- +-- Any code that imports this module is part of the+-- /Trusted Computing Base/ (TCB) of the system. Hence, untrusted+-- code must be prevented from importing this module. The exported+-- symbols ending ...@TCB@ can be used to violate label protections+-- even from within pure code or the LIO Monad. A safe subset of+-- these symbols is exported by the "LIO.Base" module, which is how+-- untrusted code should access the core label functionality.+-- ("LIO.Base" is also re-exported by "LIO.LIO", the main gateway to+-- this library.)+--+module LIO.TCB (+ -- * Basic label functions+ -- $labels+ POrdering(..), POrd(..), o2po, Label(..)+ , Priv(..), NoPrivs(..)+ -- * Labeled IO Monad (LIO)+ -- $LIO+ , LIO+ , getLabel, setLabelP+ , getClearance, lowerClr, lowerClrP, withClearance+ -- ** LIO guards+ -- $guards+ , taint, taintP+ , wguard, wguardP, aguard, aguardP+ -- * Labeled values+ , Labeled+ --+ , label, labelP+ , unlabel, unlabelP+ , toLabeled, toLabeledP, discard+ , labelOf+ , taintLabeled+ -- * Exceptions+ -- ** Exception type thrown by LIO library+ , LabelFault(..)+ -- ** Throwing and catching labeled exceptions+ -- $lexception+ , MonadCatch(..), catchP, handleP, onExceptionP, bracketP+ -- * Executing computations+ , evaluate+ , evalLIO+ -- Start TCB exports+ -- * Privileged operations+ , LIOstate(..)+ , runLIO+ , ShowTCB(..)+ , ReadTCB(..)+ , labelTCB+ , PrivTCB, MintTCB(..)+ , unlabelTCB+ , setLabelTCB, lowerClrTCB+ , getTCB, putTCB+ , ioTCB, rtioTCB+ , rethrowTCB, OnExceptionTCB(..)+ -- ** Misc symbols useful for privileged code+ , newstate, LIOstate, runLIO+ -- End TCB exports+ ) where+import Debug.Trace+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,+ onException, block, unblock, evaluate)+import qualified Control.Exception as E+import Data.Monoid+import Data.Typeable+import Text.Read (minPrec)++import LIO.MonadCatch++--+-- We need a partial order and a Label+--++{- $labels++Labels are a way of describing who can observe and modify data. There+is a partial order, generally pronounced \"can flow to\" on labels.+In Haskell we write this partial order ``leq`` (in the literature it+is usually written as a square less than or equal sign--@\\sqsubseteq@+in TeX).++The idea is that data labeled @l1@ should affect data labeled @l2@ only if+@l1@ ``leq`` @l2@, (i.e., @l1@ /can flow to/ @l2@). The 'LIO' monad keeps+track of the current label of the executing code (accessible via the+'getLabel' function). Code may attempt to perform various IO or+memory operations on labeled data. Touching data may change the+current label or throw an exception if an operation would violate+can-flow-to restrictions.++If the current label is @lcurrent@, then it is only permissible to+read data labeled @lr@ if @lr ``leq`` lcurrent@. This is sometimes+termed \"no read up\" in the literature; however, because the partial+order allows for incomparable labels (i.e., two labels @l1@ and @l2@+such that @not (l1 ``leq`` l2) && not (l2 ``leq`` l1)@), a more+appropriate phrasing would be \"read only what can flow to your+label\". Note that, rather than throw an exception, reading data will+often just increase the current label to ensure that @lr ``leq``+lcurrent@. The LIO monad keeps a second label, called the /clearance/+(see 'getClearance'), that represents the highest value the+current thread can raise its label to.++Conversely, it is only permissible to modify data labeled @lw@ when+@lcurrent ``leq`` lw@, a property often cited as \"no write down\",+but more accurately characterized as \"write only what you can flow+to\". In practice, there are very few IO abstractions in which it is+possible to do a pure write that doesn't also involve observing some+state. For instance, writing to a file handle and not getting an+exception tells you that the handle is not closed. Thus, in practice,+the requirement for modifying data labeled @lw@ is almost always that+@lcurrent == lw@.++Note that higher labels are neither more nor less privileged than+lower ones. Simply, the higher one's label is, the more things one+can read. Conversely, the lower one's label, the more things one can+write. But, because labels are a partial and not a total order, +some data may be completely inaccessible to a particular omputatoin; for+instance, if the current label is @lcurrent@, the current clearance is+@ccurrent@, and some data is labeled @ld@, such that @not (lcurrent+``leq`` ld || ld ``leq`` ccurrent)@, then the current thread can+neither read nor write the data, at least without invoking some+privilege.++Privilege comes from a separate class called 'Priv', representing the+ability to bypass the protection of certain labels. Essentially,+privilege allows you to behave as if @l1 ``leq`` l2@ even when that is+not the case. The process of making data labeled @l1@ affect data+labeled @l2@ when @not (l1 ``leq`` l2)@ is called /downgrading/.++The basic method of the 'Priv' object is 'leqp', which performs the+more permissive can-flow-to check in the presence of particular+privileges. Many 'LIO' operations have variants ending @...P@ that+take a privilege argument to act in a more permissive way. All 'Priv'+types are monoids, and so can be combined with 'mappend'.++How to create 'Priv' objects is specific to the particular label type+in use. The method used is 'mintTCB', but the arguments depend on the+particular label type. (Obviously, the symbol 'mintTCB' must not be+available to untrusted code.)++-}++data POrdering = PEQ -- ^Equal+ | PLT -- ^Less than+ | PGT -- ^Greater than+ | PNE+ -- ^Incomparable (neither less than nor greater than)+ deriving (Eq, Ord, Show)++instance Monoid POrdering where+ mempty = PEQ+ mappend PLT PGT = PNE+ mappend PGT PLT = PNE+ mappend x y = max x y++class (Eq a) => POrd a where+ pcompare :: a -> a -> POrdering+ leq :: a -> a -> Bool++ pcompare a b | a == b = PEQ+ | a `leq` b = PLT+ | b `leq` a = PGT+ | otherwise = PNE+ leq a b = case pcompare a b of+ PEQ -> True+ PLT -> True+ _ -> False++o2po :: Ordering -> POrdering+o2po EQ = PEQ; o2po LT = PLT; o2po GT = PGT++class (POrd a, Show a, Read a, Typeable a) => Label a where+ -- | bottom+ lbot :: a+ -- | top+ ltop :: a+ -- | least upper bound (join) of two labels+ lub :: a -> a -> a+ -- | greatest lower bound (meet) of two labels+ glb :: a -> a -> a+++--+-- Labeled value - Labeled+-- Downgrading privileges - Priv+--++-- | @Labeled@ is a type representing labeled data. +data (Label l) => Labeled l t = LabeledTCB l t++-- | 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+-- examine such objects from within the debugger. The 'showTCB'+-- method can be used to examine such objects.+class ShowTCB a where+ showTCB :: a -> String++instance (Label l, Show a) => ShowTCB (Labeled l a) where+ showTCB (LabeledTCB l t) = shows t $ " {" ++ shows l "}"++class MintTCB t i where+ -- |A function that mints new objects (such as instances of+ -- 'Priv') in a way that only privileged code should be allowed to+ -- do. Because the MintTCB method is only available to+ -- priviledged code, other modules imported by unpriviledged code+ -- can define instances of mintTCB.+ mintTCB :: i -> t++-- | It is useful to have the dual of 'ShowTCB', @ReadTCB@, that allows+-- for the reading of 'Labeled's that were written using 'showTCB'. Only+-- @readTCB@ (corresponding to 'read') and @readsPrecTCB@ (corresponding+-- to 'readsPrec') are implemented.+class ReadTCB a where+ readsPrecTCB :: Int -> ReadS a+ readTCB :: String -> a+ readTCB str = check $ readsPrecTCB minPrec str+ where check [] = error "readTCB: no parse"+ check [(x,rst)] | all (==' ') rst = x+ | otherwise = error "readTCB: no parse"+ check _ = error "readTCB: ambiguous parse"++instance (Label l, Read l, Read a) => ReadTCB (Labeled l a) where+ readsPrecTCB _ str = do (val, str1) <- reads str+ ("{", str2) <- lex str1+ (lab, str3) <- reads str2+ ("}", rest) <- lex str3+ return (labelTCB lab val, rest)++-- | @PrivTCB@ is a method-less class whose only purpose is to be+-- unavailable to unprivileged code. Since @(PrivTCB t) =>@ is in the+-- context of class 'Priv' and unprivileged code cannot create new+-- instances of the @PrivTCB@ class, this ensures unprivileged code+-- cannot create new instances of the 'Priv' class either, even though+-- the symbol 'Priv' is exported by "LIO.Base" and visible to+-- untrusted code.+class PrivTCB t where+class (Label l, Monoid p, PrivTCB p) => Priv l p where+ -- |@leqp p l1 l2@ means that privileges @p@ are sufficient to+ -- downgrade data from @l1@ to @l2@. Note that @'leq' l1 l2@+ -- implies @'leq' p l1 l2@ for all @p@, but for some labels and+ -- privileges, @leqp@ will hold even where @'leq'@ does not.+ leqp :: p -> l -> l -> Bool+ leqp p a b = lostar p a b `leq` b++ -- | Roughly speaking, the function+ -- + -- > result = lostar p label goal+ -- + -- computes how close one can come to downgrading data labeled+ -- @label@ to @goal@ given privileges @p@. When @p == 'NoPrivs'@,+ -- @result == 'lub' label goal@. If @p@ contains all possible+ -- privileges, then @result == goal@.+ --+ -- More specifically, @result@ is the greatest lower bound of the+ -- set of all labels @r@ satisfying:+ --+ -- 1. @'leq' goal r@, and+ --+ -- 2. @'leqp' p label r@+ --+ -- Operationally, @lostar@ captures the minimum change required to+ -- the current label when viewing data labeled @label@. A common+ -- pattern is to use the result of 'getLabel' as @goal@ (i.e.,+ -- the goal is to use privileges @p@ to avoid changing the label+ -- at all), and then compute @result@ based on the @label@ of data+ -- the code is about to observe. For example, 'taintP' could be+ -- implemented as:+ --+ -- @+ -- taintP p l = do lcurrent <- 'getLabel'+ -- 'taint' (lostar p l lcurrent)+ -- @+ lostar :: p -- ^ Privileges+ -> l -- ^ Label from which data must flow+ -> l -- ^ Goal label+ -> l -- ^ Result++-- |A generic 'Priv' instance that works for all 'Label's and confers+-- no downgrading privileges.+data NoPrivs = NoPrivs+instance PrivTCB NoPrivs+instance Monoid NoPrivs where+ mempty = NoPrivs+ mappend _ _ = NoPrivs+instance (Label l) => Priv l NoPrivs where+ leqp _ a b = leq a b+ lostar _ l goal = lub l goal++-- Trusted constructor that creates labeled values.+labelTCB :: Label l => l -> a -> Labeled l a+labelTCB l a = LabeledTCB l a++-- | Raises the label of a 'Labeled' to the 'lub' of it's current label+-- and the value supplied. The label supplied must be less than the+-- current clarance, though the resulting label may not be if the+-- 'Labeled' is already above the current thread's clearance.+taintLabeled :: (Label l) => l -> Labeled l a -> LIO l s (Labeled l a)+taintLabeled l (LabeledTCB la a) = do+ aguard l+ return $ LabeledTCB (lub l la) a++-- | Extracts the value from an 'Labeled', discarding the label and any+-- protection.+unlabelTCB :: Label l => Labeled l a -> a+unlabelTCB (LabeledTCB _ a) = a++-- | Returns label of a 'Label' type.+labelOf :: Label l => Labeled l a -> l+labelOf (LabeledTCB l _) = l+++--+-- Labeled IO+--++-- $LIO+-- +-- The 'LIO' monad is a wrapper around 'IO' that keeps track of the+-- current label and clearance. It is possible to raise one's label+-- or lower one's clearance without privilege, but moving in the other+-- direction requires appropriate privilege.+--+-- 'LIO' is parameterized by two types. The first is the particular+-- label type. The second type is state specific to the label type.+-- Trusted label implementation code can use 'getTCB' and 'putTCB' to+-- get and set the label state.++data (Label l) => LIOstate l s =+ LIOstate { labelState :: s+ , lioL :: l -- current label+ , lioC :: l -- current clearance+ }++newtype (Label l) => LIO l s a = LIO (StateT (LIOstate l s) IO a)+ deriving (Functor, Monad, MonadFix)++get :: (Label l) => LIO l s (LIOstate l s)+get = mkLIO $ \s -> return (s, s)++put :: (Label l) => LIOstate l s -> LIO l s ()+put s = mkLIO $ \_ -> return (() , s)++-- | Function to construct an 'Labeled' from a label and pure value. If+-- the current label is @lcurrent@ and the current clearance is+-- @ccurrent@, then the label @l@ specified must satisfy+-- @lcurrent ``leq`` l && l ``leq`` ccurrent@.+label :: (Label l) => l -> a -> LIO l s (Labeled l a)+label l a = get >>= doit+ where doit s | not $ l `leq` lioC s = throwIO LerrClearance+ | not $ lioL s `leq` l = throwIO LerrLow+ | otherwise = return $ LabeledTCB l a++-- | Constructs an 'Labeled' using privilege to allow the `Labeled`'s label+-- to be below the current label. If the current label is @lcurrent@+-- and the current clearance is @ccurrent@, then the privilege @p@ and+-- label @l@ specified must satisfy+-- @(leqp p lcurrent l) && l ``leq`` ccurrent@.+-- Note that privilege is not used to bypass the clearance. You must+-- use 'lowerClrP' to raise the clearance first if you wish to+-- create an 'Labeled' at a higher label than the current clearance.+labelP :: (Priv l p) => p -> l -> a -> LIO l s (Labeled l a)+labelP p l a = get >>= doit+ where doit s | not $ l `leq` lioC s = throwIO LerrClearance+ | not $ leqp p (lioL s) l = throwIO LerrLow+ | otherwise = return $ LabeledTCB l a++-- | Returns the current value of the thread's label.+getLabel :: (Label l) => LIO l s l+getLabel = get >>= return . lioL++-- | Returns the current value of the thread's clearance.+getClearance :: (Label l) => LIO l s l+getClearance = get >>= return . lioC++{- $guards++ Guards are used by privileged code to check that the invoking,+ unprivileged code has access to particular data. If the current+ label is @lcurrent@ and the current clearance is @ccurrent@, then+ the following checks should be performed when accessing data+ labeled @ldata@:++ * When /reading/ an object labeled @ldata@, it must be the case+ that @ldata ``leq`` lcurrent@. This check is performed by the+ 'taint' function, so named becuase it \"taints\" the current LIO+ context by raising @lcurrent@ until @ldata ``leq`` lcurrent@.+ (Specifically, it does this by computing the least upper bound of+ the two labels with the 'lub' method of the 'Label' class.)+ However, if after doing this it would be the case that+ @not (lcurrent ``leq`` ccurrent)@, then 'taint' throws exception+ 'LerrClearance' rather than raising the current label.++ * When /writing/ an object, it should be the case that @ldata+ ``leq`` lcurrent && lcurrent ``leq`` ldata@. (As stated, this is+ the same as saying @ldata == lcurrent@, but the two are different+ when using 'leqp' instead of 'leq'.) This is ensured by the+ 'wguard' (write guard) function, which does the equivalent of+ 'taint' to ensure the target label @ldata@ can flow to the+ current label, then throws an exception if @lcurrent@ cannot flow+ back to the target label.++ * When /creating/ or /allocating/ objects, it is permissible for+ them to be higher than the current label, so long as they are+ bellow the current clearance. In other words, it must be the+ case that @lcurrent ``leq`` ldata && ldata ``leq`` ccurrent@.+ This is ensured by the 'aguard' (allocation guard) function.++The 'taintP', 'wguardP', and 'aguardP' functions are variants of the+above that take privilege to be more permissive and raise the current+label less. ++-}++-- | General (internal) taint function. Uses @mylub@ instead of+-- 'lub', so that privileges can optionally be passed in. Throws+-- 'LerrClearance' if raising the current label would exceed the+-- current clearance.+gtaint :: (Label l) =>+ (l -> l -> l) -- ^ @mylub@ function+ -> l -- ^ @l@ - Label to taint with+ -> LIO l s ()+gtaint mylub l = do+ s <- get+ let lnew = l `mylub` (lioL s)+ if lnew `leq` lioC s+ then put s { lioL = lnew }+ else ioTCB $ E.throwIO $ LabeledExceptionTCB (lioL s)+ (toException LerrClearance)++-- |Use @taint l@ in trusted code before observing an object labeled+-- @l@. This will raise the current label to a value @l'@ such that+-- @l ``leq`` l'@, or throw @'LerrClearance'@ if @l'@ would have to be+-- higher than the current clearance.+taint :: (Label l) => l -> LIO l s ()+taint = gtaint lub++-- |Like 'taint', but use privileges to reduce the amount of taint+-- required. Note that unlike 'setLabelP', @taintP@ will never lower+-- the current label. It simply uses privileges to avoid raising the+-- label as high as 'taint' would raise it.+taintP :: (Priv l p) =>+ p -- ^Privileges to invoke+ -> l -- ^Label to taint to if no privileges+ -> LIO l s ()+taintP p = gtaint (lostar p)++-- |Use @wguard l@ in trusted code before modifying an object labeled+-- @l@. If @l'@ is the current label, then this function ensures that+-- @l' ``leq`` l@ before doing the same thing as @'taint' l@. Throws+-- @'LerrHigh'@ if the current label @l'@ is too high.+wguard :: (Label l) => l -> LIO l s ()+wguard l = do l' <- getLabel+ if l' `leq` l+ then taint l+ else throwIO LerrHigh++-- |Like 'wguard', but takes privilege argument to be more permissive.+wguardP :: (Priv l p) => p -> l -> LIO l s ()+wguardP p l = do l' <- getLabel+ if leqp p l' l+ then taintP p l+ else throwIO LerrHigh++-- |Ensures the label argument is between the current IO label and+-- current IO clearance. Use this function in code that allocates+-- objects--untrusted code shouldn't be able to create an object+-- labeled @l@ unless @aguard l@ does not throw an exception.+aguard :: (Label l) => l -> LIO l s ()+aguard newl = do c <- getClearance+ l <- getLabel+ unless (leq newl c) $ throwIO LerrClearance+ unless (leq l newl) $ throwIO LerrLow+ return ()++-- | Like 'aguardP', but takes privilege argument to be more permissive.+aguardP :: (Priv l p) => p -> l -> LIO l s ()+aguardP p newl = do c <- getClearance+ l <- getLabel+ unless (leqp p newl c) $ throwIO LerrClearance+ unless (leqp p l newl) $ throwIO LerrLow+ return ()+++-- | If the current label is @oldLabel@ and the current clearance is+-- @clearance@, this function allows code to raise the label to any+-- value @newLabel@ such that+-- @oldLabel ``leq`` newLabel && newLabel ``leq`` clearance@.+-- Note that there is no @setLabel@ variant without the @...P@ because+-- the 'taint' function provides essentially the same functionality+-- that @setLabel@ would.+setLabelP :: (Priv l p) => p -> l -> LIO l s ()+setLabelP p l = do s <- get+ if leqp p (lioL s) l+ then put s { lioL = l }+ else throwIO LerrPriv++-- | Set the current label to anything, with no security check.+setLabelTCB :: (Label l) => l -> LIO l s ()+setLabelTCB l = do s <- get+ if l `leq` lioC s+ then put s { lioL = l }+ else throwIO LerrClearance++-- |Reduce the current clearance. One cannot raise the current label+-- or create object with labels higher than the current clearance.+lowerClr :: (Label l) => l -> LIO l s ()+lowerClr l = get >>= doit+ where doit s | not $ l `leq` lioC s = throwIO LerrClearance+ | not $ lioL s `leq` l = throwIO LerrLow+ | otherwise = put s { lioC = l }++-- |Raise the current clearance (undoing the effects of 'lowerClr').+-- This requires privileges.+lowerClrP :: (Priv l p) => p -> l -> LIO l s ()+lowerClrP p l = get >>= doit+ where doit s | not $ leqp p l $ lioC s = throwIO LerrPriv+ | not $ lioL s `leq` l = throwIO LerrLow+ | otherwise = put s { lioC = l }++-- | Set the current clearance to anything, with no security check.+lowerClrTCB :: (Label l) => l -> LIO l s ()+lowerClrTCB l = get >>= doit+ where doit s | not $ lioL s `leq` l = throwIO LerrInval+ | otherwise = put s { lioC = l }++-- | Lowers the clearance of a computation, then restores the+-- clearance to its previous value. Useful to wrap around a+-- computation if you want to be sure you can catch exceptions thrown+-- by it. Also useful to wrap around 'toLabeled' to ensure that the+-- computation does not access data exceeding a particular label. If+-- @withClearance@ is given a label that can't flow to the current+-- clearance, then the clearance is lowered to the greatest lower+-- bound of the label supplied and the current clearance.+--+-- Note that if the computation inside @withClearance@ acquires any+-- 'Priv's, it may still be able to raise its clearance above the+-- supplied argument using 'lowerClrP'.+withClearance :: (Label l) => l -> LIO l s a -> LIO l s a+withClearance l m = do+ s <- get+ put s { lioC = l `glb` lioC s }+ a <- m+ put s { lioC = lioC s }+ return a++-- | Within the 'LIO' monad, this function takes an 'Labeled' and returns+-- the value. Thus, in the 'LIO' monad one can say:+--+-- > x <- unlabel (xv :: Labeled SomeLabelType Int)+--+-- And now it is possible to use the value of @x@, which is the pure+-- value of what was stored in @xv@. Of course, @unlabel@ also raises+-- the current label. If raising the label would exceed the current+-- clearance, then @unlabel@ throws 'LerrClearance'.+-- However, you can use 'labelOf' to check if 'unlabel' will suceed without+-- throwing an exception.+unlabel :: (Label l) => Labeled l a -> LIO l s a+unlabel (LabeledTCB la a) = do+ taint la+ return a++-- | Extracts the value of an 'Labeled' just like 'unlabel', but takes a+-- privilege argument to minimize the amount the current label must be+-- raised. Will still throw 'LerrClearance' under the same+-- circumstances as 'unlabel'.+unlabelP :: (Priv l p) => p -> Labeled l a -> LIO l s a+unlabelP p (LabeledTCB la a) = do+ taintP p la+ return a++-- |@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.+-- Thus, 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 suggestst 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 occured in the computation+-- producing the value of the 'Labeled'. +-- This higlights one main use of clearance: to ensure that a @Labeled@+-- computed does not exceed a particular label.+toLabeled :: (Label l) => l -> LIO l s a -> LIO l s (Labeled l a)+toLabeled = toLabeledP NoPrivs++toLabeledP :: (Priv l p) => p -> l -> LIO l s a -> LIO l s (Labeled l a)+toLabeledP p l m = do+ aguard l+ save_s <- get+ a <- m+ s <- get+ put s { lioL = lioL save_s, lioC = lioC save_s}+ unless (leqp p (lioL s) l) $ throwIO LerrLow -- l is too low+ return $ LabeledTCB l a++-- | 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 ltop $ 'hputStrLn' log_handle \"Log message\"+-- @+--+-- to create a log message without affecting the current label. (Of+-- course, if @log_handle@ is closed and this throws an exception, it+-- may not be possible to catch the exception within the 'LIO' monad+-- without sufficient privileges--see 'catchP'.)+discard :: (Label l) => l -> LIO l s a -> LIO l s ()+discard l m = toLabeled l m >> return ()++-- | Returns label-specific state of the 'LIO' monad. This is the+-- data specified as the second argument of 'evalLIO', whose type is+-- @s@ in the monad @LIO l s@.+getTCB :: (Label l) => LIO l s s+getTCB = get >>= return . labelState++-- | Sets the label-specific state of the 'LIO' monad. See 'getTCB'.+putTCB :: (Label l) => s -> LIO l s ()+putTCB ls = get >>= put . update+ where update s = s { labelState = ls }++-- | Generate a fresh state to pass 'runLIO' when invoking it for the+-- first time.+newstate :: (Label l) => s -> LIOstate l s+newstate s = LIOstate { labelState = s , lioL = lbot , lioC = ltop }++mkLIO :: (Label l) => (LIOstate l s -> IO (a, LIOstate l s)) -> LIO l s a+mkLIO = LIO . StateT++unLIO :: (Label l) => LIO l s a -> LIOstate l s+ -> IO (a, LIOstate l s)+unLIO (LIO (StateT f)) = f++-- | Execute an LIO action.+runLIO :: forall l s a. (Label l) => LIO l s a -> LIOstate l s+ -> IO (a, LIOstate l s)+runLIO m s = unLIO m s `E.catch` (E.throwIO . delabel)+ where delabel :: LabeledExceptionTCB l -> SomeException+ delabel (LabeledExceptionTCB _ e) = e+ -- trace ("unlabeling " ++ show e ++ " {" ++ show l ++ "}") e++-- | Produces an 'IO' computation that will execute a particular 'LIO'+-- computation. Because untrusted code cannot execute 'IO'+-- computations, this function should only be useful within trusted+-- code. No harm is done from exposing the @evalLIO@ symbol to+-- untrusted code. (In general, untrusted code is free to produce+-- 'IO' computations--it just can't execute them without access to+-- 'ioTCB'.)+evalLIO :: (Label l) =>+ LIO l s a -- ^ The LIO computation to execute+ -> s -- ^ Initial value of label-specific state+ -> IO (a, l) -- ^ IO computation that will execute first argument+evalLIO m s = do (a, ls) <- runLIO m (newstate s)+ return (a, lioL ls)++-- | Lifts an 'IO' computation into the 'LIO' monad. Note that+-- exceptions thrown within the 'IO' computation cannot directly be+-- caught within the 'LIO' computation. Thus, if you are not inside a+-- 'rethrowTCB' block, you will generally want to use 'rtioTCB'+-- instead of 'ioTCB'.+ioTCB :: (Label l) => IO a -> LIO l s a+ioTCB a = mkLIO $ \s -> do r <- a; return (r, s)++-- | Lifts an 'IO' computation into the 'LIO' monad. If the 'IO'+-- computation throws an exception, it labels the exception with the+-- current label so that the exception can be caught with 'catch' or+-- 'catchP'. This function's name stands for \"re-throw io\", because+-- the functionality is a combination of 'rethrowTCB' and 'ioTCB'.+-- Effectively+--+-- @+-- rtioTCB = 'rethrowTCB' . 'ioTCB'+-- @+rtioTCB :: (Label l) => IO a -> LIO l s a+rtioTCB a = rethrowTCB $ mkLIO $ \s -> do r <- a; return (r, s)++--+-- Exceptions+--++data LabelFault+ = LerrLow -- ^ Requested label too low+ | LerrHigh -- ^ Current label too high+ | LerrClearance -- ^ Label would exceed clearance+ | LerrPriv -- ^ Insufficient privileges+ | LerrInval -- ^ Invalid request+ deriving (Show, Typeable)++instance Exception LabelFault++-- | Map a function over the underlying IO computation within an LIO.+-- Obviously this symbol should not be exported, as it is privileged.+iomaps :: (Label l) =>+ (LIOstate l s -> IO (a, LIOstate l s) -> IO (a, LIOstate l s))+ -> LIO l s a -> LIO l s a+iomaps f c = mkLIO $ \s -> (f s $ unLIO c s)++-- | Like 'iomaps' if you don't need the state.+iomap :: (Label l) =>+ (IO (a, LIOstate l s) -> IO (a, LIOstate l s))+ -> LIO l s a -> LIO l s a+iomap f = iomaps $ \_ -> f++-- |Privileged code that does IO operations may cause exceptions that+-- should be caught by untrusted code in the 'LIO' monad. Such+-- operations should be wrapped by @rethrowTCB@ (or 'rtioTCB', which+-- uses @rethrowTCB@) to ensure the exception is labeled. Note that+-- it is very important that the computation executed inside+-- @rethrowTCB@ not in any way change the label, as otherwise+-- @rethrowTCB@ would put the wrong label on the exception.+rethrowTCB :: (Label l) => LIO l s a -> LIO l s a+rethrowTCB = iomaps $ \s -> handle (E.throwIO . (LabeledExceptionTCB $ lioL s))+ -- mapException (LabeledExceptionTCB $ lioL s) c++data LabeledExceptionTCB l =+ LabeledExceptionTCB l SomeException deriving Typeable++{- $lexception++ We must re-define the 'throwIO' and 'catch' functions to work in+ the 'LIO' monad. A complication is that exceptions could+ potentially leak information. For instance, within a block of code+ wrapped by 'discard', one might examine a secret bit, and throw an+ exception when the bit is 1 but not 0. Allowing untrusted code to+ catch the exception leaks the bit.++ The solution is to wrap exceptions up with a label. The exception+ may be caught, but only if the label of the exception can flow to+ the label at the point the catch statement began execution. For+ compatibility, the 'throwIO', 'catch', and 'onException' functions+ are now methods that work in both the 'IO' or 'LIO' monad.++ If an exception is uncaught in the 'LIO' monad, the 'evalLIO'+ function will unlabel and re-throw the exception, so that it is+ okay to throw exceptions from within the 'LIO' monad and catch them+ within the 'IO' monad. (Of course, code in the 'IO' monad must be+ careful not to let the 'LIO' code exploit it to exfiltrate+ information.)++ Wherever possible, however, code should use the 'catchP' and+ 'onExceptionP' variants that use whatever privilege is available to+ downgrade the exception. Privileged code that must always run some+ cleanup function can use the 'onExceptionTCB' and 'bracketTCB'+ functions to run the cleanup code on all exceptions.++ Note: Do not use 'throw' (as opposed to 'throwIO') within the+ 'LIO' monad. Because 'throw' can be invoked from pure code, it has+ no notion of current label and so cannot assign an appropriate+ label to the exception. As a result, the exception will not be+ catchable within the 'LIO' monad and will propagate all the way out+ of the 'evalLIO' function. Similarly, asynchronous exceptions+ (such as divide by zero or undefined values in lazily evaluated+ expressions) cannot be caught within the 'LIO' monad.++-}++instance Label l => Show (LabeledExceptionTCB l) where+ showsPrec _ (LabeledExceptionTCB l e) rest =+ shows e $ (" {" ++) $ shows l $ "}" ++ rest++instance (Label l) => Exception (LabeledExceptionTCB l)++instance (Label l) => MonadCatch (LIO l s) where+ block = iomap E.block+ unblock = iomap E.unblock+ -- |It is not possible to catch pure exceptions from within the 'LIO'+ -- monad, but @throwIO@ wraps up an exception with the current label,+ -- so that it can be caught with 'catch' or 'catchP'..+ throwIO e = mkLIO $ \s -> E.throwIO $+ LabeledExceptionTCB (lioL s) (toException e)+ -- | Basic function for catching labeled exceptions. (The fact that+ -- they are labeled is hidden from the handler.)+ --+ -- > catch m c = catchP m NoPrivs (\_ -> c)+ --+ catch m c = iomaps (\s m' -> m' `E.catch` doit s) m+ where+ doit s e@(LabeledExceptionTCB l se) =+ case fromException se of+ Just e' | l `leq` lioC s ->+ unLIO (c e') s { lioL = (lioL s) `lub` l }+ _ -> E.throwIO e++++-- | Catches an exception, so long as the label at the point where the+-- exception was thrown can flow to the label at which catchP is+-- invoked, modulo the privileges specified. Note that the handler+-- receives an an extra first argument (before the exception), which+-- is the label when the exception was thrown.+catchP :: (Label l, Exception e, Priv l p) =>+ p -- ^ Privileges with which to downgrade exception+ -> LIO l s a -- ^ Computation to run+ -> (l -> e -> LIO l s a) -- ^ Exception handler+ -> LIO l s a -- ^ Result of computation or handler+catchP p m c = iomaps (\s m' -> m' `E.catch` doit s) m+ where+ doit s e@(LabeledExceptionTCB l se) =+ case fromException se of+ Just e' -> let lnew = lostar p l (lioL s)+ in if leq lnew $ lioC s+ then unLIO (c l e') s { lioL = lnew }+ else E.throw e+ _ -> E.throw e++-- | Version of 'catchP' with arguments swapped.+handleP :: (Label l, Exception e, Priv l p) =>+ p -- ^ Privileges with which to downgrade exception+ -> (l -> e -> LIO l s a) -- ^ Exception handler+ -> LIO l s a -- ^ Computation to run+ -> LIO l s a -- ^ Result of computation or handler+handleP p = flip (catchP p)++-- | 'onException' cannot run its handler if the label was raised in+-- the computation that threw the exception. This variant allows+-- privileges to be supplied, so as to catch exceptions thrown with a+-- raised label.+onExceptionP :: (Priv l p) =>+ p -- ^ Privileges to downgrade exception+ -> LIO l s a -- ^ The computation to run+ -> LIO l s b -- ^ Handler to run on exception+ -> LIO l s a -- ^ Result if no exception thrown+onExceptionP p io what = catchP p io+ (\_ e -> what >> throwIO (e :: SomeException))++-- | Like standard 'E.bracket', but with privileges to downgrade+-- exception.+bracketP :: (Priv l p) =>+ p+ -> LIO l s a+ -> (a -> LIO l s c)+ -> (a -> LIO l s b)+ -> LIO l s b+bracketP p = genericBracket (onExceptionP p)++-- | For privileged code that needs to catch all exceptions in some+-- cleanup function. Note that for the 'LIO' monad, these methods do+-- /not/ call 'rethrowTCB' to label the exceptions. It is assumed+-- that you will use 'rtioTCB' instead of 'ioTCB' for IO within the+-- computation arguments of these methods.+class (MonadCatch m) => OnExceptionTCB m where+ onExceptionTCB :: m a -> m b -> m a+ bracketTCB :: m a -> (a -> m c) -> (a -> m b) -> m b+ bracketTCB = genericBracket onExceptionTCB+instance OnExceptionTCB IO where+ onExceptionTCB = E.onException+ bracketTCB = E.bracket+instance (Label l) => OnExceptionTCB (LIO l s) where+ onExceptionTCB m cleanup = + mkLIO $ \s -> unLIO m s `E.catch` \e ->+ unLIO cleanup s >> E.throwIO (e :: SomeException)++instance (Label l) => MonadError IOException (LIO l s) where+ throwError = throwIO+ catchError = catch++-- | Evaluate in LIO.+evaluate :: (Label l) => a -> LIO l s a+evaluate = rtioTCB . E.evaluate
+ LIO/TmpFile.hs view
@@ -0,0 +1,146 @@+{-# LANGUAGE ForeignFunctionInterface #-}++-- | This module creates new files and directories with unique names.+-- Its functionality is similary to C's mkstemp() and mkdtemp()+-- functions.+module LIO.TmpFile (-- * The high level interface+ mkTmpFile+ , mkTmpDir+ , mkTmpDir'+ -- * Some lower-level helper functions+ , mkTmp, openFileExclusive+ -- * Functions for generating unique names+ , tmpName, nextTmpName, serializele, unserializele+ -- * For flushing temp files before rename+ , hSync+ )where++import LIO.Armor++import Prelude hiding (catch)+import Control.Exception (throwIO, catch)+-- import qualified Control.Exception as IO+import Data.Bits (shiftL, shiftR, (.|.))+import qualified Data.ByteString.Lazy as L+import Data.Word (Word8)+import Foreign.C.Error+import Foreign.C.Types+import System.Directory (createDirectory)+import System.FilePath ((</>))+import System.Posix.IO (OpenMode(..), OpenFileFlags(..)+ , defaultFileFlags , openFd, fdToHandle)+import qualified System.IO as IO+import qualified System.IO.Error as IO+import System.Time (ClockTime(..), getClockTime)++import Data.Typeable+import GHC.IO.FD (FD(..))+import GHC.IO.Handle.Types (Handle__(..))+import GHC.IO.Handle.Internals (wantWritableHandle)++foreign import ccall "unistd.h fsync" c_fsync :: CInt -> IO CInt++--+-- Temporary file name based on time in 1/16 of a microsecond, then+-- step until unused file name found.+--++-- | Serialize an Integer into an array of bytes, in little-endian+-- order.+serializele :: Int -- ^ Minimum number of bytes to return+ -> Integer -- ^ The Integer to serialize+ -> [Word8]+serializele n i | n <= 0 && i <= 0 = []+serializele n i = (fromInteger i):serializele (n - 1) (i `shiftR` 8)++-- | Take an array of bytes containing an Integer serialized in+-- little-endian order, and return the Integer.+unserializele :: [Word8] -> Integer+unserializele [] = 0+unserializele (c:s) = (fromIntegral c) .|. (unserializele s `shiftL` 8)++-- | Return a temorary file name, based on the value of the current+-- time of day clock.+tmpName :: IO String+tmpName = do+ (TOD sec psec) <- getClockTime+ return $ armor32 $ L.pack $+ serializele 3 (psec `shiftR` 16) ++ serializele 4 sec++-- | When the file name returned by 'tmpName' already exists,+-- @nextTmpName@ modifies the file name to generate a new one.+nextTmpName :: String -> String+nextTmpName s =+ let val = unserializele $ L.unpack $ dearmor32 s+ in armor32 $ L.pack $ serializele 7 (1 + val)++-- | Opens a file in exclusive mode, throwing AlreadyExistsError if+-- the file name is already in use.+openFileExclusive :: IO.IOMode -> FilePath -> IO IO.Handle+openFileExclusive m p = do+ let dom = defaultFileFlags { exclusive = True }+ (om, fm) = case m of+ IO.WriteMode -> (WriteOnly, dom)+ IO.AppendMode -> (WriteOnly, dom { append = True })+ IO.ReadWriteMode -> (ReadWrite, dom)+ IO.ReadMode ->+ error "openFileExclusive: ReadMode is illegal"+ fd <- openFd p om (Just $ toEnum 0o666) fm+ fdToHandle fd++-- | Executes a function on temporary file names until the function+-- does not throw AlreadyExistsError. For example, 'mkTmpFile' is+-- defined as:+--+-- > mkTmpFile m d s = mkTmp (openFileExclusive m) d s+--+mkTmp :: (FilePath -> IO a) -- ^The function to execute (@f@)+ -> FilePath -- ^Directory to prepend to temp file names+ -> String -- ^Suffix for new file name+ -> IO (a, FilePath) -- ^The result of @f@ and the+ -- FilePath on which it finally+ -- succeeded.+mkTmp f dir suffix = tmpName >>= loop+ where+ ff n = case dir </> n of path -> do a <- f path; return (a, path)+ loop name = ff (name ++ suffix) `catch` reloop name+ reloop name e = if IO.isAlreadyExistsError e+ then loop $ nextTmpName name+ else throwIO e+++-- | Creates a new file with a unique name in a particular directory+mkTmpFile :: IO.IOMode -- ^@WriteMode@, @AppendMode@, or+ -- @ReadWriteMode@ (It is an error to+ -- use @ReadMode@.)+ -> FilePath -- ^Directory in which to create file+ -> String -- ^Suffix for new file name+ -> IO (IO.Handle, FilePath) -- ^Returns open handle to new+ -- file, along with pathname of+ -- new file+mkTmpFile m d s = mkTmp (openFileExclusive m) d s++-- | Creates a new subdirectory with uniqe file name. Returns the+-- pathname of the new directory as the second element of a pair, just+-- for consistency with the interface to 'mkTmpFile'. See+-- `mkTmpDir'` if you don't want this behavior.+mkTmpDir :: FilePath -- ^Directory in which to create subdirectory+ -> String -- ^Suffix to append to new directory name+ -> IO ((), FilePath) -- ^Returns full path to new directory+mkTmpDir d s = mkTmp createDirectory d s++-- | Like 'mkTmpDir', but just returns the pathname of the new directory.+mkTmpDir' :: FilePath -- ^Directory in which to create subdirectory+ -> String -- ^Suffix to append to new directory name+ -> IO FilePath -- ^Returns full path to new directory+mkTmpDir' d s = fmap snd $ mkTmpDir d s++-- | Flushes a Handle to disk with fsync()+hSync :: IO.Handle -> IO ()+hSync h = do+ IO.hFlush h+ wantWritableHandle "hSync" h $ fsyncH+ where+ fsyncH Handle__ {haDevice = dev} = maybe (return ()) fsyncD $ cast dev+ fsyncD FD {fdFD = fd} = throwErrnoPathIfMinus1_ "fsync" (show h)+ (c_fsync fd)
+ Setup.hs view
@@ -0,0 +1,3 @@+import Distribution.Simple+main :: IO ()+main = defaultMain
+ lio-eci11.cabal view
@@ -0,0 +1,75 @@+Name: lio-eci11+Version: 0.1+Cabal-Version: >= 1.2.3+build-type: Simple+License: GPL+License-File: LICENSE+Author: HAILS team+Stability: experimental+Maintainer: http://www.scs.stanford.edu/~dm/addr/+Category: Security+Synopsis: Labeled IO library+Extra-source-files:+ Examples/LambdaChair/Main.hs++Description: A package that provides dynamic tracking of information-flow. This package is intended to only be used at the computer science school ECI 2011 (Buenos Aires, Argentina) <http://www.dc.uba.ar/events/eci/2011/index_html>. Please, refer to the official version of this package if you intended to use it for other purposes. The /Labeled IO/ (LIO) library provides information flow+ control for incorporating untrusted code within Haskell+ applications. Most code should import module "LIO.LIO" and+ whichever label type the application is using (e.g.,+ "LIO.DCLabel"). The core functionality of the library is+ documented in "LIO.TCB". LIO was implemented by David+ Mazieres (<http://www.scs.stanford.edu/~dm/>), Deian Stefan+ (<http://www.scs.stanford.edu/~deian/>), Alejandro Russo+ (<http://www.cse.chalmers.se/~russo/>) and John C. Mitchell+ (<http://www.stanford.edu/~jcm/>).++ The extended version of our paper, that includes the proofs+ is available here:+ <http://www.scs.stanford.edu/~deian/lio/extended.pdf>.++ To obtain the latest experimental source code, run:+++ @git clone http:\/\/www.scs.stanford.edu\/~dm\/repos\/lio.git@++Library+ Build-Depends: base >= 4 && < 5,+ array >= 0.2 && < 1,+ bytestring >= 0.9 && < 1,+ containers >= 0.2 && < 1,+ directory >= 1.0 && < 2,+ filepath >= 1.1 && < 2,+ mtl >= 1.1.0.2 && < 3,+ old-time >= 1 && < 2,+ unix >= 2.3 && < 3,+ SHA >= 1.4.1.1 && < 2,+ time >= 1.1.4 && < 2,+ dclabel-eci11 >= 0.3 && < 2++ ghc-options: -O2 -funbox-strict-fields+ -threaded -fno-warn-unused-imports ++ Exposed-modules:+ LIO.Armor,+ LIO.Base,+ LIO.DCLabel,+ LIO.FS,+ LIO.Handle,+ LIO.HiStar,+ LIO.LIO,+ LIO.LIORef,+ LIO.MonadCatch,+ LIO.MonadLIO,+ LIO.TCB,+ LIO.TmpFile++ Extensions:+ DeriveDataTypeable,+ ExistentialQuantification,+ FlexibleContexts,+ FlexibleInstances,+ ForeignFunctionInterface,+ FunctionalDependencies,+ GeneralizedNewtypeDeriving,+ MultiParamTypeClasses,+ ScopedTypeVariables