'M      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abc d e f g h i j k l m n o p q r s t u v w x y z { | } ~  Safe<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 type kinded * -> * >This class defines a label format, corresponding to a bounded  lattice (see  -https://en.wikipedia.org/wiki/Bounded_lattice). : Specifically, it is necessary to define a bottom element  bottom (in literature, written as "), a top element top (in  literature, written as "!), a join, or least upper bound,   (in literature, written as "$), a meet, or greatest lower bound,    (in literature, written as "), and of course the  can-flow-to partial-order   (in literature, written as  "). Least9 upper bound, or join, of two labels. For any two labels  L_1 and L_2, if  L_3 = L_1 `lub` L_2, it must be that:  L_1 ` ` L_3,  L_2 ` ` L_3, and  There is no label L_4 /= L_3  such that  L_1 ` ` L_4, L_2 ` ` L_4, and  L_4 ` ` L_3. In other words L_3 is the least  such element. Greatest9 lower bound, or meet, of two labels. For any two labels  L_1 and L_2, if  L_3 = L_1 `glb` L_2, it must be that:  L_3 ` ` L_1,  L_3 ` ` L_2, and  There is no label L_4 /= L_3 such that  L_4 ` ` L_1, L_4 ` ` L_1, and  L_3 ` ` L_4. In other words L_3 is the greatest  such element. (Can-flow-to relation. An entity labeled L_1 should be allowed  to affect an entity L_2 only if L_1 ` canFlowTo` L_2. This 5 relation on labels is at least a partial order (see   3https://en.wikipedia.org/wiki/Partially_ordered_set ), and must  satisfy the following rules:  Reflexivity: L_1 ` canFlowTo` L_1 for any L_1.  Antisymmetry: If L_1 ` canFlowTo` L_2 and  L_2 ` canFlowTo` L_1 then  L_1 = L_2.  Transitivity: If L_1 ` canFlowTo` L_2 and  L_2 ` canFlowTo` L_3 then L_1 ` canFlowTo` L_3.     Unsafe !It is useful to have the dual of , ReadTCB, that allows 4 for the reading of strings that were created using . Only  readTCB (corresponding to ) and  readsPrecTCB (corresponding  to ) are implemented. Trusted  Trusted  AIt would be a security issue to make certain objects a member of  the 3 class, but nonetheless it is useful to be able to + examine such objects when debugging. The  method can be used  to examine such objects.  Labeled l a, is a value that associates a label of type l with  a value of type a0. Labeled values allow users to label data with C a label other than the current label. In an embedded setting this 9 is akin to having first class labeled values. Note that   is an instance of ), which effectively means that the label  of a 0 value is usually just protected by the current E label. (Of course if you have a nested labeled value then the label  on the inner labeled value's label is the outer label.) <A newtype wrapper that can be used by trusted code to bless 9 privileges. Privilege-related functions are defined in   LIO.Privs, but the constructor, , allows one to mint > arbitrary privileges and hence must be located in this file. AAn uncatchable exception hierarchy use 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. The LIO monad is a state monad, with  as the underlying monad,  that carries along a  current label () and current clearance  (-). The current label imposes restrictions on E what the current computation may read and write (e.g., no writes to C public channels after reading sensitive data). Since the current F label can be raised to be permissive in what a computation observes, C we need a way to prevent certain computations from reading overly G sensitive data. This is the role of the current clearance: it imposes & an upper bound on the current label. 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. Note that  exceptions thrown within the  computation cannot directly be  caught within the 0 computation. Thus, you will generally want to  use  rethrowIoTCB. "$Simple utility function that strips  from around an  exception. Trusted  instance. Trusted  instance. !  !"  !" !"    !" Trustworthy$BA 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.) % A version of $$ with the arguments swapped around. &Like '2, but only performs the final action if there was * an exception raised by the computation. ' 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. #$%&'(Computation to run first Computation to run last Computation to run in-between )* #$%&'()* #$%*&'()#$%&'()* Trustworthy +BA Gate is a lambda abstraction from a privilege description to an  arbitrary type a). Applying the gate is accomplished with 5 E which takes a privilege argument that is converted to a description ' before invoking the gate computation. ,>Generic privilege type used to denote the lack of privileges. -?This class defines privileges and the more-permissive relation  (17) on labels using privileges. Additionally, it defines  23 which is used to downgrage a label up to a limit,  given a set of privilege. .The "can-flow-to given privileges" pre-order used to compare / two labels in the presence of privileges. If 1 p L_1  L_2 holds, then privileges p" are sufficient to downgrade data  from L_1 to L_2 . Note that   L_1 L_2 implies  1 p L_1 L_2 for all p, but for some labels and  privileges, 1 will hold even where   does  not. /Roughly speaking, L_r = partDowngradeP p L L_g computes how 0 close one can come to downgrading data labeled L to the goal  label L_g, given privileges p. When p == ,, the  resulting label  L_r == L `` L_g. If p contains all  possible privileges, then  L_r == L_g. More specifically, L_r$ is the greatest lower bound of the  set of all labels L_l satisfying:    L_g " L_l, and   L "  L_l. Operationally, partDowngradeP& captures the minimum change required 0 to the current label when viewing data labeled L_l . A common ! pattern is to use the result of getLabel as L_g (i.e., the  goal is to use privileges p& to avoid changing the label at all),  and then compute L_r( based on the label of data the code is  about to observe. 1TODO(dm): document 2TODO(dm): document 4@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. 5AGiven 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. With lack of privileges, 1 is simply  , and  2 is the least  upperBound. +,-./ Privileges  Label from which data must flow  Goal label Result 01234Gate computation 5Gate %Privilege used as proof-of-ownership +,-./012345 -./120,3+45 +,-./012345 Trustworthy6 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 7. 7 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 6+, this function throws an exception if the  underlying & action terminates with an exception. 67676767 Trustworthy8Synonym for monad in which  is the base monad. 9Lift an  computation. :Verbose version of > also carrying around a  detailed message. <Generic monitor failure. =Detailed message of failure. >;Exceptions thrown when some IFC restriction is about to be  violated. @&Generic can-flow-to failure, use with  : A.Insufficient privileges. Thrown when lowering , the current label or raising the clearance * cannot be accomplished with the supplied  privileges. B+Clearance would be below current label, or * object label is not above current label. C)Current label would exceed clearance, or " object label is above clearance. D'Returns the current value of the thread' s label. E=Raise the current label to the provided label, which must be . between the current label and clearance. See O. FIf the current label is oldLabel and the current clearance is   clearance:, this function allows code to raise the current label to  any value newLabel such that  oldLabel ` ` newLabel &&  newLabel ` ` clearance. G'Returns the current value of the thread' s clearance. H>Lower the current clearance. The new clerance must be between D the current label and clerance. One cannot raise the current label A or create object with labels higher than the current clearance. I4Raise the current clearance (undoing the effects of  H4) 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., 1 p cnew c must < hold. Additionally, the current label must flow to the new  clearance, i.e., l ` ` cnew must hold. JRuns 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  C/ exception is thrown. That exception can only  be caught outside a second scopeClearance that restores the - clearance to higher than the current label. K9Lowers the clearance of a computation, then restores the B clearance to its previous value (actually, to the upper bound of A the current label and previous value). Useful to wrap around a D computation if you want to be sure you can catch exceptions thrown D by it. The supplied clearance label must be bounded by the current $ label and clearance as enforced by M. $Note that if the computation inside  withClearance acquires any  9s, it may still be able to raise its clearance above the  supplied argument using I. LSame as K$, but uses privileges when applying  N to the supplied label. M?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. (If the label does not flow to clearance C is B thrown; if the current label does not flow to the argument label  B is thrown. NLike M*, 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. OUse 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 C if l' would / have to be higher than the current clearance. PLike O3, 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  O would raise it. QUse  guardWrite l+ in any (trusted) code before modifying an  object labeled l0, for which a the modification can be observed, ! i.e., the write implies a read. The implementation of  guardWrite is straight forward:  ( guardWrite l = taint l >> guardAlloc l This guarantees that l ` ` the current label (and ( clearance), and that the current label ` ` l. RLike Q*, but takes privilege argument to be more  permissive. 89:;<=>?@ABCDEFGHIJKLMNOPQR"6789:;<=>?@ABCDEFGHIJKLMNOPQR"8976DEFGHIJKL>CBA@?:;<=MNOPQR89:;<=>CBA@?DEFGHIJKLMNOPQR Trustworthy SFunction 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 M). T 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 I to raise the clearance  first if you wish to create an  at a higher label than the  current clearance. U 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 C.  However, you can use  to check if U will succeed  without throwing an exception. VExtracts the value of an  just like U, but takes a E privilege argument to minimize the amount the current label must be  raised. Function will throw C under the same  circumstances as U. W 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 N. 8 The old label must flow to the new label (again modulo " privileges), as enforced by 1. XRaises 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 M). YSame as X), 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. ZDowngrades a label. [ 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. \ 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. STUVWXYZ[\ STUVWXYZ[\ STUVWXYZ[\ STUVWXYZ[\Unsafe^ Lifts an  action in the  monad, executing a guard  before calling the function. a%This function can be used to turn an  function into an   one. The  version expects a _ argument, and before  performing any IO uses Q! to check that the current label  can write the label in the _ object.  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 (). b A variant of a" that takes a privilege argument. ]^_`ab]^_`ab_`ab]^]^_`ab  Trustworthy cAn 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. d=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 M guard. eSame as d 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. fCRead 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 O gSame as f except  readLIORefP takes a privilege object 1 which is used when the current label is raised. h@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 M guard. iSame as h 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. j@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 M guard). kSame as j 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. l'Atomically modifies the contents of an c. 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 Q, C which will raise an exception if any of the IFC conditions cannot  be satisfied. mSame as l except atomicModifyLIORefP takes C a set of privileges which are accounted for in label comparisons. cdLabel of reference Initial value Mutable reference efghijLabeled reference  Modifier klm cdefghijklm cdefghijklm cdefghijklm  TrustworthynAn LMVar+ is a labeled synchronization variable (an ) that 3 can be used by concurrent threads to communicate. oECreate 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 M if this is  not the case. pSame as o+ 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. q@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. rSame as q/ 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. sReturn contents of the n&. Note that a take consists of a read 3 and a write, since it observes whether or not the n is full, and 8 thus the current label must be the same as that of the n (of E course, this is not the case when using privileges). Hence, if the  label of the n. 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  Q8 will throw an exception if any of the IFC checks fail.  If the Finally, like MVars if the n is empty,  takeLMVar  blocks. tSame as s except  takeLMVarP takes a privilege object 1 which is used when the current label is raised. uNon-blocking version of s . It returns Nothing if the  n is empty, otherwise it returns Just value, emptying the  n. vSame as u+, but uses priviliges when raising current  label. wPuts a value into an n). Note that a put consists of a read and / a write, since it observes whether or not the n is empty, and so 3 the current label must be the same as that of the n (of course, 8 this is not the case when using privileges). As in the s  case, if the label of the n$ 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 Q throws an exception.  If the n is full, putLMVar blocks. xSame as w except  putLMVarP takes a privilege object 1 which is used when the current label is raised. yNon-blocking version of w . It returns True if the  n7 was empty and the put succeeded, otherwise it returns False. zSame as y2, but uses privileges when raising current label. {Combination of s and w. 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 w, v, or   for this n. |Same as { except  readLMVarP takes a privilege object 1 which is used when the current label is raised. }Takes a value from an n, puts a new value into the LMvar, . and returns the taken value. Like the other n operations it is  required that the label of the n 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 Q throws an H exception if this cannot be accomplished. This operation is atomic iff " there is no other thread calling w for this n. ~Same as } except  swapLMVarP takes a privilege object 1 which is used when the current label is raised. Check the status of an n!, i.e., whether it is empty. The ' function succeeds if the label of the n is below the current = clearance -- the current label is raised to the join of the n E label and the current label. Note that this function only returns a ; snapshot of the state and does not modify it -- hence the  underlying guard is O and not Q. Same as 2, but uses privileges when raising current label. no Label of LMVar New mutable location pq Label of LMVar Initial value of LMVar New mutable location rstuvwSource n  New value xyz{|}Source LMVar  New value  Taken value ~nopqrstuvwxyz{|}~nopqrstuvwxyz{|}~nopqrstuvwxyz{|}~ UnsafeHA LabeledResult encapsulates a future result from a computation running  in a thread. It holds the ThreadId and an LMVar where the result is " stored. The thread referenced in  should fill in   lresResultTCB> (either with a value or exception), so waiting on the thread ' should ensure that a result is ready. !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 .   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 M. @ Moreover, the supplied computation must not terminate with its D label above the result label; doing so will result in an exception A (whose label will reflect this observation) being thrown in the  thread reading the result. BIf an exception is thrown in the inner computation, the exception C label will be raised to the join of the result label and original  exception label.  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 Q 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's result exceeds its label  timedWait and exceeds what the E calling thread can observe, consumes the whole timeout and throws a  ?0 exception you can catch (i.e., it never raises ! the label above the clearance).  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 nopqrstuvwxyz{|}~ SafeA DCLabel$ is a pair of secrecy and integrity s. %Extract secrecy component of a label 'Extract integrity component of a label AA component is a set of clauses, i.e., a formula (conjunction of  disjunction of s). DCFalse corresponds to logical  False, while DCFormula Set.empty corresponds to logical True. &Conjunction of disjunction categories Get underlying clause-set. Logical False -A clause or disjunction category is a set of s. C Logically the set corresponds to a disjunction of the principals. Get underlying principal-set. A  Principal- is a simple string representing a source of G authority. Any piece of code can create principals, regardless of how  untrusted it is. Get the principal name. Generate a principal from a . (To create one from a  , just use the  constructor directly.) Clause constructor Logical True. Logical False. !Arbitrary formula from a clause. Is the component True. Is the component False. +dcLabel secrecyComponent integrityComponent creates a label, ! reducing each component to CNF. DLabel contstructor. Note: the components should already be reduced. @Element in the DCLabel lattice corresponding to the most secret  and least trustworthy data.  dcTop = < False, True > . AElement in the DCLabel lattice corresponding to the least secret  and most trustworthy data.  dcTop = < True, False > . =Element in the DCLabel lattice corresponding to public data.  dcPub = < True, True > '. This corresponds to data that is not  secret nor trustworthy. Logical implication. Logical conjunction Logical disjunction @Reduce component to conjunction normal form by removing clauses  implied by other. !Privileges can be combined using  'Safe Convert a type (e.g., , ) to a label component.  Convert to   Create a  from a secrecy  and integrity  . E.g.:    "secrecy" %% " integrity"    infix 5 %% Conjunction of two -based elements.   infixl 6 /\ Disjunction of two -based elements.   infixl 7 \/ @Logical falsehood can be thought of as the component containing 8 every possible principal, hence impossible to express:  impossible = dcFalse <Logical truth can be thought of as the component containing 8 no specific principal, hence imposing no restrictions:  unrestricted = dcTrue  Convert a  to a list of list of  s if the   does not have the value . In the latter case $ the function returns an exception. Convert a list of list of s to a . Each - inner list is considered to correspond to a . Convert singleton  (in the form of a )to . Convert singleton  to . Convert singleton  to .  Identity of .  SafeL #$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\ Trustworthy<A privilege is a minted and protected privilege description  (.) that may only be created by trusted code or  delegated from an existing DCPriv. AA privilege description is simply a conjunction of disjunctions. * Unlike (actually minted) privileges (see  ), privilege 0 descriptions may be created by untrusted code. >The empty privilege, or no privileges, corresponds to logical  True. AGiven a privilege and a privilege description turn the privilege E description into a privilege (i.e., mint). Such delegation succeeds C only if the supplied privilege implies the privilege description. :We say a piece of code having a privilege object (of type ) E owns a clause when the privileges allow code to bypass restrictions < imposed by the clause. This is the case if and only if the   object contains one of the  s in the . This + function can be used to make such checks.  Trustworthy %The monad for LIO computations using  as the label.  with underlying label being  Type synonym for 8. DC +.  DC Labeled cs. DC  values. Default, starting state for a  computation. The current label  is public (i.e., ) and the current clearance is top. Evaluate computation in the  monad. Evaluate computation in the  monad.  Similar to 7', but catches any exceptions thrown by  untrusted code with throwLIO. + Unsafe)The all privilege corresponds to logical False  !"#$%&'()**+,--./0123456789:;<=>?@ABCDEFGHIJKLMMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrst u v w x y z { | } ~                  ?               lio-0.10.0.0 LIO.Exception LIO.LabelLIO.TCB LIO.PrivsLIO.RunLIO.Core LIO.Labeled LIO.TCB.LObj LIO.LIORefLIO.Concurrent.LMVarLIO.TCB.ConcurrentLIO.ConcurrentLIO.DCLabel.CoreLIO.DCLabel.DSLLIO.DCLabel.Privs LIO.DCLabelLIO.TCB.DCLabelIO mapExceptionLIObase GHC.Exception SomeException fromException toException ExceptionLabelOflabelOfLabellubglb canFlowToReadTCB readsPrecTCBreadTCBShowTCBshowTCBLabeled LabeledTCBPrivPrivTCBUncatchableTCBLIOTCBunLIOTCBLIOStatelioLabel lioClearancegetLIOStateTCBputLIOStateTCBmodifyLIOStateTCBupdateLIOStateTCBioTCB makeCatchablethrowLIOcatchhandle onExceptionfinallybracketevaluatetryGateNoPrivsPrivDesccanFlowToPrivDescpartDowngradePrivDescprivDesc canFlowToPpartDowngradePnoPrivsgatecallGaterunLIOevalLIOMonadLIOliftLIOVMonitorFailuremonitorFailuremonitorMessageMonitorFailureResultExceedsLabelCanFlowToViolationInsufficientPrivsCurrentLabelViolationClearanceViolationgetLabelsetLabel setLabelP getClearance setClearance setClearancePscopeClearance withClearancewithClearanceP guardAlloc guardAllocPtainttaintP guardWrite guardWritePlabellabelPunlabelunlabelPrelabelLabeledP taintLabeled taintLabeledPuntaintLabeledPlFmaplApGuardIO guardIOTCBLObjLObjTCBblessTCB blessPTCBLIORef newLIORef newLIORefP readLIORef readLIORefP writeLIORef writeLIORefP modifyLIORef modifyLIORefPatomicModifyLIORefatomicModifyLIORefPLMVar newEmptyLMVarnewEmptyLMVarPnewLMVar newLMVarP takeLMVar takeLMVarP tryTakeLMVar tryTakeLMVarPputLMVar putLMVarP tryPutLMVar tryPutLMVarP readLMVar readLMVarP swapLMVar swapLMVarP isEmptyLMVar isEmptyLMVarP LabeledResultLabeledResultTCBlresThreadIdTCB lresLabelTCB lresBlockTCB lresStatusTCB LResStatus LResResultLResLabelTooHigh LResEmptyforkLIOlForklForkPlWaitlWaitPtrylWait trylWaitP timedlWait timedlWaitPDCLabel dcSecrecy dcIntegrity Component DCFormula unDCFormulaDCFalseClauseunClause Principal principalName principalclausedcTruedcFalse dcFormulaisTrueisFalsedcLabeldcLabelNoReducedcTopdcBottomdcPub dcImpliesdcAnddcOrdcReduce ToComponent toComponent%%/\\/ impossible unrestrictedtoListfromListDCPriv DCPrivDescnoPrivdcDelegatePrivdcOwnsDCDCStateMonadDCDCGateDCRef DCLabeled defaultStateevalDCrunDCtryDC allPrivTCB Text.ReadreadGHC.Read readsPrecGHC.ShowShowghc-prim GHC.Types$fReadTCBLabeledRead$fShowTCBLabeled$fLabelOfLabeled $fMonoidPriv$fExceptionUncatchableTCB$fShowUncatchableTCB$fApplicativeLIO $fFunctorLIO $fMonadLIO Data.EitherEitherRightLeft$fPrivDesclNoPrivsGateTCB$fMonoidNoPrivs$fMonadLIOlLIO$fExceptionVMonitorFailure$fShowVMonitorFailure$fExceptionMonitorFailureGHC.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.MVarMVar$fLabelOfLabeledResultStringbytestring-0.10.0.2Data.ByteString.Internal ByteString$fMonoidComponent Data.Monoidmappend$fLabelDCLabel$fBoundedDCLabel $fShowDCLabel$fPrivDescDCLabelComponent$fShowComponent $fShowClause $fOrdClause$fShowPrincipal$fToComponent[]$fToComponentPrincipal$fToComponentClause$fToComponentComponent$fToComponentBool$fToComponentPriv