+      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~       !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Unsafe0ATA  LabeledResult= encapsulates a future result from a computation spawned by lFork or lForkP. See LIO.Concurrent; for a description of the concurrency abstractions of LIO. Thread executing the computation Label of the tresult This MVar is empty until such point as   is no longer  . Hence, calling readMVar? on this field allows one to wait for the thread to terminate. iResult (when it is ready), or the label at which the thread terminated, if that label could not flow to  .  Status of a .EIt would be a security issue to make certain objects members of the [ class. Nonetheless it is useful to be able to examine such objects when debugging. The - method can be used to examine such objects.Generic class used to get the type of labeled objects. For, instance, if you wish to associate a label with a pure value (as in  LIO.Labeled), you may create a data type: data LVal l a = LValTCB l aEThen, you may wish to allow untrusted code to read the label of any LValRs but not necessarily the actual value. To do so, simply provide an instance for LabelOf: 7instance LabelOf LVal where labelOf (LValTCB l a) = lrGet the label of a labeled value or object. Note the label must be the second to last type constructor argument. Labeled l a, is a value that associates a label of type l with a pure value of type ab. Labeled values allow users to label data with a label other than the current label. Note that  is an instance of , which means that only the contents of a labeled value (the type t<) is kept secret, not the label. Of course, if you have a Labeled within a LabeledJ, then the label on the inner value will be protected by the outer label.A newtype wrapper that can be used by trusted code to transform a powerless description of privileges into actual privileges. The constructor, p, is dangerous as it allows creation of arbitrary privileges. Hence it is only exported by the unsafe module LIO.TCB9. A safe way to create arbitrary privileges is to call privInit (see LIO.Run#v:privInit ) from the  monad before running your  computation.rAn uncatchable exception hierarchy is used to terminate an untrusted thread. Wrap the uncatchable exception in $ before throwing it to the thread. runLIO will subsequently unwrap the  constructor.!Note this can be circumvented by _, which should be made unsafe. In the interim, auditing untrusted code for this is necessary.The LIO monad is a wrapper around  that keeps track of a  current label and current clearance'. Safe code cannot execute arbitrary  actions from the 5 monad. However, trusted runtime functions can use # to perform J actions (which they should only do after appropriately checking labels).Internal state of an  computation.Current label.Current clearance. Get internal state. This function is not actually unsafe, but to avoid future security bugs we leave all direct access to the internal state to trusted code.!Set internal state.".Update the internal state given some function.# Lifts an  computation into the d monad. This function is dangerous and should only be called after appropriate checks ensure the ) computation will not violate IFC policy.$$Simple utility function that strips  from around an exception.'Trusted  instance.(  !"#$%&'()*+,-  !"#$ !"#$    !"#$%&'()*+,- Trustworthy09;<=4Generic 69 used to denote the lack of privileges. Works with any ;G type. This is only a privilege description; a more useful symbol is A, which actually embodies the NoPrivs privilege.6This class represents privilege descriptions, which define a pre-order on labels in which distinct labels become equivalent. The pre-oder implied by a privilege description is specified by the method 82. In addition, this this class defines a method 7R, which is important for finding least labels satisfying a privilege equivalence.Minimal complete definition: 7.(The 71 requirement represents the fact that a generic 8- can be implemented efficiently in terms of 7, but not vice-versa.)7qPrivileges are described in terms of a pre-order on labels in which sets of distinct labels become equivalent. downgradeP p l0 returns the lowest of all labels equivalent to l under privilege description p.Less formally, downgradeP p lK returns a label representing the furthest you can downgrade data labeled l given privileges described by p.8canFlowToP p l1 l2 determines whether p: describes sufficient privileges to observe data labeled l11 and subsequently write it to an object labeled l2. The function returns  if and only if either canFlowTo l1 l2 or  l1 and l2 are equivalent under p.The default definition is: 3canFlowToP p l1 l2 = downgradeP p l1 `canFlowTo` l2 canFlowToP is a method rather than a function so that it can be optimized in label-specific ways. However, custom definitions should behave identically to the default.9,Every privilege type must be an instance of 9i, which is a partial order specifying when one privilege value is at least as powerful as another. If 8 p1 l1 l2 and p2 : p1#, then it should also be true that 8 p2 l1 l2.As a partial order, 9 should obey the reflexivity, antisymmetry and transitivity laws. However, if you do not wish to allow delegation of a particular privilege type, you can define : _ _ = False` (which violates the reflexivity law, but is reasonable when you don't want the partial order).:speaksFor p1 p2 returns  iff p1! subsumes all the privileges of p2". In other words, it is safe for delegate to hand out p2 to a caller who already has p1. Has fixity: infix 4 `speaksFor`;QThis class defines the operations necessary to make a label into a lattice (see  ,http://en.wikipedia.org/wiki/Lattice_(order)). > partially orders labels. < and =U compute the least upper bound and greatest lower bound of two labels, respectively.< Compute the least upper boundj, or join, of two labels. When data carrying two different labels is mixed together in a document, the lubL of the two labels is the lowest safe value with which to label the result."More formally, for any two labels l1 and l2, if ljoin = l1 `lub` l2, it must be that:L_1 `>` ljoin,L_2 `>` ljoin, andThere is no label  l /= ljoin such that l1 `>` l, l2 `>` l, and l `>` ljoin. In other words ljoin$ is the least element to which both l1 and l2 can flow.When used infix, has fixity: infixl 5 `lub`=Greatest lower bound., or meet, of two labels. For any two labels l1 and l2, if lmeet = l1 `glb` l2, it must be that:lmeet `>` l1,lmeet `>` l2, andThere is no label  l /= lmeet such that l `>` l1, l `>` l2, and lmeet `>` l. In other words lmeet) is the greatest element flowing to both l1 and l2.When used infix, has fixity: infixl 5 `glb`> Can-flow-to! relation ("). An entity labeled l1( should be allowed to affect an entity l2 only if l1 `canFlowTo` l2<. This relation on labels is at least a partial order (see  3https://en.wikipedia.org/wiki/Partially_ordered_set(), and must satisfy the following laws: Reflexivity: l1 `canFlowTo` l1 for any l1.Antisymmetry: If l1 `canFlowTo` l2 and l2 `canFlowTo` l1 then l1 = l2.Transitivity: If l1 `canFlowTo` l2 and l2 `canFlowTo` l3 then l1 `canFlowTo` l3.When used infix, has fixity: infix 4 `canFlowTo`?STurns privileges into a powerless description of the privileges by unwrapping the  newtype.@Uses dynamic typing to return " iff the type of the argument is  a (for any a?). Mostly useful to prevent users from accidentally wrapping  objects inside other D objects or accidentally including real privileges in an exception.A object corresponding to 4.C7 4# is the identify function. Hence 8 4 is the same as >.456789:;<=>?@ABCDEF456789:;<=>?@A;<=>9:678?@45A 456789:;<=>?@ABCDEF:4<5=5>4 Trustworthy9;<=?ISynonym for monad in which  is the base monad.JLift an  computation.IJKIJIJIJK TrustworthyL Execute an u action, returning its result and the final label state as a pair. Note that it returns a pair whether or not the ~ action throws an exception. Forcing the result value will re-throw the exception, but the label state will always be valid. See also N.M A variant of L that returns results in  and exceptions in !, much like the standard library  function.N Given an { computation and some initial state, return an IO action which, when executed, will perform the IFC-safe LIO computation.&Because untrusted code cannot execute m computations, this function should only be useful within trusted code. No harm is done from exposing the evalLIOL symbol to untrusted code. (In general, untrusted code is free to produce , computations, but it cannot execute them.)Unlike L7, this function throws an exception if the underlying % action terminates with an exception.O'Initialize some privileges (within the  monad) that can be passed to  computations run with L or N?. This is a pure function, but the result is encapsulated in - to make the return value inaccessible from  computations./Note the same effect can be achieved using the  constructor, but 9 is easier to misuse and is only available by importing LIO.TCB.LMNOLMNOLMNOLMNO Trustworthy0ATPThrow an exception.QA simple wrapper around IO catch. The only subtlety is that code is not allowed to run unless the current label can flow to the current clearance. Hence, if the label exceeds the clearance, the exception is not caught. (Only a few conditions such as lWait" or raising the clearance within scopeClearancem can lead to the label exceeding the clarance, and an exception is always thrown at the time this happens.)R A version of Q# with the arguments swapped around.SLike T[, but only performs the final action if there was an exception raised by the computation. T A variant of UE where the return value from the first computation is not required. UtWhen you want to acquire a resource, do some work with it, and then release the resource, it is a good idea to use bracket, because bracket will install the necessary exception handler to release the resource in the event that an exception is raised during the computation. If an exception is raised, then bracket will re-raise the exception (after performing the release). VQForces its argument to be evaluated to weak head normal form when the resultant  action is executed.W!Similar to catch, but returns an  result which is ( a) if no exception of type e was raised, or ( ex) if an exception of type e was raised and its value is exs. If any other type of exception is raised than it will be propogated up to the next enclosing exception handler.PQRSTUComputation to run firstComputation to run lastComputation to run in-betweenVWPQRSTUVWPQRWSTUVPQRSTUVW Trustworthy0ATX+Error raised when a computation spawned by lForkB terminates with its current label above the label of the result.^kError indicating insufficient privileges (independent of the current label). This exception is thrown by delegate], and should also be thrown by gates that receive insufficient privilege descriptions (see  LIO.Delegate).d0Main error type thrown by label failures in the  monad.f)Annotation of where the failure happened.gActual function that failed.hCurrent label at time of error.i#Current clearance at time of error.j!Any privileges involved in error.kAny labels involved in error.lQA generic privilege description for recording relevant privileges in exceptions.n'Parent of all label-related exceptions.p;Class of error messages that can be annotated with context.r]Executes an action with a context string, which will be added to any label exception thrown.+Note: this function wraps an action with a Qh, and thus may incur a small runtime cost (though it is well under 100 ns on machines we benchmarked).sDefinition of  for children of n in the exception hierarchy.tDefinition of  for children of n in the exception hierarchy.uThrow a label-error exception.vThrow a label-error exception.wRaise ^ error.+XYZ[\]^_`abcdefghijklmnopqrstuFunction that failed.Labels involved in error.vFunction that failed.Privileges involved.Labels involved.wFunction in which error occurs"Description of privileges supplied Description of privileges neededxyz{|}~ XYZ[\]^_`abcdefghijklmnopqrstuvw pqrnostlmdefghijkuv^_`abcwXYZ[\]XYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Safe0ATSee .See .Function that failed.Labels involved in error.Function that failed.Privileges involved.Labels involved. Trustworthy0RA Gate is a lambda abstraction from a privilege description to an arbitrary type a). Applying the gate is accomplished with l which takes a privilege argument that is converted to a description before invoking the gate computation.delegate allows you to create a new privilege object that is less powerful than an existing privilege object. The first argument supplies actual privileges. The second argument is a 6l describing the desired new privileges. The call throws an exception unless the privilege object supplied :! the privilege object requested.9Note: If you are looking for a way to create privileges more7 powerful than ones you already have, you can use the * function to combine existing privileges.dCreate a gate given a computation from a privilege description. Note that because of currying type al may itself be a function type and thus gates can take arguments in addition to the privilege descriptoin.guardGate name minPriv aE creates a simple gate that requires privileges at least as high as minPriv$ to return the payload or function aF. If the privileges supplied are insufficient, an exception of type ^ is thrown. The argument namef is used only when an exception is thrown, to make the source of the exception more easily traceable. tguardGate name minPriv a = gate $ \pd -> if pd `speaksFor` minPriv then a else insufficientPrivs name pd minPrivYGiven a gate and privilege, execute the gate computation. It is important to note that callGateB invokes the gate computation with the privilege description and NOT the privilege itself.#Note that, in general, code should not- provide privileges to functions other than callGate( when wishing to call a gate. This function is provided by LIO since it can be easily inspected by both the gate creator and caller to be doing the "right" thing: provide the privilege description corresponding to the supplied privilege as "proof" without explicitly passing in the privilege.Gate computationGate$Privilege used as proof-of-ownership  Trustworthy9;<=?0Returns the value of the thread's current label.lRaises the current label to the provided label, which must be between the current label and clearance. See .If the current label is oldLabel and the current clearance is  clearanceE, this function allows code to raise the current label to any value newLabel such that 8 priv oldLabel newLabel && > newLabel clearanceY. (Note the privilege argument affects the label check, not the clearance check; call  first to raise the clearance.)'Returns the thread's current clearance.Lowers the current clearance. The new clerance must be between the current label and previous current clerance. One cannot raise the current label or create object with labels higher than the current clearance.6Raises the current clearance (undoing the effects of 6) by exercising privileges. If the current label is l and current clearance is c, then setClearanceP p cnewf succeeds only if the new clearance is can flow to the current clearance (modulo privileges), i.e., 8 p cnew c == TrueJ. Additionally, the current label must flow to the new clearance, i.e., l `>` cnew == True.ASince LIO guards that are used when reading/writing data (e.g., ) do not use privileges when comparing labels with the current clearance, code must always raise the current clearance, to read/write data above the current clearance.Runs an  action and re-sets the current clearance to its previous value once the action returns. In particular, if the action lowers the current clearance, the clearance will be restored upon return. Note that scopeClearancec always restores the clearance. If that causes the clearance to drop below the current label, a ClearanceViolationK exception is thrown. That exception can only be caught outside a second scopeClearance? that restores the clearance to higher than the current label.VTemporarily lowers the clearance for a computation, then restores it. Equivalent to: withClearance c lio =  $  c >> lio $Note that if the computation inside  withClearance acquires any Rs, it may still be able to raise its clearance above the supplied argument using . A variant of ( that takes privileges. Equivalent to: withClearanceP p c lio =  $  p c >> lio 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  guardAlloc lf does not throw an exception. Similarly use this guard in any code that writes to an object labeled l5 for which the write has no observable side-effects.Like O, but takes a privilege argument to be more permissive. Note: privileges are onlyJ used when checking that 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.Use taint l5 in trusted code before observing an object labeled l0. This will raise the current label to a value l' such that l `>` l' , or throw a d exception if l'5 would have to be higher than the current clearance.Like I, but use privileges to reduce the amount of taint required. Note that taintPg will never lower the current label. It simply uses privileges to avoid raising the label as high as  would raise it.Use  guardWrite l; in any (trusted) code before modifying an object labeled lN, for which the modification can be observed, i.e., the write implies a read.The implementation of  guardWrite is straight forward: &guardWrite l = guardAlloc l >> taint lThe 9 ensures that we can write(-only) to the object labeled l, i.e., the current label `>` l (and l `>W` the current clearance). If this check succeeds then we raise the current label with j to reflect the fact that this is a also a read effect. Note that if the write-only guard succeeds, the e will always suceed (we're simply raising the current label to a label that is below the clearance).Like 8, but takes a privilege argument to be more permissive.(IJLN^_`abcdefghijkno(IJNLnodefghijk^_`abc Safe9;<=? See  .See  .See  .See  .See  .See  .See  !.See  ".See  #.See  $.See  %.See  &.  Trustworthy Function to construct a @ 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 `> ` l && l `> ` ccurrent). Otherwise an exception is thrown (see ). Constructs a l 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 `> ` ccurrentK. Note that privilege is not used to bypass the clearance. You must use 7 to raise the clearance first if you wish to create a 5 value at a higher label than the current clearance. Within the  monad, this function takes a Y value and returns it as an unprotected value of the inner type. For instance, in the  monad one can say: .x <- unlabel (lx :: Labeled SomeLabelType Int)-And now it is possible to use the pure value x :: Int0, which was previously protected by a label in lx.unlabelv raises the current label as needed to reflect the fact that the thread's behavior can now depend on the contents of lx. If unlabelWing a value would require raising the current label above the current clearance, then unlabel throws an exception of type d. You can use  to check beforehand whether  will succeed.Extracts the contents of a  value just like , 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 dv if the privileges supplied are insufficient to save the current label from needing to exceed the current clearance. Relabels a  value to the supplied label if the given privileges permit it. An exception is thrown unless the following two conditions hold: 2The new label must be below the current clearance.QThe old label and new label must be equal (modulo privileges), as enforced by 8.Raises the label of a  value to the < 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 l 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 ).Same as , but uses privileges when comparing the current label to the supplied label. In other words, this function can be used to lower the label of the labeled value by leveraging the supplied privileges.A function similar to  for # values. Applies a function to a  value without Xing the value or changing the thread's current label. The label of the result is the </ of the current label and that of the supplied L value. Because of laziness, the actual computation on the value of type a? will be deferred until a thread with a higher label actually  s the result. Similar to , apply function (wrapped by ?) to the labeld value. The label of the returned value is the <j of the thread's current label, the label of the supplied function, and the label of the supplied value.   Safe09;<= An alias for  values labeled with a . privileges are expressed as a 7 of the principals whose authority is being exercised.%The main monad type alias to use for $ computations that are specific to s. As a type, a  is always a conjunction of s of 0s. However, mathematically speaking, a single  or single B is also a degenerate example of conjunctive normal form. Class L abstracts over the differences between these types, promoting them all to .Main DCLabel type. DCLabels use f boolean formulas over principals to express authority exercised by a combination of principals. A DCLabel contains two  s. One, i, specifies the minimum authority required to make data with the label completely public. The second, , expresses the minimum authority that was used to endorse data with the label, or, for mutable objects, the minimum authority required to modify the object.DCLabel,s are more conveniently expressed using the  operator, with  on the left and  on the right, i.e.: (dcSecrecyValue  dcIntegrityValue).DCLabel"s enforce the following relations:If cnf1 and cnf2 are  s describing authority, then cnf1 `:` cnf2 if and only if cnf1 logically implies cnf2 (often written  cnf1 ' cnf2). For example, ("A"  "B") `:`  "A", while  "A" `:` ("A"  "C"). Given two DCLabels  dc1 = (s1  i1) and  dc2 = (s2  i2), dc1 `>` dc2 (often written dc1 " dc2) if and only if s2 `: ` s1 && i1 `:` i2. In other words, data can flow in the direction of requiring more authority to make it public or removing integrity endorsements. Given two DCLabels  dc1 = (s1  i1) and  dc2 = (s2  i2), and a p:: representing privileges, 8 p dc1 dc2 (often written dc1 " dc2) if and only if (p  s2) `: ` s2 && (p  i1) `:` i2.:Describes the authority required to make the data public.sDescribes the authority with which immutable data was endorsed, or the authority required to modify mutable data./A boolean formula in Conjunctive Normal Form. CNF is used to describe = privileges, as well to provide each of the two halves of a .Represents a disjunction of s, or one clause of a ;. There is generally not much need to work directly with  DisjunctionCs unless you need to serialize and de-serialize them (by means of  and ).A  Principal is a primitive source of authority, represented as a string. The interpretation of principal strings is up to the application. Reasonable schemes include encoding user names, domain names, and/or URLs in the  type.,Extract the name of a principal as a strict . (Use  to get it as a regular .)!Create a principal from a strict .Create a principal from a . The  is packed into a  using Y, which will almost certainly give unexpected results for non-ASCII unicode code points.Expose the set of s being ORed together in a .Convert a list of  s into a .Returns 5 iff the first disjunction is a subset of the second. Convert a  to a  of .s. Mostly useful if you wish to serialize a .A  that is always True&--i.e., trivially satisfiable. When  = cTrue", it means data is public. When  = cTrueS, it means data carries no integrity guarantees. As a description of privileges, cTrue conveys no privileges; 8 cTrue l1 l2 is equivalent to > l1 l2. Note that   = cTrue . Hence  =  cTrue cTrue.A  that is always False. If  = cFalsed, then no combination of principals is powerful enough to make the data public. For that reason, cFalse\ generally shouldn't appear in a data label. However, it is convenient to include as the  component of 7 to indicate a thread may arbitrarily raise its label. = cFalse indicates impossibly much integrity--i.e., data that no combination of principals is powerful enough to modify or have created. Generally this is not a useful concept.As a privilege description, cFalseh indicates impossibly high privileges (i.e., higher than could be achieved through any combination of s). cFalse `:` p for any  pI. This can be a useful concept for bootstrapping privileges within the - monad itself. For instance, the result of O cFalse can be passed to fully-trusted  code, which can in turn use delegateH to create arbitrary finite privileges to pass to less privileged code.Convert a list of  s into a 0. Mostly useful if you wish to de-serialize a . dcPublic = True %% TrueThis 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 such that (s %% i) " dcPublic, while i+ is the exact minimum authority such that dcPublic "b (s %% i).The primary way of creating a c. The secrecy component goes on the left, while the integrity component goes on the right, e.g.: "label = secrecyCNF %% integrityCNF Unlike the 4 constructor, the arguments can be any instance of . %% has fixity:  infix 6 %%Compute a conjunction of two s or  instances. Has fixity:  infixr 7 /\Compute a disjunction of two s or a instances. Note that this can be an expensive operation if the inputs have many conjunctions.*The fixity is specifically chosen so that \/ and = cannot be mixed in the same expression without parentheses:  infixl 7 \/'A common default starting state, where  =  and  = False  True) (i.e., the highest possible clearance).Wrapper function for running   computations.  evalDC dc = N dc   wrapper for M:  tryDC dc = M dc  9Note that a disjunction containing more than one element must2 be surrounded by parentheses to parse correctly.C<677  Trustworthy See  '.See  (.See  ).See  *.See  +.See  ,.See  -.See  ..See  /. Unsafe09;<=?Class for lifting  actions. Lifts an  action in the 7 monad, executing a guard before calling the function.A "LObj label object1" 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 7 monad when the caller can 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 associated with a single label, and that the abstraction combined with its blessed IO operations (see G) cannot be used to communicate with code running at different labels.%This function can be used to turn an  function into an  one. The  version expects a . argument, and before performing any IO uses = to check that the current label can write the label in the  object.JThe first argument should be the name of the function being defined with blessTCB-. Its purpose is to enhance error reporting. Note that io and liow are function types (of up to nine arguments), which must be the same in all types except the monad. For example, if io is Int -> String -> IO (), then lio must be Int -> String -> LIO l (). A variant of  that produces an ' function taking a privilege argument. Similar to X, but enforces the weaker restriction that the action is write-only. When in doubt use . Similar to W, but enforces the weaker restriction that the action is read-only. When in doubt use .  Trustworthy*: An LIORef is an IORef with an associated, fixed label. The 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.Create a new reference with a particularlabel. The label specified must be between the thread's current label and clearance, as enforced by . Same as  except  newLIORefPc takes privileges which make the comparison to the current label more permissive, as enforced by . 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 <W of the current label and the reference label. To avoid failures (introduced by the  guard) use labelOf$ to check that a read will succeed. Same as   , except  readLIORefPR takes a privilege object which is used when the current label is raised (using  instead of ). Write a new value into a labeled reference. A write succeeds if the current label can-flow-to the label of the reference, and the label of the reference can-flow-to the current clearance. Otherwise, an exception is raised by the underlying  guard. Same as   except  writeLIORefPr takes a set of privileges which are accounted for in comparing the label of the reference to the current label.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 . The caller of  modifyLIORef8 learns no information about the previous contents the G. For that reason, there is no need to raise the current label. The Z's label must still lie between the current label and clearance, however (as enforced by ).Like <, but takes a privilege argument and guards execution with  instead of .'Atomically modifies the contents of an /. It is required that the label of the reference be above the current label, but below the current clearance. Moreover, since this function can be used to directly read the value of the stored reference, the computation is "tainted" by the reference label (i.e., the current label is raised to the joinQ of the current and reference labels). These checks and label raise are done by , which will raise a d= exception if any of the IFC conditions cannot be satisfied.Same as  except atomicModifyLIORefP% takes a set of privileges and uses  instead of . Label of reference Initial valueMutable reference     Labeled referenceModifier                  Safe*: See 0.See 1.See 2.See 3.See 4.See 5.See 6.See 7.See 8.See 9. Label of reference Initial valueMutable referenceLabeled referenceModifier   Unsafe 09;<=?OTTakes a liftIO-like function and an IOZ function of an arbitrary number of arguments (up to 10). Applies the arguments to the IOT function, then passed the result to its argument funciton to transform it into an LIO function.3IO Object with a mutable label. By contrast with :, the label on an 6 can change over time. If this happens, the internal "N ensures that threads accessing the object receive an asynchronous exception. %Class of objects with mutable labels."A mutable label. Consists of a static label on the label, a mutable label, and a list of threads currently accessing the label. This is intended to be used by privileged code implementing IOE abstractions with mutable labels. Routines for accessing such an IO abstraction should perform tne IO from within a call to 2J, to ensure an exception is raised if another thread revokes access with 3.(( is for objects that communicate to the outside world, where extra privileges are required since once data gets out, so as to vouch for the fact that the other end of a socket won't arbitrarily downgrade data.**t is for objects contained entirely within Haskell, such as a variable. Raising the label can't cause data to leak., Class for .:s that don't encode any interesting values. This allows 6 to create an & without requiring a policy argument..;Class of policies for when it is permissible to update an ".0SReturns the immutable label that controls access to the mutable label value of an ".1yRetreive a snapshot of the value of a mutable label. Of course, it may already have changed by the time you process it.2Run an action that should be protected by a mutable label. An exception is thrown if the invoking thread cannot write to the mutable label given the privileges. No attempt is made to adjust the current label, even if doing so would make the permissions acceptable.Note that if the label changes after this function has been invoked, an exception may be raised in the middle of the protected action.3Change the mutable label in an "D. Raises asynchronous exceptions in other threads that are inside 2( if the new label revokes their access.newMLabelP policy ll l creates an ". policyX is a policy specifying under what conditions it is permissible to change the label. ll/ is the immutable label of the mutable label. l- is the initial value of this mutable label.4 Create an ", performing access control checks to ensure that the labels are within the range allowed given the current label and clearance, and the supplied privileges.5Like 6, but create an L with a particular policy value. Note that you don't need to use this for ( and *, as these don't have anything interesting in the policy value, only the type matters. This might be useful if, for instance, you wished to design a new policy type that embeds a clearance.66 ll l a creates an  wrapping some IO object a. Here llN is the label on the label, which remains immutable over the lifetime of the . l, is the initial value of the mutable lable.7 Modify the " within an .8The  equivalent of blessTCB in LIO.TCB.LObj#v:blessTCB(. Use this for conveniently providing LIO versions of standard IO functions.9The  equivalent of  blessPTCB in LIO.TCB.LObj#v:blessPTCB(. Use this for conveniently providing LIO versions of standard IO functions./ !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHI !"#$%&'()*+,-./012345678965789"#$%&'40123 !,-./*+()# !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHI Trustworthy*:LAn LMVar+ is a labeled synchronization variable (an 9) that can be used by concurrent threads to communicate.MCreate a new labeled MVar, in an empty state. Note that the supplied label must be above the current label and below the current clearance. An exception will be thrown by the underlying  if this is not the case.NSame as M except it takes a set of privileges which are accounted for in comparing the label of the MVar to the current label and clearance.OCreate a new labeled MVar, in an filled state with the supplied value. Note that the supplied label must be above the current label and below the current clearance.PSame as Ov except it takes a set of privileges which are accounted for in comparing the label of the MVar to the current label.QReturn contents of the LY. Note that a take consists of a read and a write, since it observes whether or not the LF is full, and thus the current label must be the same as that of the LX (of course, this is not the case when using privileges). Hence, if the label of the L is below the current clearance, we raise the current label to the join of the current label and the label of the MVar and read the contents of the MVar. The underlying guard G will throw an exception if any of the IFC checks fail. Finally, like MVars if the L is empty,  takeLMVar blocks.RSame as Q except  takeLMVarPJ takes a privilege object which is used when the current label is raised.SNon-blocking version of Q . It returns Nothing if the L is empty, otherwise it returns Just value, emptying the L.TSame as S2, but uses priviliges when raising current label.UPuts a value into an LX. Note that a put consists of a read and a write, since it observes whether or not the LE is empty, and so the current label must be the same as that of the LE (of course, this is not the case when using privileges). As in the Q case, if the label of the L is below the current clearance, we raise the current label to the join of the current label and the label of the MVar and put the value into the MVar<. Moreover if these IFC restrictions fail, the underlying  throws an exception. If the L is full, putLMVar blocks.VSame as U except  putLMVarPJ takes a privilege object which is used when the current label is raised.WNon-blocking version of U . It returns True if the L7 was empty and the put succeeded, otherwise it returns False.XSame as W1, but uses privileges when raising current label.YCombination of Q and U. Read the value, and just put it back. This operation is not atomic, and can can result in unexpected outcomes if another thread is simultaneously calling a function such as U, T, or ] for this L.ZSame as Y except  readLMVarPJ takes a privilege object which is used when the current label is raised.[Takes a value from an L, puts a new value into the LMvar0, and returns the taken value. Like the other L2 operations it is required that the label of the L be above the current label and below the current clearance. Moreover, the current label is raised to accommodate for the observation. The underlying u throws an exception if this cannot be accomplished. This operation is atomic iff there is no other thread calling U for this L.\Same as [ except  swapLMVarPJ takes a privilege object which is used when the current label is raised.]Check the status of an LH, i.e., whether it is empty. The function succeeds if the label of the LS is below the current clearance -- the current label is raised to the join of the L label and the current label.^Same as ]1, but uses privileges when raising current label.LM Label of LMVarNew mutable locationNO Label of LMVarInitial value of LMVarNew mutable locationPQRSTUSource L New valueVWXYZ[Source LMVar New value Taken value\]^LMNOPQRSTUVWXYZ[\]^LMNOPQRSTUVWXYZ[\]^LMNOPQRSTUVWXYZ[\]^Safe_See ;.`See <.aSee =.bSee >.cSee ?.dSee @.eSee A.fSee B.gSee C.hSee D.iSee E.jSee F.kSee G.lSee H.mSee I.nSee J.oSee K.pSee L._`abcdefghijklmnop_`abcdefghijklmnop_`abcdefghijklmnop_`abcdefghijklmnop Trustworthy qA LChan7 is a labeled channel, i.e., an unbounded FIFO channel.rCreate a new labeled channel. Note that the supplied label must be above the current label and below the current clearance. An exception will be thrown by the underlying  if this is not the case.sSame as rv except it takes a set of privileges which are accounted for in comparing the label of the Chan to the current label.tqWrite value to the labeled channel. The label of the channel must be bounded by the current label and clearance.uSame as tT, but uses privileges when comparing the current label to the label of the channel.vRead the next value from the channel. The current label is raised to join of the channel label and current label. Howerver, the label of the channel must be below the current clearance.wSame as vq, but takes a privilege object which is used when the current label is raised to avoid over-taining the context.xhDuplicate labeled channel. The label of the channel must be bounded by the current label and clearance.ySame as xT, but uses privileges when comparing the current label to the label of the channel. qrstuvwxy qrstuvwxy qrsvwtuxy qrstuvwxySafezSee M.{See N.|See O.}See P.~See Q.See R.See S.See T.z{|}~z{|}~z{|}~z{|}~ Trustworthy  Execute an ) computation in a new lightweight thread.Labeled fork. lFork\ allows one to invoke computations that would otherwise raise the current label, but without actually raising the label. The computation is executed in a separate thread and writes its result into a labeled result (whose label is supplied). To observe the result of the computation, or if the computation has terminated, one will have to call \ and raise the current label. Of couse, this can be postponed until the result is needed.lFork takes a label, which corresponds to the label of the result. It is required that this label be between the current label and clearance as enforced by a call to . Moreover, the supplied computation must not terminate with its label above the result label; doing so will result in an exception being thrown in the thread reading the result. Note that lFork immediately returns a , which is essentially a "future", or "promise". This prevents timing/termination attacks in which the duration of the forked computation affects the duration of the lFork.To guarantee that the computation has completed, it is important that some thread actually touch the future, i.e., perform an .Same as Z, but the supplied set of priviliges are accounted for when performing label comparisons.Given a  (a future), lWait; returns the unwrapped result (blocks, if necessary). For lWait to succeed, the label of the result must be above the current label and below the current clearance. Moreover, before block-reading, lWait| raises the current label to the join of the current label and label of result. An exception is thrown by the underlying  if this is not the case. Additionally, if the thread terminates with an exception (for example if it violates clearance), the exception is rethrown by lWaito. Similarly, if the thread reads values above the result label, an exception is thrown in place of the result.Same as 1, but uses priviliges in label checks and raises.Same as (, but does not block waiting for result.Same as 1, but uses priviliges in label checks and raises.Like , with two differences. First, a timeout is specified and the thread is unconditionally killed after this timeout (if it has not yet returned a value). Second, if the thread's result exceeds what the calling thread can observe,  timedlWait* consumes the whole timeout and throws a XP exception you can catch (i.e., it never raises the label above the clearance).^Because this function can alter the result by killing a thread, it requires the label of the 8 to be both readable and writable at the current label. A version of x that takes privileges. The privileges are used both to downgrade the result (if necessary), and to try catching any X* before the timeout period (if possible). Label of result)Computation to execute in separate threadLabeled result#XYZ[\]LMNOPQRSTUVWXYZ[\]^XYZ[\] USafeU456789:;<=>?AIJLNPQRSTUVW^_`abcdefghijknoVWXVWYVWZVW[VW\VWX]^_`abcdefghijklmnooUpqqrstuvwxyz{|}~      ! " # $ % &      ! " # $ % & ' ( ) * + , - . /                         ' ( ) * + , - . /: !"#$%01234567890123456789&'()*+,-./012233456789:;<=>?@ABCDEFGHIJKLMNOPQRST;<=>?@ABCDEFGHIJKL;<=>?@ABCDEFGHIJKLUMNOPQRSTMNOPQRSTVWXYZ[\]^V_`ababcVdeVdfVgVdhVijkVilVimnopV_qVirVst uvwx    y z { | } ~       V#lio-0.11.6.0-KbdXFtsenByKKE1ChirBF9 LIO.ExceptionLIO.TCB LIO.Label LIO.MonadLIO.Run LIO.ErrorLIO.Error.Trans LIO.DelegateLIO.CoreLIO.Core.Trans LIO.Labeled LIO.DCLabelLIO.Labeled.Trans LIO.TCB.LObj LIO.LIORefLIO.LIORef.Trans LIO.TCB.MLObjLIO.Concurrent.LMVarLIO.Concurrent.LMVar.TransLIO.Concurrent.LChanLIO.Concurrent.LChan.TransLIO.ConcurrentIO mapException labelError labelErrorPgetLabelsetLabel setLabelP getClearance setClearance setClearanceP guardAlloc guardAllocPtainttaintP guardWrite guardWritePlabellabelPunlabelunlabelPrelabelLabeledP taintLabeled taintLabeledPlFmaplAp newLIORef newLIORefP readLIORef readLIORefP writeLIORef writeLIORefP modifyLIORef modifyLIORefPatomicModifyLIORefatomicModifyLIORefPLObj newEmptyLMVarnewEmptyLMVarPnewLMVar newLMVarP takeLMVar takeLMVarP tryTakeLMVar tryTakeLMVarPputLMVar putLMVarP tryPutLMVar tryPutLMVarP readLMVar readLMVarP swapLMVar swapLMVarP isEmptyLMVar isEmptyLMVarPnewLChan newLChanP writeLChan writeLChanP readLChan readLChanPdupLChan dupLChanPLIObase GHC.Exception SomeExceptiondisplayException fromException toException Exception LabeledResultLabeledResultTCBlresThreadIdTCB lresLabelTCB lresBlockTCB lresStatusTCB LResStatus LResEmptyLResLabelTooHigh LResResultShowTCBshowTCBLabelOflabelOfLabeled LabeledTCBPrivPrivTCBUncatchableTCBLIOTCBLIOStatelioLabel lioClearancegetLIOStateTCBputLIOStateTCBmodifyLIOStateTCBioTCB makeCatchable$fLabelOfLabeledResult$fLabelOfLabeled$fShowTCBLabeled $fMonoidPriv$fExceptionUncatchableTCB$fShowUncatchableTCB$fApplicativeLIO $fFunctorLIO $fMonadLIO $fEqLIOState$fShowLIOState$fReadLIOState $fShowPriv$fEqPriv$fShowLResStatusNoPrivsPrivDesc downgradeP canFlowToP SpeaksFor speaksForLabellubglb canFlowToprivDescisPrivnoPrivs$fMonoidNoPrivs$fPrivDesclNoPrivs$fSpeaksForNoPrivs$fPrivDesclPriv$fSpeaksForPriv $fShowNoPrivs $fReadNoPrivsMonadLIOliftLIO$fMonadLIOlLIOrunLIOtryLIOevalLIOprivInitthrowLIOcatchhandle onExceptionfinallybracketevaluatetryResultExceedsLabel relContext relLocationrelDeclaredLabelrelActualLabelInsufficientPrivs inspContext inspFailure inspSupplied inspNeeded LabelError lerrContext lerrFailure lerrCurLabellerrCurClearance lerrPrivs lerrLabelsGenericPrivDesc AnyLabelError Annotatableannotate withContextlerrToExceptionlerrFromExceptioninsufficientPrivs$fExceptionResultExceedsLabel$fAnnotatableResultExceedsLabel$fExceptionInsufficientPrivs$fAnnotatableInsufficientPrivs$fShowInsufficientPrivs$fExceptionLabelError$fAnnotatableLabelError$fShowGenericPrivDesc$fExceptionAnyLabelError$fAnnotatableAnyLabelError$fShowAnyLabelError$fShowLabelError$fShowResultExceedsLabelGatedelegategate guardGatecallGatescopeClearance withClearancewithClearanceP DCLabeledDCPrivDCToCNFtoCNFDCLabel dcSecrecy dcIntegrityCNF Disjunction Principal principalName principalBS principaldToSet dFromListcToSetcTruecFalse cFromListdcPublic%%/\\/dcDefaultStateevalDCtryDC$fPrivDescDCLabelCNF$fSpeaksForCNF$fLabelDCLabel $fToCNFBool $fToCNF[]$fToCNFPrincipal$fToCNFDisjunction $fToCNFPriv $fToCNFCNF $fReadDCLabel $fShowDCLabel $fMonoidCNF $fReadCNF $fShowCNF$fMonoidDisjunction$fReadDisjunction$fShowDisjunction$fOrdDisjunction$fEqDisjunction $fEqPrincipal$fReadPrincipal$fShowPrincipal$fOrdPrincipal$fEqCNF$fOrdCNF $fEqDCLabel $fOrdDCLabelGuardIO guardIOTCBLObjTCBblessTCB blessPTCBblessWriteOnlyTCBblessWriteOnlyPTCBblessReadOnlyTCBblessReadOnlyPTCB$fGuardIOl(->)(->)$fGuardIOl(->)(->)0$fGuardIOl(->)(->)1$fGuardIOl(->)(->)2$fGuardIOl(->)(->)3$fGuardIOl(->)(->)4$fGuardIOl(->)(->)5$fGuardIOl(->)(->)6$fGuardIOl(->)(->)7$fGuardIOl(->)(->)8$fGuardIOlIOLIO $fShowTCBLObj $fLabelOfLObjLIORefLabelIOlabelIOMLObjMLObjTCBMLabelOfmLabelOfMLabel MLabelTCB mlLabelLabelmlLabelmlUsersmlPolicy ExternalML InternalMLMLabelPolicyDefaultmlabelPolicyDefault MLabelPolicy mlabelPolicy labelOfMlabel readMLabelP withMLabelP modifyMLabelP newMLabelPmlPolicyObjTCBmlObjTCBmodifyMLObjLabelP mblessTCB mblessPTCB$fLabelIOl(->)(->)$fLabelIOl(->)(->)0$fLabelIOl(->)(->)1$fLabelIOl(->)(->)2$fLabelIOl(->)(->)3$fLabelIOl(->)(->)4$fLabelIOl(->)(->)5$fLabelIOl(->)(->)6$fLabelIOl(->)(->)7$fLabelIOl(->)(->)8$fLabelIOlIOLIO$fMLabelOfMLObj$fMLabelPolicyDefaultExternalML$fMLabelPolicyExternalMLl$fMLabelPolicyDefaultInternalML$fMLabelPolicyInternalMLl$fShowInternalML$fShowExternalMLLMVarLChanforkLIOlForklForkPlWaitlWaitPtrylWait trylWaitP timedlWait timedlWaitPGHC.ShowShowghc-prim GHC.TypesTrue Data.EitherRightLeftControl.Exception.BaseEitherGHC.BasemappendGateTCBfmapapbytestring-0.10.8.1Data.ByteString.Internal ByteStringshowString Data.String fromStringdImpliescontainers-0.5.7.1 Data.Set.BaseSetSetTagdFalse dSingletondUnion cSingletonsetAnysetAllcInsertcUnioncOr cImplies1cImpliesdcMaxDowngrade newMLabelTCBGHC.MVarMVar