!      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~       !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Unsafe2EXJ[lioA  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.lio Thread executing the computation lioLabel of the tresult lioThis 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. lioiResult (when it is ready), or the label at which the thread terminated, if that label could not flow to  . lio Status of a .lioEIt 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.lioGeneric 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) = lliorGet the label of a labeled value or object. Note the label must be the second to last type constructor argument.lio 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.lioA 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.liorAn 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.lioThe 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).lioInternal state of an  computation.lioCurrent label.lioCurrent clearance. lioGet 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.!lioSet internal state."lio.Update the internal state given some function.#lio 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.$lio$Simple utility function that strips  from around an exception.-lioTrusted  instance.  !"#$ !"#$  Trustworthy2=?@AI5lioGeneric 79 used to denote the lack of privileges. Works with any <G type. This is only a privilege description; a more useful symbol is B, which actually embodies the NoPrivs privilege.7lioThis 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 92. In addition, this this class defines a method 8R, which is important for finding least labels satisfying a privilege equivalence.Minimal complete definition: 8.(The 81 requirement represents the fact that a generic 9- can be implemented efficiently in terms of 8, but not vice-versa.)8lioqPrivileges 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.9liocanFlowToP 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.:lio,Every privilege type must be an instance of :i, which is a partial order specifying when one privilege value is at least as powerful as another. If 9 p1 l1 l2 and p2 ; p1#, then it should also be true that 9 p2 l1 l2.As a partial order, : 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).;liospeaksFor 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`<lioQThis 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.=lio 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`>lioGreatest 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`?lio 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`@lioSTurns privileges into a powerless description of the privileges by unwrapping the  newtype.AlioUses 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.Blio object corresponding to 5.Glio8 5# is the identify function. Hence 9 5 is the same as ?.8lioPrivilege descriptionlioLabel to downgradelio Lowest label equivelent to input56789:;<=>?@AB<=>?:;789@A56B;4=5>5?4 TrustworthyKlio 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 M.Llio A variant of K that returns results in  and exceptions in !, much like the standard library  function.Mlio 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 K7, this function throws an exception if the underlying % action terminates with an exception.Nlio'Initialize some privileges (within the  monad) that can be passed to  computations run with K or M?. 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.KLMNKLMN Trustworthy=?@ACOlioSynonym for monad in which  is the base monad.PlioLift an  computation.OPOP Trustworthy2EXRlioThrow an exception.SlioA 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.)Tlio A version of S# with the arguments swapped around.UlioLike V[, but only performs the final action if there was an exception raised by the computation. Vlio A variant of WE where the return value from the first computation is not required. WliotWhen 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). XlioQForces its argument to be evaluated to weak head normal form when the resultant  action is executed.Ylio!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.WlioComputation to run firstlioComputation to run lastlioComputation to run in-betweenRSTUVWXYRSTYUVWX Trustworthy2EXlZlio+Error raised when a computation spawned by lForkB terminates with its current label above the label of the result.`liokError 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).flio0Main error type thrown by label failures in the  monad.hlio)Annotation of where the failure happened.ilioActual function that failed.jlioCurrent label at time of error.klio#Current clearance at time of error.llio!Any privileges involved in error.mlioAny labels involved in error.nlioQA generic privilege description for recording relevant privileges in exceptions.plio'Parent of all label-related exceptions.rlio;Class of error messages that can be annotated with context.tlio]Executes an action with a context string, which will be added to any label exception thrown.+Note: this function wraps an action with a Sh, and thus may incur a small runtime cost (though it is well under 100 ns on machines we benchmarked).ulioDefinition of  for children of p in the exception hierarchy.vlioDefinition of  for children of p in the exception hierarchy.wlioThrow a label-error exception.xlioThrow a label-error exception.ylioRaise ` error.wlioFunction that failed.lioLabels involved in error.xlioFunction that failed.lioPrivileges involved.lioLabels involved.ylioFunction in which error occurslio"Description of privileges suppliedlio Description of privileges needed Z[\]^_`abcdefghijklmnopqrstuvwxy rstpquvnofghijklmwx`abcdeyZ[\]^_Safe2EXRlioSee .lioSee .lioFunction that failed.lioLabels involved in error.lioFunction that failed.lioPrivileges involved.lioLabels involved. Trustworthy2lioRA 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.liodelegate 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 7l 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.liodCreate 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.lioguardGate 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 minPrivlioYGiven 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.lioGate computationlioGatelio$Privilege used as proof-of-ownership  Trustworthy=?@ACEXlio0Returns the value of the thread's current label.liolRaises the current label to the provided label, which must be between the current label and clearance. See .lioIf 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 9 priv oldLabel newLabel && ? newLabel clearanceY. (Note the privilege argument affects the label check, not the clearance check; call  first to raise the clearance.)lio'Returns the thread's current clearance.lioLowers 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.lio6Raises 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., 9 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.lioRuns 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.lioVTemporarily 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 .lio A variant of ( that takes privileges. Equivalent to: withClearanceP p c lio =  $  p c >> lio lioEnsures 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.lioLike 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.lioUse 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 f exception if l'5 would have to be higher than the current clearance.lioLike 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.lioUse  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).lioLike 8, but takes a privilege argument to be more permissive.(KMOP`abcdefghijklmpq(OPMKpqfghijklm`abcde  Trustworthyz lioFunction 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 ).lio 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.lio 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 f. You can use  to check beforehand whether  will succeed.lioExtracts 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 fv if the privileges supplied are insufficient to save the current label from needing to exceed the current clearance.lio 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 9.lioRaises 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 ).lioSame 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.lioA 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.lio 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.    Trustworthy}l lioSee  .lioSee  .lioSee  .lioSee  .lioSee  .lioSee  .lioSee  !.lioSee  ".lioSee  #. Safe2=?@Aslio An alias for  values labeled with a .lio privileges are expressed as a 7 of the principals whose authority is being exercised.lio%The main monad type alias to use for $ computations that are specific to s.lio 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 .lioMain 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, 9 p dc1 dc2 (often written dc1 " dc2) if and only if (p  s2) `; ` s2 && (p  i1) `;` i2.lio:Describes the authority required to make the data public.liosDescribes the authority with which immutable data was endorsed, or the authority required to modify mutable data.lio/A boolean formula in Conjunctive Normal Form. CNF is used to describe = privileges, as well to provide each of the two halves of a .lioRepresents 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 ).lioA  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.lio,Extract the name of a principal as a strict . (Use  to get it as a regular .)lio!Create a principal from a strict .lioCreate a principal from a . The  is packed into a  using Y, which will almost certainly give unexpected results for non-ASCII unicode code points.lioExpose the set of s being ORed together in a .lioConvert a list of  s into a .lioReturns 5 iff the first disjunction is a subset of the second.lio Convert a  to a  of .s. Mostly useful if you wish to serialize a .lioA  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; 9 cTrue l1 l2 is equivalent to ? l1 l2. Note that   = cTrue . Hence  =  cTrue cTrue.lioA  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 N 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.lioConvert a list of  s into a 0. Mostly useful if you wish to de-serialize a .lio 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).lioThe 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 %%lioCompute a conjunction of two s or  instances. Has fixity:  infixr 7 /\lioCompute 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 \/lio'A common default starting state, where  =  and  = False  True) (i.e., the highest possible clearance).lioWrapper function for running   computations.  evalDC dc = M dc  lio wrapper for L:  tryDC dc = L dc  lio9Note that a disjunction containing more than one element must2 be surrounded by parentheses to parse correctly.677 Safe=?@ACߊ lioSee  $.lioSee  %.lioSee  &.lioSee  '.lioSee  (.lioSee  ).lioSee  *.lioSee  +.lioSee  ,.lioSee  -.lioSee  ..lioSee  /. 0Safe U56789:;<=>?@BKMOPRSTUVWXY`abcdefghijklmpq56789:;<=>?@BUnsafe2=?@AClioClass for lifting  actions.lio Lifts an  action in the 7 monad, executing a guard before calling the function.lioA "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.lio%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 ().lio A variant of  that produces an ' function taking a privilege argument.lio Similar to X, but enforces the weaker restriction that the action is write-only. When in doubt use .lio Similar to W, but enforces the weaker restriction that the action is read-only. When in doubt use .  Trustworthy,>&  lioAn 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. lioCreate a new reference with a particularlabel. The label specified must be between the thread's current label and clearance, as enforced by . lioSame as   except  newLIORefPc takes privileges which make the comparison to the current label more permissive, as enforced by .lioRead 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.lioSame as  , except  readLIORefPR takes a privilege object which is used when the current label is raised (using  instead of ).lioWrite 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.lioSame as  except  writeLIORefPr takes a set of privileges which are accounted for in comparing the label of the reference to the current label.lioMutate 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 ).lioLike <, but takes a privilege argument and guards execution with  instead of .lio'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 f= exception if any of the IFC conditions cannot be satisfied.lioSame as  except atomicModifyLIORefP% takes a set of privileges and uses  instead of . lioLabel of referencelio Initial valuelioMutable referencelioLabeled referencelioModifier        Safe,>+U lioSee 1.lioSee 2.lioSee 3.lioSee 4.lioSee 5.lioSee 6.lioSee 7.lioSee 8.lioSee 9.lioSee :.lioLabel of referencelio Initial valuelioMutable referencelioLabeled referencelioModifier   Trustworthy,>i lioAn LMVar+ is a labeled synchronization variable (an 9) that can be used by concurrent threads to communicate.!lioCreate 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."lioSame as ! except it takes a set of privileges which are accounted for in comparing the label of the MVar to the current label and clearance.#lioCreate 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.$lioSame as #v except it takes a set of privileges which are accounted for in comparing the label of the MVar to the current label.%lioReturn contents of the  Y. Note that a take consists of a read and a write, since it observes whether or not the  F is full, and thus the current label must be the same as that of the  X (of course, this is not the case when using privileges). Hence, if the label of the   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   is empty,  takeLMVar blocks.&lioSame as % except  takeLMVarPJ takes a privilege object which is used when the current label is raised.'lioNon-blocking version of % . It returns Nothing if the   is empty, otherwise it returns Just value, emptying the  .(lioSame as '2, but uses priviliges when raising current label.)lioPuts a value into an  X. Note that a put consists of a read and a write, since it observes whether or not the  E is empty, and so the current label must be the same as that of the  E (of course, this is not the case when using privileges). As in the % case, if the label of the   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   is full, putLMVar blocks.*lioSame as ) except  putLMVarPJ takes a privilege object which is used when the current label is raised.+lioNon-blocking version of ) . It returns True if the  7 was empty and the put succeeded, otherwise it returns False.,lioSame as +1, but uses privileges when raising current label.-lioCombination of % and ). 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 ), (, or 1 for this  ..lioSame as - except  readLMVarPJ takes a privilege object which is used when the current label is raised./lioTakes a value from an  , puts a new value into the LMvar0, and returns the taken value. Like the other  2 operations it is required that the label of the   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 ) for this  .0lioSame as / except  swapLMVarPJ takes a privilege object which is used when the current label is raised.1lioCheck the status of an  H, i.e., whether it is empty. The function succeeds if the label of the  S is below the current clearance -- the current label is raised to the join of the   label and the current label.2lioSame as 11, but uses privileges when raising current label.!lio Label of LMVarlioNew mutable location#lio Label of LMVarlioInitial value of LMVarlioNew mutable location)lioSource  lio New value/lioSource LMVarlio New valuelio Taken value !"#$%&'()*+,-./012 !"#$%&'()*+,-./012Safen3lioSee ;.4lioSee <.5lioSee =.6lioSee >.7lioSee ?.8lioSee @.9lioSee A.:lioSee B.;lioSee C.<lioSee D.=lioSee E.>lioSee F.?lioSee G.@lioSee H.AlioSee I.BlioSee J.ClioSee K.DlioSee L.3456789:;<=>?@ABCD3456789:;<=>?@ABCD Trustworthy Elio Execute an ) computation in a new lightweight thread.FlioLabeled 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 H\ 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 H.GlioSame as FZ, but the supplied set of priviliges are accounted for when performing label comparisons.HlioGiven 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.IlioSame as H1, but uses priviliges in label checks and raises.JlioSame as H(, but does not block waiting for result.KlioSame as J1, but uses priviliges in label checks and raises.LlioLike H, 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 ZP 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.Mlio A version of Lx that takes privileges. The privileges are used both to downgrade the result (if necessary), and to try catching any Z* before the timeout period (if possible).FlioLabel of resultlio)Computation to execute in separate threadlioLabeled result#Z[\]^_ !"#$%&'()*+,-./012EFGHIJKLMEFGZ[\]^_HIJKLM TrustworthyE NlioA LChan7 is a labeled channel, i.e., an unbounded FIFO channel.OlioCreate 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.PlioSame as Ov except it takes a set of privileges which are accounted for in comparing the label of the Chan to the current label.QlioqWrite value to the labeled channel. The label of the channel must be bounded by the current label and clearance.RlioSame as QT, but uses privileges when comparing the current label to the label of the channel.SlioRead 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.TlioSame as Sq, but takes a privilege object which is used when the current label is raised to avoid over-taining the context.UliohDuplicate labeled channel. The label of the channel must be bounded by the current label and clearance.VlioSame as UT, but uses privileges when comparing the current label to the label of the channel. NOPQRSTUV NOPSTQRUVSafeWlioSee M.XlioSee N.YlioSee O.ZlioSee P.[lioSee Q.\lioSee R.]lioSee S.^lioSee T.WXYZ[\]^WXYZ[\]^Unsafe 2=?@ACSX_lioTakes 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.alio3IO Object with a mutable label. By contrast with U, the label on an a6 can change over time. If this happens, the internal eN ensures that threads accessing the object receive an asynchronous exception.clio%Class of objects with mutable labels.elioA 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 uJ, to ensure an exception is raised if another thread revokes access with v.kliok 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.mliomt is for objects contained entirely within Haskell, such as a variable. Raising the label can't cause data to leak.olio Class for q:s that don't encode any interesting values. This allows y to create an a& without requiring a policy argument.qlio;Class of policies for when it is permissible to update an e.slioSReturns the immutable label that controls access to the mutable label value of an e.tlioyRetreive a snapshot of the value of a mutable label. Of course, it may already have changed by the time you process it.ulioRun 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.vlioChange the mutable label in an eD. Raises asynchronous exceptions in other threads that are inside u( if the new label revokes their access.lionewMLabelP policy ll l creates an e. 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.wlio Create an e, performing access control checks to ensure that the labels are within the range allowed given the current label and clearance, and the supplied privileges.xlioLike y, but create an aL with a particular policy value. Note that you don't need to use this for k and m, 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.ylioy ll l a creates an a wrapping some IO object a. Here llN is the label on the label, which remains immutable over the lifetime of the a. l, is the initial value of the mutable lable.zlio Modify the e within an a.{lioThe a equivalent of blessTCBF in "LIO.TCB.LObj#v:blessTCB". Use this for conveniently providing LIO versions of standard IO functions.|lioThe a equivalent of  blessPTCBG in "LIO.TCB.LObj#v:blessPTCB". Use this for conveniently providing LIO versions of standard IO functions._`abcdefghijklmnopqrstuvwxyz{|abyxz{|efghijwstuvcdopqrmnkl_`VWXVWYVWZVW[VW\VWX]^_`abcdefghijklmnoo0pqqrstuvwxyz{|}~ $ % & ' ( ) * + , - . /      ! " #      ! " #                             $ % & ' ( ) * + , - . /U !"#$%&'()123456789:123456789:*;<=>?@ABCDEFGHIJKL;<=>?@ABCDEFGHIJKL+,-./01234MNOPQRSTMNOPQRST56789:;<=>?@AABBCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abVcdefefgVhiVhjVkVhlVmnVmoVmpqrsVctVmuVvw xyz{V|}~#lio-0.11.7.0-DlG3TxBVudx1L7FGXZmZl2 LIO.ExceptionLIO.TCB LIO.LabelLIO.Run LIO.Monad LIO.ErrorLIO.Error.Trans LIO.DelegateLIO.Core LIO.LabeledLIO.Labeled.Trans LIO.DCLabelLIO.Core.Trans LIO.TCB.LObj LIO.LIORefLIO.LIORef.TransLIO.Concurrent.LMVarLIO.Concurrent.LMVar.TransLIO.ConcurrentLIO.Concurrent.LChanLIO.Concurrent.LChan.Trans LIO.TCB.MLObjIO mapException labelError labelErrorPlabellabelPunlabelunlabelPrelabelLabeledP taintLabeled taintLabeledPlFmaplApgetLabelsetLabel setLabelP getClearance setClearance setClearanceP guardAlloc guardAllocPtainttaintP guardWrite guardWritePLIO newLIORef newLIORefP readLIORef readLIORefP writeLIORef writeLIORefP modifyLIORef modifyLIORefPatomicModifyLIORefatomicModifyLIORefP newEmptyLMVarnewEmptyLMVarPnewLMVar newLMVarP takeLMVar takeLMVarP tryTakeLMVar tryTakeLMVarPputLMVar putLMVarP tryPutLMVar tryPutLMVarP readLMVar readLMVarP swapLMVar swapLMVarP isEmptyLMVar isEmptyLMVarPnewLChan newLChanP writeLChan writeLChanP readLChan readLChanPdupLChan dupLChanPLObjbaseGHC.Exception.Type SomeExceptiondisplayException fromException toException Exception LabeledResultLabeledResultTCBlresThreadIdTCB lresLabelTCB lresBlockTCB lresStatusTCB LResStatus LResEmptyLResLabelTooHigh LResResultShowTCBshowTCBLabelOflabelOfLabeled LabeledTCBPrivPrivTCBUncatchableTCBLIOTCBLIOStatelioLabel lioClearancegetLIOStateTCBputLIOStateTCBmodifyLIOStateTCBioTCB makeCatchable$fApplicativeLIO $fFunctorLIO $fMonadLIO$fExceptionUncatchableTCB$fShowUncatchableTCB $fMonoidPriv$fSemigroupPriv$fLabelOfLabeled$fShowTCBLabeled$fLabelOfLabeledResult $fEqLIOState$fShowLIOState$fReadLIOState $fShowPriv$fEqPriv$fShowLResStatusNoPrivsPrivDesc downgradeP canFlowToP SpeaksFor speaksForLabellubglb canFlowToprivDescisPrivnoPrivs$fSpeaksForPriv$fPrivDesclPriv$fMonoidNoPrivs$fSemigroupNoPrivs$fPrivDesclNoPrivs$fSpeaksForNoPrivs $fShowNoPrivs $fReadNoPrivsrunLIOtryLIOevalLIOprivInitMonadLIOliftLIO$fMonadLIOlLIOthrowLIOcatchhandle onExceptionfinallybracketevaluatetryResultExceedsLabel relContext relLocationrelDeclaredLabelrelActualLabelInsufficientPrivs inspContext inspFailure inspSupplied inspNeeded LabelError lerrContext lerrFailure lerrCurLabellerrCurClearance lerrPrivs lerrLabelsGenericPrivDesc AnyLabelError Annotatableannotate withContextlerrToExceptionlerrFromExceptioninsufficientPrivs$fExceptionAnyLabelError$fAnnotatableAnyLabelError$fShowAnyLabelError$fShowGenericPrivDesc$fExceptionLabelError$fAnnotatableLabelError$fExceptionInsufficientPrivs$fAnnotatableInsufficientPrivs$fShowInsufficientPrivs$fExceptionResultExceedsLabel$fAnnotatableResultExceedsLabel$fShowLabelError$fShowResultExceedsLabelGatedelegategate guardGatecallGatescopeClearance withClearancewithClearanceP DCLabeledDCPrivDCToCNFtoCNFDCLabel dcSecrecy dcIntegrityCNF Disjunction Principal principalName principalBS principaldToSet dFromListcToSetcTruecFalse cFromListdcPublic%%/\\/dcDefaultStateevalDCtryDC $fEqPrincipal$fReadPrincipal$fShowPrincipal$fMonoidDisjunction$fSemigroupDisjunction$fReadDisjunction$fShowDisjunction$fOrdDisjunction$fEqDisjunction$fSpeaksForCNF $fMonoidCNF$fSemigroupCNF $fReadCNF $fShowCNF$fPrivDescDCLabelCNF$fLabelDCLabel $fReadDCLabel $fShowDCLabel $fToCNFBool $fToCNF[]$fToCNFPrincipal$fToCNFDisjunction $fToCNFPriv $fToCNFCNF$fOrdPrincipal$fEqCNF$fOrdCNF $fEqDCLabel $fOrdDCLabelGuardIO guardIOTCBLObjTCBblessTCB blessPTCBblessWriteOnlyTCBblessWriteOnlyPTCBblessReadOnlyTCBblessReadOnlyPTCB $fShowTCBLObj $fLabelOfLObj$fGuardIOl->->$fGuardIOl->->0$fGuardIOl->->1$fGuardIOl->->2$fGuardIOl->->3$fGuardIOl->->4$fGuardIOl->->5$fGuardIOl->->6$fGuardIOl->->7$fGuardIOl->->8$fGuardIOlIOLIOLIORefLMVarforkLIOlForklForkPlWaitlWaitPtrylWait trylWaitP timedlWait timedlWaitPLChanLabelIOlabelIOMLObjMLObjTCBMLabelOfmLabelOfMLabel MLabelTCB mlLabelLabelmlLabelmlUsersmlPolicy ExternalML InternalMLMLabelPolicyDefaultmlabelPolicyDefault MLabelPolicy mlabelPolicy labelOfMlabel readMLabelP withMLabelP modifyMLabelP newMLabelPmlPolicyObjTCBmlObjTCBmodifyMLObjLabelP mblessTCB mblessPTCB$fMLabelPolicyDefaultInternalML$fMLabelPolicyInternalMLl$fMLabelPolicyDefaultExternalML$fMLabelPolicyExternalMLl$fMLabelOfMLObj$fLabelIOl->->$fLabelIOl->->0$fLabelIOl->->1$fLabelIOl->->2$fLabelIOl->->3$fLabelIOl->->4$fLabelIOl->->5$fLabelIOl->->6$fLabelIOl->->7$fLabelIOl->->8$fLabelIOlIOLIO$fShowInternalML$fShowExternalMLGHC.ShowShowghc-prim GHC.TypesTrue Data.EitherRightLeftControl.Exception.BaseEitherGHC.Basemappendfmapapbytestring-0.10.8.2Data.ByteString.Internal ByteStringshowString Data.String fromStringdImpliescontainers-0.6.0.1Data.Set.InternalSetGHC.MVarMVar newMLabelTCB