diff --git a/LIO.hs b/LIO.hs --- a/LIO.hs +++ b/LIO.hs @@ -34,5 +34,5 @@ import safe LIO.Core import safe LIO.Delegate import safe LIO.Exception -import safe LIO.Label +import safe LIO.Label hiding (isPriv) import safe LIO.Labeled diff --git a/LIO/Concurrent/LMVar.hs b/LIO/Concurrent/LMVar.hs --- a/LIO/Concurrent/LMVar.hs +++ b/LIO/Concurrent/LMVar.hs @@ -6,13 +6,13 @@ This module implements labeled 'MVar's. The interface is analogous to "Control.Concurrent.MVar", but the operations take place in the 'LIO' monad. A labeled MVar, of type @'LMVar' l a@, is a mutable location -that can be in of of two states; an 'LMVar' can be empty, or it can be -full (with a value of type @a@). The location is protected by a label -of type 'l'. As in the case of @LIORef@s (see "LIO.LIORef"), this -label is fixed and does not change according to the content placed -into the location. Different from @LIORef@s, taking and putting -'LMVars' calls the write guard 'guardWrite' to enforce sound -information flow control. +that can be in one of two states; an 'LMVar' can be empty, or it can +be full (with a value of type @a@). The location is protected by a +label of type 'l'. As in the case of @LIORef@s (see "LIO.LIORef"), +this label is fixed and does not change according to the content +placed into the location. Unlike @LIORef@s, most operations use +'guardWrite' or 'guardWriteP', reflecting the fact that there is no +such thing as read-only or write-only operations on an 'LMVar'. 'LMVar's can be used to build synchronization primitives and communication channels ('LMVar's themselves are single-place diff --git a/LIO/Core.hs b/LIO/Core.hs --- a/LIO/Core.hs +++ b/LIO/Core.hs @@ -269,9 +269,11 @@ unless (canFlowTo l newl && canFlowTo newl c) $ labelError "guardAllocP" [newl] --- | Like 'guardAlloc', but takes privilege argument to be more +-- | Like 'guardAlloc', but takes a privilege argument to be more -- permissive. Note: privileges are /only/ used when checking that --- the current label can flow to the given label. +-- the current label can flow to the target label; @guardAllocP@ still +-- always throws an exception when the target label is higher than the +-- current clearance. guardAllocP :: PrivDesc l p => Priv p -> l -> LIO l () guardAllocP p newl = do LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB diff --git a/LIO/DCLabel.hs b/LIO/DCLabel.hs --- a/LIO/DCLabel.hs +++ b/LIO/DCLabel.hs @@ -41,7 +41,7 @@ e2 = e1 '\/' \"p4\" @ -Similarly, the conjunction operator ('/\') creates 'CNF' as a +Similarly, the conjunction operator ('/\') creates a 'CNF' as a conjunction of 'Principal's, 'String's, 'Disjunction's, or 'CNF's. @ @@ -79,6 +79,22 @@ >>> canFlowToP pr dc1 dc2 True +Because the '\/' and '/\' operators accept strings and 'Principal's as +well as 'CNF's, it is sometimes easy to forget that strings and +'Principal's are not actually 'CNF's. For example: + +>>> "Alice" /\ "Bob" `speaksFor` "Alice" \/ "Bob" +True +>>> "Alice" `speaksFor` "Alice" \/ "Bob" +:12:21: + Couldn't match expected type `[Char]' with actual type `CNF' + +To convert a single string or 'Principal' to a 'CNF', you must use the +'toCNF' method: + +>>> toCNF "Alice" `speaksFor` "Alice" \/ "Bob" +True + -} module LIO.DCLabel ( @@ -266,7 +282,7 @@ -- @'dcSecrecy' = cTrue@, it means data is public. When -- @'dcIntegrity' = cTrue@, it means data carries no integrity -- guarantees. As a description of privileges, @cTrue@ conveys no --- privileges; @'canFlowToPrivDesc' cTrue l1 l2@ is equivalent to +-- privileges; @'canFlowToP' cTrue l1 l2@ is equivalent to -- @'canFlowTo' l1 l2@. -- -- Note that @'toCNF' 'True' = cTrue@. Hence @'dcPublic' = 'DCLabel' @@ -359,11 +375,11 @@ -- other words, data can flow in the direction of requiring more -- authority to make it public or removing integrity endorsements. -- --- * Given two @DCLabel@s @dc1 = (s1 '%%' i1)@ and @dc 2 = (s2 '%%' --- i2)@, and a @p::'CNF'@ representing privileges, --- @'canFlowToPrivDesc' p dc1 dc2@ (often written @dc1@ --- ⊑ₚ @dc2@) if and only if @(p '/\' s2) ``speaksFor`` --- s2 && (p '/\' i1) ``speaksFor`` i2@. +-- * Given two @DCLabel@s @dc1 = (s1 '%%' i1)@ and @dc2 = (s2 '%%' +-- i2)@, and a @p::'CNF'@ representing privileges, @'canFlowToP' p +-- dc1 dc2@ (often written @dc1@ ⊑ₚ @dc2@) if and only +-- if @(p '/\' s2) ``speaksFor`` s2 && (p '/\' i1) ``speaksFor`` +-- i2@. data DCLabel = DCLabel { dcSecrecy :: !CNF -- ^ Describes the authority required to make -- the data public. @@ -390,10 +406,9 @@ -- This label corresponds to public data with no integrity guarantees. -- For instance, an unrestricted Internet socket should be labeled -- @dcPublic@. The significance of @dcPublic@ is that given data --- labeled @(s %% i)@, @s@ is the exact minimum authority required to --- transition the data to @dcPublic@. Conversely, given data labeled --- @dcPublic@, @i@ is the exact authority required to transition the --- data to @(s %% i)@ (assuming sufficient clearance). +-- labeled @(s %% i)@, @s@ is the exact minimum authority such that +-- @(s %% i) ⊑ₛ dcPublic@, while @i@ is the exact +-- minimum authority such that @dcPublic ⊑ᵢ (s %% i)@. dcPublic :: DCLabel dcPublic = True %% True diff --git a/LIO/Delegate.hs b/LIO/Delegate.hs --- a/LIO/Delegate.hs +++ b/LIO/Delegate.hs @@ -10,7 +10,7 @@ delegate -- * Gates -- $gateIntro - , Gate, gate, callGate + , Gate, gate, guardGate, callGate -- ** Gate example -- $gateExample ) where @@ -25,8 +25,8 @@ -- less powerful than an existing privilege object. The first -- argument supplies actual privileges. The second argument is a -- 'PrivDesc' describing the desired new privileges. The call throws --- an exception unless the privileges supplied 'speaksFor' the --- privileges requested. +-- an exception unless the privilege object supplied 'speaksFor' the +-- privilege object requested. -- -- Note: If you are looking for a way to create privileges /more/ -- powerful than ones you already have, you can use the 'mappend' @@ -34,7 +34,7 @@ delegate :: (SpeaksFor p) => Priv p -> p -> Priv p delegate p1 p2 | privDesc p1 `speaksFor` p2 = PrivTCB p2 - | otherwise = insufficientPrivs "delegate" p1 p2 + | otherwise = insufficientPrivs "delegate" (privDesc p1) p2 {- $gateIntro @@ -48,12 +48,18 @@ invoked with 'callGate', and as such the service provider has the guarantee that the client (the caller) owns the privileges corresponding to the privilege description @p@. In effect, this -allows a client to \"prove\" to the service provider that they own -certain privileges without entrusting the service with its privileges. -The gate computation can analyze this privilege description before -performing the \"actual\" computation. The client and server solely -need to trust the implementation of 'callGate'. +allows a client to \"prove\" to the service provider that it owns +certain privileges without actually entrusting the service with these +privileges. The gate computation can analyze this privilege +description before performing the \"actual\" computation. The +'speaksFor' function may be useful. When supplied privileges are +insufficient, the gate code can raise an exception with +'insufficientPrivs'. +Note that the client and server must both trust the implementation of +'callGate', which is why it is part of the LIO library, even though +the function itself is only one line of code. + -} @@ -75,6 +81,21 @@ -> Gate p a {-# INLINE gate #-} gate = GateTCB + +-- | @guardGate name minPriv a@ creates a simple gate that requires +-- privileges at least as high as @minPriv@ to return the payload or +-- function @a@. If the privileges supplied are insufficient, an +-- exception of type 'InsufficientPrivs' is thrown. The argument +-- @name@ is used only when an exception is thrown, to make the source +-- of the exception more easily traceable. +-- +-- > guardGate name minPriv a = gate $ \pd -> +-- > if pd `speaksFor` minPriv then a +-- > else insufficientPrivs name pd minPriv +guardGate :: (SpeaksFor p) => String -> p -> a -> Gate p a +guardGate name minPriv a = gate $ \pd -> + if pd `speaksFor` minPriv then a + else insufficientPrivs name pd minPriv -- | Given a gate and privilege, execute the gate computation. It is -- important to note that @callGate@ invokes the gate computation with diff --git a/LIO/Error.hs b/LIO/Error.hs --- a/LIO/Error.hs +++ b/LIO/Error.hs @@ -44,7 +44,7 @@ instance Exception AnyLabelError --- | Executes an action with a context string which will be added to +-- | Executes an action with a context string, which will be added to -- any label exception thrown. -- -- Note: this function wraps an action with a 'catch', and thus may @@ -151,10 +151,15 @@ fromException = lerrFromException -- | Raise 'InsufficientPrivs' error. -insufficientPrivs :: (SpeaksFor p) => String -> Priv p -> p -> a -insufficientPrivs fl supplied needed = - IO.throw $ InsufficientPrivs [] fl (privDesc supplied) needed - +insufficientPrivs :: (SpeaksFor p) => + String -- ^ Function in which error occurs + -> p -- ^ Description of privileges supplied + -> p -- ^ Description of privileges needed + -> a +insufficientPrivs fl supplied needed + | isPriv supplied = error $ "insufficientPrivs: " ++ show fl ++ + " supplied actual privileges instead of description" + | otherwise = IO.throw $ InsufficientPrivs [] fl supplied needed -- | Error raised when a computation spawned by 'lFork' terminates -- with its current label above the label of the result. diff --git a/LIO/LIORef.hs b/LIO/LIORef.hs --- a/LIO/LIORef.hs +++ b/LIO/LIORef.hs @@ -41,17 +41,16 @@ -- -- | An @LIORef@ is an @IORef@ with an associated, fixed label. The --- restriction to an immutable label come from the fact that it is --- possible to leak information through the label itself, if we wish to --- allow @LIORef@ to be an instance of 'LabelOf'. Of course, you can --- create an @LIORef@ of 'Labeled' to get a limited form of +-- restriction to an immutable label comes from the fact that it is +-- possible to leak information through the label itself, since we +-- wish to allow @LIORef@ to be an instance of 'LabelOf'. Of course, +-- you can create an @LIORef@ of 'Labeled' to get a limited form of -- flow-sensitivity. type LIORef l a = LObj l (IORef a) --- | To create a new reference the label of the reference must be --- below the thread's current clearance and above the current label. --- If this is the case, the reference is built. Otherwise an exception --- will be thrown by the underlying 'guardAlloc' guard. +-- | Create a new reference with a particularlabel. The label +-- specified must be between the thread's current label and clearance, +-- as enforced by 'guardAlloc'. newLIORef :: Label l => l -- ^ Label of reference -> a -- ^ Initial value @@ -60,9 +59,9 @@ withContext "newLIORef" $ guardAlloc l ioTCB (LObjTCB l `fmap` newIORef a) --- | Same as 'newLIORef' except @newLIORefP@ takes a set of --- privileges which are accounted for in comparing the label of --- the reference to the current label and clearance. +-- | Same as 'newLIORef' except @newLIORefP@ takes privileges which +-- make the comparison to the current label more permissive, as +-- enforced by 'guardAllocP'. newLIORefP :: PrivDesc l p => Priv p -> l -> a -> LIO l (LIORef l a) newLIORefP p l a = do withContext "newLIORefP" $ guardAllocP p l @@ -72,18 +71,20 @@ -- Read 'LIORef's -- --- | Read the value of a labeled reference. A read succeeds only if the --- label of the reference is below the current clearance. Moreover, --- the current label is raised to the join of the current label and --- the reference label. To avoid failures (introduced by the 'taint' --- guard) use 'labelOf' to check that a read will succeed. +-- | Read the value of a labeled reference. A read succeeds only if +-- the label of the reference is below the current +-- clearance. Moreover, the current label is raised to the 'lub' of +-- the current label and the reference label. To avoid failures +-- (introduced by the 'taint' guard) use 'labelOf' to check that a +-- read will succeed. readLIORef :: Label l => LIORef l a -> LIO l a readLIORef (LObjTCB l r) = do withContext "readLIORef" $ taint l ioTCB (readIORef r) --- | Same as 'readLIORef' except @readLIORefP@ takes a privilege object --- which is used when the current label is raised. +-- | Same as 'readLIORef', except @readLIORefP@ takes a privilege +-- object which is used when the current label is raised (using +-- 'taintP' instead of 'taint'). readLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> LIO l a readLIORefP p (LObjTCB l r) = do withContext "readLIORefP" $ taintP p l @@ -103,8 +104,8 @@ ioTCB (writeIORef r a) -- | Same as 'writeLIORef' except @writeLIORefP@ takes a set of --- privileges which are accounted for in comparing the label of --- the reference to the current label and clearance. +-- privileges which are accounted for in comparing the label of the +-- reference to the current label. writeLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> a -> LIO l () writeLIORefP p (LObjTCB l r) a = do withContext "writeLIORefP" $ guardAllocP p l @@ -114,14 +115,14 @@ -- Modify 'LIORef's -- --- | Mutate the contents of a labeled reference. For the mutation to --- succeed it must be that the current label can flow to the label of the --- reference, and the label of the reference can flow to the current --- clearance. Note that because a modifier is provided, the reference --- contents are not observable by the outer computation and so it is not --- required that the current label be raised. It is, however, required --- that the label of the reference be bounded by the current label and --- clearance (as checked by the underlying 'guardAlloc' guard). +-- | Mutate the contents of a labeled reference. The mutation is +-- performed by a a pure function, which, because of laziness, is not +-- actually evaluated until such point as a (possibly higher-labeled) +-- thread actually reads the 'LIORef'. The caller of @modifyLIORef@ +-- learns no information about the previous contents the 'LIORef'. +-- For that reason, there is no need to raise the current label. The +-- `LIORef`'s label must still lie between the current label and +-- clearance, however (as enforced by 'guardAlloc'). modifyLIORef :: Label l => LIORef l a -- ^ Labeled reference -> (a -> a) -- ^ Modifier @@ -130,9 +131,8 @@ withContext "modifyLIORef" $ guardAlloc l ioTCB (modifyIORef r f) --- | Same as 'modifyLIORef' except @modifyLIORefP@ takes a set of --- privileges which are accounted for in comparing the label of --- the reference to the current label and clearance. +-- | Like 'modifyLIORef', but takes a privilege argument and guards +-- execution with 'guardAllocP' instead of 'guardAlloc'. modifyLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> (a -> a) -> LIO l () modifyLIORefP p (LObjTCB l r) f = do @@ -146,13 +146,13 @@ -- computation is \"tainted\" by the reference label (i.e., the -- current label is raised to the 'join' of the current and reference -- labels). These checks and label raise are done by 'guardWrite', --- which will raise an exception if any of the IFC conditions cannot --- be satisfied. +-- which will raise a 'LabelError' exception if any of the IFC +-- conditions cannot be satisfied. atomicModifyLIORef :: Label l => LIORef l a -> (a -> (a, b)) -> LIO l b atomicModifyLIORef = blessTCB "atomicModifyIORef" atomicModifyIORef --- | Same as 'atomicModifyLIORef' except @atomicModifyLIORefP@ takes --- a set of privileges which are accounted for in label comparisons. +-- | Same as 'atomicModifyLIORef' except @atomicModifyLIORefP@ takes a +-- set of privileges and uses 'guardWriteP' instead of 'guardWrite'. atomicModifyLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> (a -> (a, b)) -> LIO l b atomicModifyLIORefP = blessPTCB "atomicModifyLIORefP" atomicModifyIORef diff --git a/LIO/Label.hs b/LIO/Label.hs --- a/LIO/Label.hs +++ b/LIO/Label.hs @@ -12,6 +12,8 @@ -- $Privileges , SpeaksFor(..), PrivDesc(..) , Priv, privDesc + -- ** Internal functions + , isPriv -- * Empty privileges , NoPrivs(..), noPrivs ) where @@ -45,7 +47,7 @@ that @l1 ``canFlowTo`` lcur@. If the thread is later permitted to modify an object labeled @l2@, it must hold that @lcur ``canFlowTo`` l2@. By transitifity of the ``canFlowTo`` relation, it holds that @l1 -``canFlowTo` l2@. +``canFlowTo`` l2@. -} @@ -142,15 +144,15 @@ allowing data labeled @l1@ to infulence data labeled @l2@ when @(l1 ``canFlowTo`` l2) == False@ is known as /downgrading/. -The core privilege function is 'canFlowToP', which performs a -more permissive can-flow-to check by exercising particular privileges -(in literature this relation is commonly written @⊑ₚ@ for +The core privilege function is 'canFlowToP', which performs a more +permissive can-flow-to check by exercising particular privileges (in +the literature this relation is commonly written @⊑ₚ@ for privileges @p@). Most core 'LIO' function have variants ending @...P@ that take a privilege argument to act in a more permissive way. By convention, all 'PrivDesc' instances should also be instances of 'Monoid', allowing privileges to be combined with 'mappend', though -this is not enforced with superclasses. +there is no superclass to enforce this. -} @@ -161,10 +163,25 @@ {-# INLINE privDesc #-} privDesc (PrivTCB a) = a --- | Every privilege type must be an instance of 'SpeaksFor', which --- specifies when one privilege value is more powerful than another. --- If you do not wish to allow delegation, you can simply define --- @'speaksFor' _ _ = False@. +-- | Uses dynamic typing to return 'True' iff the type of the argument +-- is @'Priv' a@ (for any @a@). Mostly useful to prevent users from +-- accidentally wrapping 'Priv' objects inside other 'Priv' objects or +-- accidentally including real privileges in an exception. +isPriv :: (Typeable p) => p -> Bool +isPriv p = typeRepTyCon (typeOf p) == privcon + where privcon = typeRepTyCon $ typeOf noPrivs + +-- | Every privilege type must be an instance of 'SpeaksFor', which is +-- a partial order specifying when one privilege value is at least as +-- powerful as another. If @'canFlowToP' p1 l1 l2@ and @p2 +-- `speaksFor` p1@, then it should also be true that @'canFlowToP' p2 +-- l1 l2@. +-- +-- As a partial order, 'SpeaksFor' should obeying the reflexivity, +-- antisymmetry and transitivity laws. However, if you do not wish to +-- allow delegation of a particular privilege type, you can define +-- @'speaksFor' _ _ = False@ (which violates the reflexivity law, but +-- is reasonable when you don't want the partial order). class (Typeable p, Show p) => SpeaksFor p where -- | @speaksFor p1 p2@ returns 'True' iff @p1@ subsumes all the -- privileges of @p2@. In other words, it is safe for 'delegate' to diff --git a/LIO/Labeled.hs b/LIO/Labeled.hs --- a/LIO/Labeled.hs +++ b/LIO/Labeled.hs @@ -17,10 +17,11 @@ data. This module exports functions for creating labeled values ('label'), using the values protected by 'Labeled' by unlabeling them ('unlabel'), and changing the value of a labeled value without -inspection ('relabelLabeledP', 'taintLabeled'). A -'Functor'-like class ('LabeledFunctor') on 'Labeled' is also defined -in this module. +inspection ('relabelLabeledP', 'taintLabeled'). +Two 'Applicative' 'Functor'-like operations are also defined for +'Labeled' data, namely 'lFmap' and 'lAp'. + -} module LIO.Labeled ( @@ -46,24 +47,24 @@ -- Label values -- --- | Function to construct a '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 --- ``canFlowTo`` l && l ``canFlowTo`` ccurrent@. Otherwise an --- exception is thrown (see 'guardAlloc'). +-- | Function to construct a 'Labeled' value from a label and a pure +-- value. If the current label is @lcurrent@ and the current +-- clearance is @ccurrent@, then the label @l@ specified must satisfy +-- @lcurrent ``canFlowTo`` l && l ``canFlowTo`` ccurrent@. Otherwise +-- an exception is thrown (see 'guardAlloc'). label :: Label l => l -> a -> LIO l (Labeled l a) label l a = do withContext "label" $ guardAlloc l return $ LabeledTCB l a --- | Constructs a 'Labeled' using privilege to allow the `Labeled`'s +-- | Constructs a 'Labeled' value using privilege to allow the value'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 @canFlowTo p lcurrent l@ and --- @l ``canFlowTo`` ccurrent@. Note that privilege is not used to bypass --- the clearance. You must use 'setClearanceP' to raise the clearance --- first if you wish to create an 'Labeled' at a higher label than the --- current clearance. +-- @lcurrent@ and the current clearance is @ccurrent@, then the +-- privilege @p@ and label @l@ specified must satisfy @canFlowTo p +-- lcurrent l@ and @l ``canFlowTo`` ccurrent@. Note that privilege is +-- not used to bypass the clearance. You must use 'setClearanceP' to +-- raise the clearance first if you wish to create a 'Labeled' value +-- at a higher label than the current clearance. labelP :: PrivDesc l p => Priv p -> l -> a -> LIO l (Labeled l a) labelP p l a = do withContext "labelP" $ guardAllocP p l @@ -73,24 +74,31 @@ -- Unlabel values -- --- | Within the 'LIO' monad, this function takes a 'Labeled' and returns --- the underlying value. Thus, in the 'LIO' monad one can say: +-- | Within the 'LIO' monad, this function takes a 'Labeled' value and +-- returns it as an unprotected value of the inner type. For +-- instance, in the 'LIO' monad one can say: -- --- > x <- unlabel (xv :: Labeled SomeLabelType Int) +-- > x <- unlabel (lx :: Labeled SomeLabelType Int) -- --- And now it is possible to use the value of @x :: Int@, 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 'ClearanceViolation'. --- However, you can use 'labelOf' to check if 'unlabel' will succeed --- without throwing an exception. +-- And now it is possible to use the pure value @x :: Int@, which was +-- previously protected by a label in @lx@. +-- +-- @unlabel@ raises the current label as needed to reflect the fact +-- that the thread's behavior can now depend on the contents of @lx@. +-- If @unlabel@ing a value would require raising the current label +-- above the current clearance, then @unlabel@ throws an exception of +-- type 'LabelError'. You can use 'labelOf' to check beforehand +-- whether 'unlabel' will succeed. unlabel :: Label l => Labeled l a -> LIO l a unlabel (LabeledTCB l v) = withContext "unlabel" (taint l) >> return v --- | Extracts the value of an 'Labeled' just like 'unlabel', but takes a --- privilege argument to minimize the amount the current label must be --- raised. Function will throw 'ClearanceViolation' under the same --- circumstances as 'unlabel'. +-- | Extracts the contents of a 'Labeled' value just like 'unlabel', +-- but takes a privilege argument to minimize the amount the current +-- label must be raised. The privilege is used to raise the current +-- label less than might be required otherwise, but this function does +-- not change the current clarance and still throws a 'LabelError' if +-- the privileges supplied are insufficient to save the current label +-- from needing to exceed the current clearance. unlabelP :: PrivDesc l p => Priv p -> Labeled l a -> LIO l a unlabelP p (LabeledTCB l v) = withContext "unlabelP" (taintP p l) >> return v @@ -99,29 +107,30 @@ -- -- | Relabels a 'Labeled' value to the supplied label if the given --- privilege privileges permits it. An exception is thrown unless the --- following two conditions hold: +-- privileges permit it. An exception is thrown unless the following +-- two conditions hold: -- --- 1. The new label must be between the current label and clearance --- (modulo privileges), as enforced by 'guardAllocP'. +-- 1. The new label must be below the current clearance. -- --- 2. The old label must flow to the new label (again modulo --- privileges), as enforced by 'canFlowToP'. +-- 2. The old label and new label must be equal (modulo privileges), +-- as enforced by 'canFlowToP'. -- relabelLabeledP :: PrivDesc l p => Priv p -> l -> Labeled l a -> LIO l (Labeled l a) relabelLabeledP p newl (LabeledTCB oldl v) = do - withContext "relabelLabeledP" $ guardAllocP p newl - unless (canFlowToP p oldl newl) $ - labelErrorP "relabelLabeledP" p [oldl, newl] + clr <- getClearance + unless (canFlowTo newl clr && + canFlowToP p newl oldl && + canFlowToP p oldl newl) $ labelErrorP "relabelLabeledP" p [oldl, newl] return $ LabeledTCB newl v --- | Raises the label of a 'Labeled' to the 'upperBound' of it's current --- label and the value supplied. The label supplied must be bounded by --- the current label and clearance, though the resulting label may not be --- if the 'Labeled' is already above the current thread's clearance. If --- the supplied label is not bounded then @taintLabeled@ will throw an --- exception (see 'guardAlloc'). +-- | Raises the label of a 'Labeled' value to the 'lub' of it's +-- current label and the value supplied. The label supplied must be +-- bounded by the current label and clearance, though the resulting +-- label may not be if the 'Labeled' value's label is already above +-- the current thread's clearance. If the supplied label is not +-- bounded then @taintLabeled@ will throw an exception (see +-- 'guardAlloc'). taintLabeled :: Label l => l -> Labeled l a -> LIO l (Labeled l a) taintLabeled l (LabeledTCB lold v) = do let lnew = lold `lub` l @@ -160,9 +169,13 @@ -} --- | Similar to 'fmap', apply function to the 'Labeled' value. The --- label of the returned value is the least upper bound of the current --- label and label of the supplied labeled value. +-- | A function similar to 'fmap' for 'Labeled' values. Applies a +-- function to a 'Labeled' value without 'unlabel'ing the value or +-- changing the thread's current label. The label of the result is the +-- 'lub' of the current label and that of the supplied 'Labeled' +-- value. Because of laziness, the actual computation on the value of +-- type @a@ will be deferred until a thread with a higher label +-- actually 'unlabel's the result. lFmap :: Label l => Labeled l a -> (a -> b) -> LIO l (Labeled l b) lFmap (LabeledTCB lold v) f = do l <- getLabel @@ -173,9 +186,9 @@ -- | Similar to 'ap', apply function (wrapped by 'Labeled') to the --- labeld value. The label of the returned value is the least upper --- bound of the current label, label of the supplied labeled value, --- and label of the supplied function. +-- labeld value. The label of the returned value is the 'lub' of the +-- thread's current label, the label of the supplied function, and the +-- label of the supplied value. lAp :: Label l => Labeled l (a -> b) -> Labeled l a -> LIO l (Labeled l b) lAp (LabeledTCB lf f) (LabeledTCB la a) = do l <- getLabel diff --git a/LIO/Run.hs b/LIO/Run.hs --- a/LIO/Run.hs +++ b/LIO/Run.hs @@ -13,7 +13,6 @@ import safe Control.Exception import safe Data.IORef -import safe Data.Typeable import safe LIO.Label import LIO.TCB @@ -69,10 +68,3 @@ privInit :: (SpeaksFor p) => p -> IO (Priv p) privInit p | isPriv p = fail "privInit called on Priv object" | otherwise = return $ PrivTCB p - --- | Uses dynamic typing to return 'True' iff the type of the argument --- is @'Priv' a@ (for any @a@). Mostly useful to prevent users from --- accidentally wrapping 'Priv' objects inside other 'Priv' objects. -isPriv :: (Typeable p) => p -> Bool -isPriv p = typeRepTyCon (typeOf p) == privcon - where privcon = typeRepTyCon $ typeOf noPrivs diff --git a/LIO/TCB.hs b/LIO/TCB.hs --- a/LIO/TCB.hs +++ b/LIO/TCB.hs @@ -9,7 +9,7 @@ \"@...TCB@\" (short for \"trusted computing base\"). In many cases, a type is safe to export while its constructor is not. Hence, only the constructor ends \"@TCB@\", while the type is re-exported to safe code -(without constructors) to from "LIO.Core". +(without constructors) from "LIO.Core". Security rests on the fact that untrusted code must be compiled with @-XSafe@. Because this module is flagged unsafe, it cannot be @@ -183,14 +183,14 @@ -- instance, if you wish to associate a label with a pure value (as in -- "LIO.Labeled"), you may create a data type: -- --- > newtype LVal l a = LValTCB (l, a) +-- > data LVal l a = LValTCB l a -- -- Then, you may wish to allow untrusted code to read the label of any -- @LVal@s but not necessarily the actual value. To do so, simply -- provide an instance for @LabelOf@: -- -- > instance LabelOf LVal where --- > labelOf (LValTCB lv) = fst lv +-- > labelOf (LValTCB l a) = l class LabelOf t where -- | Get the label of a labeled value or object. Note the label -- must be the second to last type constructor argument. @@ -231,6 +231,9 @@ , lresLabelTCB :: !l -- ^ Label of the tresult , lresBlockTCB :: !(IO.MVar ()) + -- ^ This 'MVar' is empty until such point as 'lresStatusTCB' is + -- no longer 'LResEmpty'. Hence, calling 'readMVar' on this field + -- allows one to wait for the thread to terminate. , lresStatusTCB :: !(IORef (LResStatus l a)) -- ^ Result (when it is ready), or the label at which the thread -- terminated, if that label could not flow to 'lresLabelTCB'. diff --git a/LIO/TCB/LObj.hs b/LIO/TCB/LObj.hs --- a/LIO/TCB/LObj.hs +++ b/LIO/TCB/LObj.hs @@ -18,10 +18,13 @@ -- > type Handle = LObj DCLabel IO.Handle -- > -- > hPutStrLn :: LObj DCLabel IO.Handle -> String -> LIO DCLabel () --- > hPutStrLn h = blessTCB IO.hPutStrLn noPrivs h +-- > hPutStrLn h = blessTCB "hPutStrLn" IO.hPutStrLn h +-- > +-- > hPutStrLnP :: DCPriv -> LObj DCLabel IO.Handle -> String -> LIO DCLabel () +-- > hPutStrLnP h = blessPTCB "hPutStrLnP" IO.hPutStrLn h -- > -- > hGetLine :: LObj DCLabel IO.Handle -> LIO DCLabel String --- > hGetLine h = blessTCB IO.hGetLine noPrivs h +-- > hGetLine h = blessTCB "hGetLine" IO.hGetLine h -- -- Then application-specific trusted code can wrap a specific label -- around each 'Handle' using the 'LObjTCB' constructor. @@ -37,9 +40,9 @@ -- | A \"@LObj label object@\" is a wrapper around an IO abstraction -- of type @object@ (such as a file handle or socket) on which it is -- safe to do @IO@ operations in the 'LIO' monad when the caller can --- read and write a particular label. It is the job of the trusted +-- read and write a the label @label@. It is the job of the trusted -- code constructing such a @LObj@ object to ensure both that the same --- IO object is only ever blessed with one label, and that the +-- IO object is only ever associated with a single label, and that the -- abstraction combined with its blessed IO operations (see -- 'blessTCB') cannot be used to communicate with code running at -- different labels. @@ -117,7 +120,8 @@ blessTCB name io (LObjTCB l a) = guardIOTCB (withContext name $ guardWrite l) (io a) --- | A variant of 'blessTCB' that takes a privilege argument. +-- | A variant of 'blessTCB' that produces an 'LIO' function taking a +-- privilege argument. blessPTCB :: (GuardIO l io lio, PrivDesc l p) => String -> (a -> io) -> Priv p -> (LObj l a) -> lio {-# INLINE blessPTCB #-} diff --git a/examples/dclabel.hs b/examples/dclabel.hs --- a/examples/dclabel.hs +++ b/examples/dclabel.hs @@ -5,20 +5,20 @@ import LIO.DCLabel -- | Simple secrecy component example -s :: Component -s = "Alice" \/ "Bob" /\ "Carla" +s :: CNF +s = ("Alice" \/ "Bob") /\ "Carla" -- | Simple integrity component example -i :: Component +i :: CNF i = "Alice" /\ "Carla" -- | Simple label l1 :: DCLabel -l1 = dcLabel s i +l1 = s %% i -- | Simple label l2 :: DCLabel -l2 = dcLabel (toComponent "Djon") (toComponent "Alice") +l2 = "Djon" %% "Alice" -- | Creating privilege using constructor from TCB p :: DCPriv @@ -36,12 +36,11 @@ {- Output: ghci> main -Label 1: < {[Carla] /\ [Alice \/ Bob]} , {[Alice] /\ [Carla]} > -Label 2: < {[Djon]} , {[Alice]} > -Join of labels: < {[Carla] /\ [Djon] /\ [Alice \/ Bob]} , {[Alice]} > -Meet of labels: < {[Carla \/ Djon] /\ [Alice \/ Bob \/ Djon]} , -{[Alice] /\ [Carla]} > -Privileges: DCPrivTCB {unDCPriv = {[Alice] /\ [Carla]}} +Label 1: "Carla" /\ ("Alice" \/ "Bob") %% "Alice" /\ "Carla" +Label 2: "Djon" %% "Alice" +Join of labels: "Carla" /\ "Djon" /\ ("Alice" \/ "Bob") %% "Alice" +Meet of labels: ("Carla" \/ "Djon") /\ ("Alice" \/ "Bob" \/ "Djon") %% "Alice" /\ "Carla" +Privileges: PrivTCB ("Alice" /\ "Carla") Label 1 flows to Label 2? False Label 1 flows to Label 2 given privileges? True -} diff --git a/examples/gate.hs b/examples/gate.hs --- a/examples/gate.hs +++ b/examples/gate.hs @@ -1,21 +1,22 @@ import LIO +import LIO.Delegate import LIO.DCLabel import LIO.TCB -- | Add two numbers if the computation is invoked by Alice or Bob. -addGate :: DCGate (Int -> Int -> Maybe Int) +addGate :: Gate CNF (Int -> Int -> Maybe Int) addGate = gate $ \pd a b -> - if pd `elem` (map dcPrivDesc ["Alice", "Bob"]) + if pd `elem` (map toCNF ["Alice", "Bob"]) then Just $ a + b else Nothing alice, bob, clark :: DCPriv -alice = PrivTCB . dcPrivDesc $ "Alice" -bob = PrivTCB . dcPrivDesc $ "Bob" -clark = PrivTCB . dcPrivDesc $ "Clark" +alice = PrivTCB . toCNF $ "Alice" +bob = PrivTCB . toCNF $ "Bob" +clark = PrivTCB . toCNF $ "Clark" main = putStrLn . show $ [ callGate addGate alice 1 2 -- Just 3 diff --git a/examples/sign.hs b/examples/sign.hs new file mode 100644 --- /dev/null +++ b/examples/sign.hs @@ -0,0 +1,14 @@ +import LIO +import LIO.DCLabel +import LIO.TCB + +amit = PrivTCB $ toCNF "amit" +deian = PrivTCB $ toCNF "deian" + +l1 = True %% privDesc amit +l2 = True %% amit /\ deian + +main = tryDC $ do + lv1 <- labelP amit l1 "w00t" + lv2 <- relabelLabeledP deian l2 lv1 + return $ labelOf lv2 diff --git a/examples/waitAndCatch.hs b/examples/waitAndCatch.hs --- a/examples/waitAndCatch.hs +++ b/examples/waitAndCatch.hs @@ -11,9 +11,9 @@ l,m,h :: DCLabel -l = dcLabel ("A" \/ "B") dcTrue -m = dcLabel (toComponent "M") dcTrue -h = dcLabel ("A" /\ "B") dcTrue +l = "A" \/ "B" %% True +m = "M" %% True +h = "A" /\ "B" %% True main = do lr <- evalDC $ do diff --git a/lio.cabal b/lio.cabal --- a/lio.cabal +++ b/lio.cabal @@ -1,5 +1,5 @@ Name: lio -Version: 0.11.0.1 +Version: 0.11.2.0 Cabal-Version: >= 1.8 Build-type: Simple License: GPL @@ -55,6 +55,7 @@ Extra-source-files: examples/dclabel.hs examples/gate.hs + examples/sign.hs examples/waitAndCatch.hs