lio 0.11.0.1 → 0.11.2.0
raw patch · 17 files changed
+251/−164 lines, 17 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
+ LIO.Delegate: guardGate :: SpeaksFor p => String -> p -> a -> Gate p a
+ LIO.Label: isPriv :: Typeable p => p -> Bool
- LIO.Error: insufficientPrivs :: SpeaksFor p => String -> Priv p -> p -> a
+ LIO.Error: insufficientPrivs :: SpeaksFor p => String -> p -> p -> a
Files
- LIO.hs +1/−1
- LIO/Concurrent/LMVar.hs +7/−7
- LIO/Core.hs +4/−2
- LIO/DCLabel.hs +26/−11
- LIO/Delegate.hs +30/−9
- LIO/Error.hs +10/−5
- LIO/LIORef.hs +35/−35
- LIO/Label.hs +26/−9
- LIO/Labeled.hs +62/−49
- LIO/Run.hs +0/−8
- LIO/TCB.hs +6/−3
- LIO/TCB/LObj.hs +9/−5
- examples/dclabel.hs +10/−11
- examples/gate.hs +6/−5
- examples/sign.hs +14/−0
- examples/waitAndCatch.hs +3/−3
- lio.cabal +2/−1
LIO.hs view
@@ -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
LIO/Concurrent/LMVar.hs view
@@ -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
LIO/Core.hs view
@@ -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
LIO/DCLabel.hs view
@@ -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"+<interactive>: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
LIO/Delegate.hs view
@@ -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
LIO/Error.hs view
@@ -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.
LIO/LIORef.hs view
@@ -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
LIO/Label.hs view
@@ -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
LIO/Labeled.hs view
@@ -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
LIO/Run.hs view
@@ -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
LIO/TCB.hs view
@@ -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'.
LIO/TCB/LObj.hs view
@@ -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 #-}
examples/dclabel.hs view
@@ -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 -}
examples/gate.hs view
@@ -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
+ examples/sign.hs view
@@ -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
examples/waitAndCatch.hs view
@@ -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
lio.cabal view
@@ -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