{l      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{ | } ~  UnsafeA  LabeledResult1 encapsulates a future result from a computation  spawned by lFork or lForkP. See LIO.Concurrent for a 5 description of the concurrency abstractions of LIO. !Thread executing the computation Label of the tresult <Result (when it is ready), or the label at which the thread - terminated, if that label could not flow to .  Status of a . @It would be a security issue to make certain objects members of  the 8 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, E instance, if you wish to associate a label with a pure value (as in   LIO.Labeled), you may create a data type:  # newtype LVal l a = LValTCB (l, a) DThen, you may wish to allow untrusted code to read the label of any  LVal9s but not necessarily the actual value. To do so, simply  provide an instance for LabelOf:  instance LabelOf LVal where ! labelOf (LValTCB lv) = fst lv <Get the label of a labeled value or object. Note the label 7 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 a+. Labeled values allow users to label data 7 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 Labeled, then the label : on the inner value will be protected by the outer label. BA newtype wrapper that can be used by trusted code to transform a B powerless description of privileges into actual privileges. The  constructor, (, is dangerous as it allows creation of @ arbitrary privileges. Hence it is only exported by the unsafe  module LIO.TCB3. A safe way to create arbitrary privileges is to  call privInit (see LIO.Run#v:privInit ) from the  monad  before running your  computation. ;An uncatchable exception hierarchy is used to terminate an 6 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 B 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  monad. However, trusted  runtime functions can use " to perform  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 A 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  monad. This function is E 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. (  !"#  !"# !"#     !"# Trustworthy $Generic &/ used to denote the lack of privileges. Works  with any +0 type. This is only a privilege description; a  more useful symbol is 0, which actually embodies the  NoPrivs privilege. &=This class represents privilege descriptions, which define a A pre-order on labels in which distinct labels become equivalent. E The pre-oder implied by a privilege description is specified by the  method (1. In addition, this this class defines a method  '., which is important for finding least labels % satisfying a privilege equivalence. Minimal complete definition: '. (The '0 requirement represents the fact that a generic  (, can be implemented efficiently in terms of  ', but not vice-versa.) '>Privileges are described in terms of a pre-order on labels in 3 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 l returns a label representing - the furthest you can downgrade data labeled l given  privileges described by p. .Yet another way to view this function is that downgradeP p l ) returns the greatest lower bound (under . ) of the set  of all labels l' such that ( p l' l. (canFlowToP p l1 l2 determines whether p describes / sufficient privileges to observe data labeled l1 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:  5 canFlowToP p l1 l2 = downgradeP p l1 `canFlowTo` l2  canFlowToP3 is a method rather than a function so that it can 7 be optimized in label-specific ways. However, custom 7 definitions should behave identically to the default. ),Every privilege type must be an instance of ), which C specifies when one privilege value is more powerful than another. ? If you do not wish to allow delegation, you can simply define  * _ _ = False. *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` +AThis class defines the operations necessary to make a label into  a lattice (see  ,http://en.wikipedia.org/wiki/Lattice_(order)).  . partially orders labels.  , and -2 compute the least upper bound and greatest lower $ bound of two labels, respectively. , Compute the least upper bound , or join, of two labels. When ; data carrying two different labels is mixed together in a  document, the lub, 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, and  There 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, and  There 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` /@Turns privileges into a powerless description of the privileges  by unwrapping the  newtype. 0 object corresponding to $. ' $" is the identify function. Hence  ( $ is the same as .. $%&'Privilege description Label to downgrade !Lowest label equivelent to input ()*+,-./0$%&'()*+,-./0+,-.)*&'(/$%0 $%&'()*+,-./0 Trustworthy1 Execute an 2 action, returning its result and the final label B state as a pair. Note that it returns a pair whether or not the  < action throws an exception. Forcing the result value will C re-throw the exception, but the label state will always be valid.  See also 3. 2 A variant of 1 that returns results in  and  exceptions in !, much like the standard library   function. 3 Given an 2 computation and some initial state, return an IO < action which, when executed, will perform the IFC-safe LIO  computation. &Because untrusted code cannot execute  computations, this function B should only be useful within trusted code. No harm is done from  exposing the evalLIO) symbol to untrusted code. (In general, # untrusted code is free to produce  computations, but it cannot  execute them.) Unlike 1+, this function throws an exception if the  underlying & action terminates with an exception. 4'Initialize some privileges (within the  monad) that can be  passed to  computations run with 1 or 3. This 7 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 . is easier to misuse and is only available by  importing LIO.TCB. 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  objects. 1234123412341234 Trustworthy5Throw an exception. 6BA simple wrapper around IO catch. The only subtlety is that code @ is not allowed to run unless the current label can flow to the D 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 scopeClearance can lead to the label B exceeding the clarance, and an exception is always thrown at the  time this happens.) 7 A version of 6$ with the arguments swapped around. 8Like 92, but only performs the final action if there was * an exception raised by the computation. 9 A variant of :' where the return value from the first  computation is not required. :?When you want to acquire a resource, do some work with it, and 5 then release the resource, it is a good idea to use bracket, A because bracket will install the necessary exception handler to ? release the resource in the event that an exception is raised A during the computation. If an exception is raised, then bracket > will re-raise the exception (after performing the release). ;BForces its argument to be evaluated to weak head normal form when  the resultant  action is executed. <!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 ex. E If any other type of exception is raised than it will be propogated - up to the next enclosing exception handler. 56789:Computation to run first Computation to run last Computation to run in-between ;< 56789:;< 567<89:;56789:;< Trustworthy=+Error raised when a computation spawned by lFork terminates 7 with its current label above the label of the result. C=Error indicating insufficient privileges (independent of the . current label). This exception is thrown by delegate, and D should also be thrown by gates that receive insufficient privilege  descriptions (see  LIO.Delegate). I0Main error type thrown by label failures in the  monad. K*Annotation of where the failure happened. LActual function that failed. M Current label at time of error. N$Current clearance at time of error. O"Any privileges involved in error. PAny labels involved in error. QBA generic privilege description for recording relevant privileges  in exceptions. S(Parent of all label-related exceptions. U<Class of error messages that can be annotated with context. W@Executes an action with a context string which will be added to  any label exception thrown. +Note: this function wraps an action with a 6, and thus may ? incur a small runtime cost (though it is well under 100 ns on  machines we benchmarked). XDefinition of  for children of S in  the exception hierarchy. YDefinition of  for children of S in  the exception hierarchy. ZThrow a label-error exception. [Throw a label-error exception. \Raise C error. +=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZFunction that failed. Labels involved in error. [Function that failed. Privileges involved. Labels involved. \ =>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\ UVWSTXYQRIJKLMNOPZ[CDEFGH\=>?@AB=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\ Trustworthy]BA Gate is a lambda abstraction from a privilege description to an  arbitrary type a). Applying the gate is accomplished with ` E which takes a privilege argument that is converted to a description ' before invoking the gate computation. ^delegate5 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  &9 describing the desired new privileges. The call throws - an exception unless the privileges supplied * the  privileges requested. 9Note: If you are looking for a way to create privileges more 6 powerful than ones you already have, you can use the mappend * function to combine existing privileges. _@Create a gate given a computation from a privilege description. $ Note that because of currying type a may itself be a function E type and thus gates can take arguments in addition to the privilege  descriptoin. `AGiven a gate and privilege, execute the gate computation. It is  important to note that callGate# 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 A function is provided by LIO since it can be easily inspected by 2 both the gate creator and caller to be doing the "right" thing: A provide the privilege description corresponding to the supplied  privilege as "proof". without explicitly passing in the privilege. ]^_Gate computation `Gate %Privilege used as proof-of-ownership ]^_`^]_`]^_` TrustworthyaSynonym for monad in which  is the base monad. bLift an  computation. cReturns the value of the thread's current label. d>Raises the current label to the provided label, which must be . between the current label and clearance. See n. eIf the current label is oldLabel and the current clearance is   clearance7, this function allows code to raise the current label  to any value newLabel such that ( priv oldLabel  newLabel && . newLabel clearance. (Note the privilege A argument affects the label check, not the clearance check; call  h first to raise the clearance.) fReturns the thread's current clearance. g@Lowers the current clearance. The new clerance must be between D the current label and previous current clerance. One cannot raise @ the current label or create object with labels higher than the  current clearance. h5Raises the current clearance (undoing the effects of  g5) by exercising privileges. If the current label is  l and current clearance is c, then setClearanceP p cnew ? succeeds only if the new clearance is can flow to the current & clearance (modulo privileges), i.e., ( p cnew c ==  True8. Additionally, the current label must flow to the new  clearance, i.e., l `.` cnew == True. +Since LIO guards that are used when reading/writing data (e.g.,  m7) do not use privileges when comparing labels with the E current clearance, code must always raise the current clearance, to  read/(write data above the current clearance. iRuns an 1 action and re-sets the current clearance to its @ previous value once the action returns. In particular, if the E action lowers the current clearance, the clearance will be restored  upon return.  Note that scopeClearance$ always restores the clearance. If > that causes the clearance to drop below the current label, a  ClearanceViolation/ exception is thrown. That exception can only  be caught outside a second scopeClearance that restores the - clearance to higher than the current label. jBTemporarily lowers the clearance for a computation, then restores  it. Equivalent to:    withClearance c lio = i $ g c >> lio $Note that if the computation inside  withClearance acquires any  9s, it may still be able to raise its clearance above the  supplied argument using h. k A variant of j$ that takes privileges. Equivalent  to:   withClearanceP p c lio = i $ h p c >> lio l?Ensures the label argument is between the current IO label and A 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 l does not throw an exception. 8 Similarly use this guard in any code that writes to an  object labeled l' for which the write has no observable  side-effects. mLike l*, but takes privilege argument to be more # permissive. Note: privileges are only used when checking that 0 the current label can flow to the given label. nUse taint l4 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 I exception if l' 5 would have to be higher than the current clearance. oLike n3, but use privileges to reduce the amount of taint  required. Note that taintP% will never lower the current label. A It simply uses privileges to avoid raising the label as high as  n would raise it. pUse  guardWrite l+ in any (trusted) code before modifying an  object labeled l., 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 l This guarantees that l `.` the current label (and ( clearance), and that the current label `.` l. qLike p,, but takes a privilege argument to be more  permissive. abcdefghijklmnopq(13CDEFGHIJKLMNOPSTabcdefghijklmnopq(ab31cdefghijkSTIJKLMNOPCDEFGHlmnopqabcdefghijklmnopq Trustworthy rFunction to construct a " from a label and pure value. If  the current label is lcurrent and the current clearance is  ccurrent, then the label l specified must satisfy  lcurrent  `.` l && l `.` ccurrent. Otherwise an  exception is thrown (see l). s Constructs a  using privilege to allow the '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 `.` ccurrent-. Note that privilege is not used to bypass  the clearance. You must use h to raise the clearance  first if you wish to create an  at a higher label than the  current clearance. t Within the  monad, this function takes a  and returns % the underlying value. Thus, in the  monad one can say:  0 x <- unlabel (xv :: Labeled SomeLabelType Int) +And now it is possible to use the value of x :: Int, which is the " pure value of what was stored in xv. Of course, unlabel also B raises the current label. If raising the label would exceed the  current clearance, then unlabel throws ClearanceViolation.  However, you can use  to check if t will succeed  without throwing an exception. uExtracts the value of an  just like t, but takes a E privilege argument to minimize the amount the current label must be  raised. Function will throw ClearanceViolation under the same  circumstances as t. v Relabels a * value to the supplied label if the given E privilege privileges permits it. An exception is thrown unless the  following two conditions hold: ? The new label must be between the current label and clearance * (modulo privileges), as enforced by m. 8 The old label must flow to the new label (again modulo " privileges), as enforced by (. wRaises the label of a  to the  upperBound of it' s current F label and the value supplied. The label supplied must be bounded by H the current label and clearance, though the resulting label may not be  if the $ is already above the current thread's clearance. If ( the supplied label is not bounded then  taintLabeled will throw an  exception (see l). xSame as w), but uses privileges when comparing the D current label to the supplied label. In other words, this function C can be used to lower the label of the labeled value by leveraging  the supplied privileges. y Similar to , apply function to the  value. The E label of the returned value is the least upper bound of the current 0 label and label of the supplied labeled value. z Similar to , apply function (wrapped by  ) to the B labeld value. The label of the returned value is the least upper B bound of the current label, label of the supplied labeled value, % and label of the supplied function. rstuvwxyz rstuvwxyz rstuvwxyz rstuvwxyz Unsafe{Class for lifting  actions. | Lifts an  action in the  monad, executing a guard  before calling the function. }A "LObj label object"' is a wrapper around an IO abstraction  of type object2 (such as a file handle or socket) on which it is  safe to do IO operations in the  monad when the caller can B read and write a particular label. It is the job of the trusted  code constructing such a LObj% object to ensure both that the same = IO object is only ever blessed with one label, and that the : abstraction combined with its blessed IO operations (see  5) 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 p! to check that the current label  can write the label in the } object. DThe first argument should be the name of the function being defined  with blessTCB.. Its purpose is to enhance error reporting.  Note that io and lio# are function types (of up to nine C 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 takes a privilege argument. {|}~{|}~}~{|{|}~  Trustworthy An LIORef is an IORef' with an associated, fixed label. The A restriction to an immutable label come from the fact that it is F possible to leak information through the label itself, if we wish to  allow LIORef to be an instance of . Of course, you can  create an LIORef of  to get a limited form of  flow-sensitivity. =To create a new reference the label of the reference must be  below the thread'1s current clearance and above the current label. E If this is the case, the reference is built. Otherwise an exception " will be thrown by the underlying l guard. Same as  except  newLIORefP takes a set of > privileges which are accounted for in comparing the label of 3 the reference to the current label and clearance. CRead the value of a labeled reference. A read succeeds only if the B label of the reference is below the current clearance. Moreover, B the current label is raised to the join of the current label and ; the reference label. To avoid failures (introduced by the n  guard) use $ to check that a read will succeed. Same as  except  readLIORefP takes a privilege object 1 which is used when the current label is raised. @Write a new value into a labeled reference. A write succeeds if C the current label can-flow-to the label of the reference, and the F label of the reference can-flow-to the current clearance. Otherwise, * an exception is raised by the underlying l guard. Same as  except  writeLIORefP takes a set of > privileges which are accounted for in comparing the label of 3 the reference to the current label and clearance. @Mutate the contents of a labeled reference. For the mutation to H succeed it must be that the current label can flow to the label of the C reference, and the label of the reference can flow to the current D clearance. Note that because a modifier is provided, the reference G contents are not observable by the outer computation and so it is not E required that the current label be raised. It is, however, required E that the label of the reference be bounded by the current label and ) clearance (as checked by the underlying l guard). Same as  except  modifyLIORefP takes a set of > privileges which are accounted for in comparing the label of 3 the reference to the current label and clearance. 'Atomically modifies the contents of an . It is required A that the label of the reference be above the current label, but C 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 join of the current and reference 3 labels). These checks and label raise are done by p, C which will raise an exception if any of the IFC conditions cannot  be satisfied. Same as  except atomicModifyLIORefP takes C a set of privileges which are accounted for in label comparisons. Label of reference Initial value Mutable reference Labeled reference  Modifier  TrustworthyAn LMVar+ is a labeled synchronization variable (an ) that 3 can be used by concurrent threads to communicate. ECreate a new labeled MVar, in an empty state. Note that the supplied H label must be above the current label and below the current clearance. / An exception will be thrown by the underlying l if this is  not the case. Same as + except it takes a set of privileges which E are accounted for in comparing the label of the MVar to the current  label and clearance. @Create a new labeled MVar, in an filled state with the supplied E value. Note that the supplied label must be above the current label " and below the current clearance. Same as / except it takes a set of privileges which are G accounted for in comparing the label of the MVar to the current label  and clearance. Return contents of the &. Note that a take consists of a read 3 and a write, since it observes whether or not the  is full, and 8 thus the current label must be the same as that of the  (of E course, this is not the case when using privileges). Hence, if the  label of the . is below the current clearance, we raise the E 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  p8 will throw an exception if any of the IFC checks fail.  Finally, like MVars if the  is empty,  takeLMVar  blocks. Same as  except  takeLMVarP takes a privilege object 1 which is used when the current label is raised. Non-blocking version of  . It returns Nothing if the   is empty, otherwise it returns Just value, emptying the  . Same as +, but uses priviliges when raising current  label. Puts a value into an ). Note that a put consists of a read and / a write, since it observes whether or not the  is empty, and so 3 the current label must be the same as that of the  (of course, 8 this is not the case when using privileges). As in the   case, if the label of the $ is below the current clearance, we H 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 p throws an exception.  If the  is full, putLMVar blocks. Same as  except  putLMVarP takes a privilege object 1 which is used when the current label is raised. Non-blocking version of  . It returns True if the  7 was empty and the put succeeded, otherwise it returns False. Same as 2, but uses privileges when raising current label. Combination of  and . Read the value, and D just put it back. This operation is not atomic, and can can result D in unexpected outcomes if another thread is simultaneously calling  a function such as , , or   for this . Same as  except  readLMVarP takes a privilege object 1 which is used when the current label is raised. Takes a value from an , puts a new value into the LMvar, . and returns the taken value. Like the other  operations it is  required that the label of the  be above the current label and G below the current clearance. Moreover, the current label is raised to 1 accommodate for the observation. The underlying p throws an H exception if this cannot be accomplished. This operation is atomic iff " there is no other thread calling  for this . Same as  except  swapLMVarP takes a privilege object 1 which is used when the current label is raised. Check the status of an !, i.e., whether it is empty. The ' function succeeds if the label of the  is below the current = clearance -- the current label is raised to the join of the   label and the current label. Same as 2, but uses privileges when raising current label.  Label of LMVar New mutable location  Label of LMVar Initial value of LMVar New mutable location Source   New value Source LMVar  New value  Taken value   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 E 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 3 computation has terminated, one will have to call  and E raise the current label. Of couse, this can be postponed until the  result is needed. lFork6 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 l. @ Moreover, the supplied computation must not terminate with its D label above the result label; doing so will result in an exception 0 being thrown in the thread reading the result.  Note that lFork immediately returns a  , which is  essentially a "future", or "promise". This prevents  timing/8termination attacks in which the duration of the forked ) computation affects the duration of the lFork. FTo guarantee that the computation has completed, it is important that 9 some thread actually touch the future, i.e., perform an . Same as 3, 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 B the result must be above the current label and below the current , clearance. Moreover, before block-reading, lWait raises the current A label to the join of the current label and label of result. An ' exception is thrown by the underlying n if this is not the F case. Additionally, if the thread terminates with an exception (for A example if it violates clearance), the exception is rethrown by  lWait@. Similarly, if the thread reads values above the result label, 0 an exception is thrown in place of the result. Same as 2, but uses priviliges in label checks and raises. Same as ), but does not block waiting for result. Same as 2, 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'6s result exceeds what the calling thread can observe,   timedlWait) consumes the whole timeout and throws a  =0 exception you can catch (i.e., it never raises ! the label above the clearance). CBecause this function can alter the result by killing a thread, it  requires the label of the  to be both readable and  writable at the current label.  A version of ( that takes privileges. The privileges B are used both to downgrade the result (if necessary), and to try  catching any = before the timeout period (if  possible). Label of result *Computation to execute in separate thread Labeled result #=>?@AB=>?@AB  Trustworthy An alias for  values labeled with a .  privileges are expressed as a  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  /s. However, mathematically speaking, a single   or single ! is also a degenerate example of ! conjunctive normal form. Class  abstracts over the 8 differences between these types, promoting them all to . Main DCLabel type. DCLabels use  boolean formulas over ? principals to express authority exercised by a combination of  principals. A DCLabel contains two  s. One, , @ specifies the minimum authority required to make data with the ' label completely public. The second, , expresses the E minimum authority that was used to endorse data with the label, or, C 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 A other words, data can flow in the direction of requiring more C authority to make it public or removing integrity endorsements.  Given two DCLabels  dc1 = (s1  i1) and  dc 2 = (s2   i2), and a p:: representing privileges,  canFlowToPrivDesc 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. #Describes 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 0 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   Disjunction5s unless you need to serialize and de-serialize them  (by means of  and ). A  Principal4 is a primitive source of authority, represented as A 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 , 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 6 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   = cTrue%, it means data carries no integrity . guarantees. As a description of privileges, cTrue conveys no  privileges; canFlowToPrivDesc cTrue l1 l2 is equivalent to  . l1 l2.  Note that   = cTrue . Hence  =   cTrue cTrue. A  that is always False. If  = cFalse, then B 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  to indicate a thread may  arbitrarily raise its label.  = cFalse, indicates impossibly much integrity--i.e., 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, cFalse indicates impossibly high = privileges (i.e., higher than could be achieved through any  combination of s). cFalse `*` p for any   p2. This can be a useful concept for bootstrapping  privileges within the ) monad itself. For instance, the result  of 4 cFalse can be passed to fully-trusted  code,  which can in turn use delegate to create arbitrary finite - privileges to pass to less privileged code. Convert a list of  s into a . Mostly useful if  you wish to de-serialize a .   dcPublic = True %% True DThis label corresponds to public data with no integrity guarantees. A For instance, an unrestricted Internet socket should be labeled  dcPublic. The significance of dcPublic is that given data  labeled (s %% i), s, is the exact minimum authority required to  transition the data to dcPublic". Conversely, given data labeled  dcPublic, i3 is the exact authority required to transition the  data to (s %% i)" (assuming sufficient clearance). The primary way of creating a . The secrecy component D goes on the left, while the integrity component goes on the right,  e.g.:  $ label = secrecyCNF %% integrityCNF  Unlike the 0 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  instances. Note A 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 = 3 dc   wrapper for 2:   tryDC dc = 2 dc  9Note that a disjunction containing more than one element must 2 be surrounded by parentheses to parse correctly. C      !"<      !"SafeS$%&'()*+,-./01356789:;<CDEFGHIJKLMNOPST]^_`abcdefghijklmnopqrstuvwxyz# !"#$%&'())*++,-./01233456789:;<=>?@ABCDEFGHIJKKLMNOPPQRSTUUVWXYZ[\\]]^_`abcdefghijklmnopqrstuvwxyz{|}~               J                             ! " # $ % & ' ( ) * + , - . / 0 1 23 lio-0.11.0.0 LIO.ExceptionLIO.TCB LIO.LabelLIO.Run LIO.Error LIO.DelegateLIO.Core LIO.Labeled LIO.TCB.LObj LIO.LIORefLIO.Concurrent.LMVarLIO.Concurrent LIO.DCLabelIO mapExceptionLIObase GHC.Exception SomeException fromException toException Exception LabeledResultLabeledResultTCBlresThreadIdTCB lresLabelTCB lresBlockTCB lresStatusTCB LResStatus LResResultLResLabelTooHigh LResEmptyShowTCBshowTCBLabelOflabelOfLabeled LabeledTCBPrivPrivTCBUncatchableTCBLIOTCBLIOStatelioLabel lioClearancegetLIOStateTCBputLIOStateTCBmodifyLIOStateTCBioTCB makeCatchableNoPrivsPrivDesc downgradeP canFlowToP SpeaksFor speaksForLabellubglb canFlowToprivDescnoPrivsrunLIOtryLIOevalLIOprivInitthrowLIOcatchhandle onExceptionfinallybracketevaluatetryResultExceedsLabel relContext relLocationrelDeclaredLabelrelActualLabelInsufficientPrivs inspContext inspFailure inspSupplied inspNeeded LabelError lerrContext lerrFailure lerrCurLabellerrCurClearance lerrPrivs lerrLabelsGenericPrivDesc AnyLabelError Annotatableannotate withContextlerrToExceptionlerrFromException labelError labelErrorPinsufficientPrivsGatedelegategatecallGateMonadLIOliftLIOgetLabelsetLabel setLabelP getClearance setClearance setClearancePscopeClearance withClearancewithClearanceP guardAlloc guardAllocPtainttaintP guardWrite guardWritePlabellabelPunlabelunlabelPrelabelLabeledP taintLabeled taintLabeledPlFmaplApGuardIO guardIOTCBLObjLObjTCBblessTCB blessPTCBLIORef newLIORef newLIORefP readLIORef readLIORefP writeLIORef writeLIORefP modifyLIORef modifyLIORefPatomicModifyLIORefatomicModifyLIORefPLMVar newEmptyLMVarnewEmptyLMVarPnewLMVar newLMVarP takeLMVar takeLMVarP tryTakeLMVar tryTakeLMVarPputLMVar putLMVarP tryPutLMVar tryPutLMVarP readLMVar readLMVarP swapLMVar swapLMVarP isEmptyLMVar isEmptyLMVarPforkLIOlForklForkPlWaitlWaitPtrylWait trylWaitP timedlWait timedlWaitP DCLabeledDCPrivDCToCNFtoCNFDCLabel dcSecrecy dcIntegrityCNF Disjunction Principal principalName principalBS principaldToSet dFromListcToSetcTruecFalse cFromListdcPublic%%/\\/dcDefaultStateevalDCtryDCGHC.ShowShowghc-prim GHC.Types$fShowTCBLabeled$fLabelOfLabeledResult$fLabelOfLabeled $fMonoidPriv$fExceptionUncatchableTCB$fShowUncatchableTCB$fApplicativeLIO $fFunctorLIO $fMonadLIOTrue$fPrivDesclNoPrivs$fMonoidNoPrivs$fSpeaksForNoPrivs$fPrivDesclPriv$fSpeaksForPriv Data.EitherRightLeftControl.Exception.BaseisPrivEither$fExceptionResultExceedsLabel$fAnnotatableResultExceedsLabel$fExceptionInsufficientPrivs$fAnnotatableInsufficientPrivs$fShowInsufficientPrivs$fExceptionLabelError$fAnnotatableLabelError$fShowGenericPrivDesc$fExceptionAnyLabelError$fAnnotatableAnyLabelError$fShowAnyLabelErrorGateTCB$fMonadLIOlLIOGHC.Basefmap Control.Monadap$fGuardIOl(->)(->)$fGuardIOl(->)(->)0$fGuardIOl(->)(->)1$fGuardIOl(->)(->)2$fGuardIOl(->)(->)3$fGuardIOl(->)(->)4$fGuardIOl(->)(->)5$fGuardIOl(->)(->)6$fGuardIOl(->)(->)7$fGuardIOl(->)(->)8$fGuardIOlIOLIO $fShowTCBLObj $fLabelOfLObjGHC.MVarMVarbytestring-0.10.0.2Data.ByteString.Internal ByteStringshowString Data.String fromStringdImpliescontainers-0.5.0.0 Data.Set.BaseSet$fReadDisjunctionSetTagdFalse dSingletondUnion cSingletonsetAnysetAllcInsertcUnioncOr cImplies1cImpliesdcMaxDowngrade$fPrivDescDCLabelCNF$fSpeaksForCNF$fLabelDCLabel $fToCNFBool $fToCNF[]$fToCNFPrincipal$fToCNFDisjunction $fToCNFPriv $fToCNFCNF $fReadDCLabel $fShowDCLabel $fMonoidCNF $fReadCNF $fShowCNF$fMonoidDisjunction$fShowDisjunction$fOrdDisjunction$fEqDisjunction $fEqPrincipal$fReadPrincipal$fShowPrincipal