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,31 @@
+import LIO.TCB
+import LIO.DCLabel
+import LIO.LIO
+import LambdaChair
+import DCLabel.PrettyShow
+import DCLabel.Safe
+
+import AliceCode as Alice
+import BobCode as Bob
+
+printL m = do
+ (_, l) <- m
+ putStrLn . prettyShow $ l
+
+main = printL . 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
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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
diff --git a/LIO/Armor.hs b/LIO/Armor.hs
new file mode 100644
--- /dev/null
+++ b/LIO/Armor.hs
@@ -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
+-}
+
diff --git a/LIO/Base.hs b/LIO/Base.hs
new file mode 100644
--- /dev/null
+++ b/LIO/Base.hs
@@ -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
+ )
diff --git a/LIO/DCLabel.hs b/LIO/DCLabel.hs
new file mode 100644
--- /dev/null
+++ b/LIO/DCLabel.hs
@@ -0,0 +1,114 @@
+{-| 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
+ {-
+ The implementation of lostar deserves an explanation. Firstly note
+ that the properties, for @r = lostar p l g@ that must be satisfied
+ are [the suffix \'s\' (\'i\')is used for seecrecy (resp. integrity):
+ 1.) @leq g r : (rs => gs) and (gi => ri)@
+ 2.) @leqp p l r : (rs /\ p => ls) and (li /\ p => ri)@
+ Finding the integrity component of @r@ is trivial: it's
+ simply the least upper bound of @gi@ and @li /\ p@.
+ Finding the secrecy component is a bit trickier. To do so, we first
+ find all the categories of @ls@ that are not implied by @p@ (this
+ gives us @rs'@), such that @rs' /\ p => ls@. Then, we need to find
+ the remaining categories in @gs@ that are not implied by @rs'@ (this
+ gives us @rs''@). Directly, @rs = rs' /\ rs''@.
+ -}
+ lostar p l g =
+ let (ls, li) = (secrecy l, integrity l)
+ (gs, gi) = (secrecy g, integrity g)
+ lp = DCL.priv p
+ rs' = c2l [c | c <- getCats ls
+ , not (lp `DCL.implies` (c2l [c]))]
+ rs'' = c2l [c | c <- getCats gs
+ , not (rs' `DCL.implies` (c2l [c]))]
+ rs = rs' `DCL.and_label` rs''
+ ri = (li `DCL.and_label` lp) `DCL.or_label` gi
+ in DCL.toLNF $ newDC rs ri
+ where getCats = DCL.conj . DCL.label
+ c2l = DCL.MkLabel . DCL.MkConj
+ {- OLD, BROKEN (was more elegant than above, so maybe use some ideas
+ when rewriting the above):
+ lostar p li lg =
+ let lip = newDC (DCL.secrecy li) ((DCL.integrity li) ./\. lp)
+ lgp = newDC ((DCL.secrecy lg) ./\. lp) (DCL.integrity lg)
+ lp = DCL.priv p
+ in DCL.join lip lgp
+ -}
+
+--
+-- 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 ()
diff --git a/LIO/FS.hs b/LIO/FS.hs
new file mode 100644
--- /dev/null
+++ b/LIO/FS.hs
@@ -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 ()
diff --git a/LIO/Handle.hs b/LIO/Handle.hs
new file mode 100644
--- /dev/null
+++ b/LIO/Handle.hs
@@ -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
+
diff --git a/LIO/HiStar.hs b/LIO/HiStar.hs
new file mode 100644
--- /dev/null
+++ b/LIO/HiStar.hs
@@ -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
+
+
diff --git a/LIO/LIO.hs b/LIO/LIO.hs
new file mode 100644
--- /dev/null
+++ b/LIO/LIO.hs
@@ -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
diff --git a/LIO/LIORef.hs b/LIO/LIORef.hs
new file mode 100644
--- /dev/null
+++ b/LIO/LIORef.hs
@@ -0,0 +1,8 @@
+-- |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. This module exports only the safe subset (non TCB) of the
+-- "LIORef" module -- trusted code can import "LIO.LIORef.TCB".
+module LIO.LIORef ( module LIO.LIORef.Safe) where
+
+import LIO.LIORef.Safe
diff --git a/LIO/LIORef/Safe.hs b/LIO/LIORef/Safe.hs
new file mode 100644
--- /dev/null
+++ b/LIO/LIORef/Safe.hs
@@ -0,0 +1,9 @@
+-- |This module exports the safe subset of the "LIO.LIORef.TCB" module.
+-- It is important that untrusted code be limited to this subset; information
+-- flow can easily be violated if the TCB functions are exported.
+module LIO.LIORef.Safe ( module LIO.LIORef.TCB ) where
+import LIO.LIORef.TCB hiding ( newLIORefTCB
+ , readLIORefTCB
+ , writeLIORefTCB
+ , atomicModifyLIORefTCB
+ )
diff --git a/LIO/LIORef/TCB.hs b/LIO/LIORef/TCB.hs
new file mode 100644
--- /dev/null
+++ b/LIO/LIORef/TCB.hs
@@ -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.TCB (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
+
diff --git a/LIO/MonadCatch.hs b/LIO/MonadCatch.hs
new file mode 100644
--- /dev/null
+++ b/LIO/MonadCatch.hs
@@ -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
diff --git a/LIO/MonadLIO.hs b/LIO/MonadLIO.hs
new file mode 100644
--- /dev/null
+++ b/LIO/MonadLIO.hs
@@ -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
diff --git a/LIO/TCB.hs b/LIO/TCB.hs
new file mode 100644
--- /dev/null
+++ b/LIO/TCB.hs
@@ -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
diff --git a/LIO/TmpFile.hs b/LIO/TmpFile.hs
new file mode 100644
--- /dev/null
+++ b/LIO/TmpFile.hs
@@ -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)
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+main :: IO ()
+main = defaultMain
diff --git a/lio.cabal b/lio.cabal
new file mode 100644
--- /dev/null
+++ b/lio.cabal
@@ -0,0 +1,82 @@
+Name: lio
+Version: 0.0.1
+Cabal-Version: >= 1.6
+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:
+ 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 (), Deian Stefan
+ (), Alejandro Russo
+ () and John C. Mitchell
+ ().
+
+ The extended version of our paper, that includes the proofs
+ is available here:
+ .
+
+ To obtain the latest experimental source code, run:
+
+ @git clone http:\/\/www.scs.stanford.edu\/~deian\/lio.git@.
+
+ The library depends on the @DCLabel@ module. You can read more on
+ DC Labels here:
+ .
+
+Source-repository head
+ Type: git
+ Location: http://www.scs.stanford.edu/~deian/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 >= 0.0.1 && < 2
+
+ Exposed-modules:
+ LIO.Armor,
+ LIO.Base,
+ LIO.DCLabel,
+ LIO.FS,
+ LIO.Handle,
+ LIO.HiStar,
+ LIO.LIO,
+ LIO.LIORef,
+ LIO.LIORef.TCB,
+ LIO.LIORef.Safe,
+ LIO.MonadCatch,
+ LIO.MonadLIO,
+ LIO.TCB,
+ LIO.TmpFile
+
+ Extensions:
+ DeriveDataTypeable,
+ ExistentialQuantification,
+ FlexibleContexts,
+ FlexibleInstances,
+ ForeignFunctionInterface,
+ FunctionalDependencies,
+ GeneralizedNewtypeDeriving,
+ MultiParamTypeClasses,
+ ScopedTypeVariables