=9      !"#$%&'()*+,-./0123456789:;<=> ? @ A B C D E F G H I J K L M N O P Q R S T U V W X Y Z [ \ ] ^ _ ` a b c d e f g h i j k l m n o p q r s t u v w x y z { | } ~        !"#$%&'()*+,-./012345678Unsafe The dual of . This class provides mintTCB which may  be used to convert, or mint", a privilege descriptions into a  privilege. Of course, mintTCB must be restricted to the TCB. ;Mint a new privilege values given a privilege description. DClass used to convert a privilege to a privilege description. This ? is particularly useful when one piece of code wishes to prove A ownership of certain privileges without granting the privilege. C NOTE: it (almost) always a security violation if the privilege is ! also the privilege description. CAlthough this class is not part of the TCB there are some security > implications that should be considered when making a type an D instance of this class. Specifically, if the value constructor for  the privilege description type d is exported then some  trusted code must be used when "proving" ownership of a certain E privilege. This is generally a good idea even if the constructor is D not made available, since code can (usually) cache such privilege C descriptions. An alternative is to use phantom types to enforce a  linear-type-like behavior. 0Retrive privilege description from a privilege. :Zero-method class that imposes a restriction on what code  (namely trusted) can make a "privilege type". 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   (in literature, written as "), a top element  (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  "). ;Bottom, or minimum, element. It must be that for any label L,   `` L. 8Top, or maximum, element. It must be that for any label L,  L `` . Least9 upper bound, or join, of two labels. For any two labels  L_1 and L_2 , such that  L_3 = L_1 `` 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 , such that  L_3 = L_1 `` 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 `` 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 `` L_1 for any L_1.  Antisymmetry: If L_1 `` L_2 and  L_2 `` L_1 then  L_1 = L_2.  Transitivity: If L_1 `` L_2 and  L_2 `` L_3 then L_1 `` L_3. A more meaningful name for . Note that since the name  does not imply least# upper bound it is not a method of . A more meaningful name for . Note that since the name  does not imply greatest# lower bound it is not a method of  .    Trustworthy>Generic privilege type used to denote the lack of privileges. !?This class defines privileges and the more-permissive relation  ("7) on labels using privileges. Additionally, it defines  #3 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 " 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  " p L_1 L_2 for all p, but for some labels and  privileges, " 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. 9With lack of privileges, " is simply , and  # is the least .  !"# Privileges  Label from which data must flow  Goal label Result 9:;<= !"#!"#  !"#9:;<=Safe$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. %@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 $%&$%&$>?%&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 A) are implemented. (Trusted A )Trusted @ *AIt would be a security issue to make certain objects a member of  the B3 class, but nonetheless it is useful to be able to + examine such objects when debugging. The + method can be used  to examine such objects. ,DA labeled exception is simply an exception associated with a label. .Synonym for monad in which 0 is the base monad. /Lift an 0 computation. 0The LIO monad is a state monad, with C as the underlying monad,  that carries along a  current label (5) and current clearance  (6-). 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. 3Internal state of an 0 computation. 5Current label. 6Current clearance. 7>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. 8Set internal state. 9/Update the internal state given some function. :<Throw an arbitrary exception. Note that the exception being  thrown is not labeled. ;?Catch an exception. Note that all exceptions thrown by LIO are B labeled and thus this trusted function can be used to handle any D exception. Note that the label of the exception must be considered @ in the handler (i.e., handler must raise the current label) to  preserve security. < Lifts an C computation into the 0 monad. Note that  exceptions thrown within the C computation cannot directly be  caught within the 00 computation. Thus, you will generally want to  use rtioTCB exported by LIO.Exception.TCB instead of <. = Lifts an C computation into the 0 monad. If the C C computation throws an exception, it labels the exception with the 8 current label so that the exception can be caught with catchLIO. '()*+,-./0123456789:;<=DE'()*+,-./0123456789:;<=012./3456789,-:;<=*+'()'()*+,-./0123456789:;<=DE  Trustworthy$>Verbose version of B also carrying around a  detailed message. @Generic monitor failure. ADetailed message of failure. B;Exceptions thrown when some IFC restriction is about to be  violated. C&Generic can-flow-to failure, use with  > D.Insufficient privileges. Thrown when lowering , the current label or raising the clearance * cannot be accomplished with the supplied  privileges. E+Clearance would be below current label, or * object label is not above current label. F)Current label would exceed clearance, or " object label is above clearance. G Given an 0/ computation and some initial state, return an = IO action which when executed will perform the IFC-safe LIO  computation. &Because untrusted code cannot execute C 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 C computations, but it cannot  execute them.) H Execute an 0$ action, returning the final state.  See G. I Similar to G(, but catches all exceptions, including  language level exceptions. J Similar to G(, but catches all exceptions exceptions  thrown with S. K'Returns the current value of the thread' s label. L=Raise the current label to the provided label, which must be . between the current label and clearance. See _. MIf 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. N'Returns the current value of the thread' s clearance. O>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. P4Raise the current clearance (undoing the effects of  O4) 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 must < hold. Additionally, the current label must flow to the new  clearance, i.e., l `` cnew must hold. QJLowers the clearance of a computation, then restores the clearance to its P previous value (actually, to the upper bound of the current label and previous M value). Useful to wrap around a computation if you want to be sure you can P catch exceptions thrown by it. The supplied clearance label must be bounded by 0 the current label and clearance as enforced by ]. $Note that if the computation inside  withClearance acquires any  !9s, it may still be able to raise its clearance above the  supplied argument using P. RSame as Q$, but uses privileges when applying  ^ to the supplied label. S>Throw an exception. The label on the exception is the current  label. TSame as U. but does not use privileges when raising the E current label to the join of the current label and exception label. UBCatches an exception, so long as the label at the point where the 9 exception was thrown can flow to the clearance at which catchLIO is E invoked. Note that the handler raises the current label to the join  (,) of the current label and exception label. V@Performs an action only if there was an exception raised by the B computation. Note that the exception is rethrown after the final  computation is executed. WPrivileged version of W. V cannot run its C handler if the label was raised in the computation that threw the E exception. This variant allows privileges to be supplied, so as to  catch exceptions thrown with a "higher" label. XAExecute a computation and a finalizer, which is executed even if 2 an exception is raised in the first computation. Y Version of X$ that uses privileges when handling - exceptions thrown in the first computation. ZThe bracket2 function is used in patterns where you acquire a G resource, perform a computation on it, and then release the resource. F The function releases the resource even if an exception is raised in ? the computation. An example of its use case is file handling:   bracket $ (openFile ... {- open file -} ) # (\handle -> {- close file -} ) - (\handle -> {- computation on handle -}) Note: bracket does not use F! and thus asynchronous may leave D the resource unreleased if the thread is killed in during release. F An interface for arbitrarily killing threads is not provided by LIO. [Like Z4, but uses privileges to downgrade the label of any  raised exception. \FForces its argument to be evaluated to weak head normal form when the A resultant LIO action is executed. This is simply a wrapper for  Control.Exception's evaluate. ]?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 F is B thrown; if the current label does not flow to the argument label  E is thrown. ^Like ]*, 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. _Use 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 F if l' would / have to be higher than the current clearance. `Like _3, 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  _ would raise it. aUse  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. bLike a*, but takes privilege argument to be more  permissive. (>?@ABCDEFGLIO computation Initial state H,LIO computation that may throw an exception Initial state I,LIO computation that may throw an exception Initial state J,LIO computation that may throw an exception Initial state KLMNOPQRSTUVThe computation to run  Computation to run on exception Result if no exception thrown W"Privileges to downgrade exception The computation to run  Computation to run on exception Result if no exception thrown XThe computation to run firstly 7Final computation to run (even if exception is thrown) Result of first action Y"Privileges to downgrade exception The computation to run firstly 7Final computation to run (even if exception is thrown) Result of first action ZComputation to run first Computation to run last Computation to run in-between [Priviliges used to downgrade Computation to run first Computation to run last Computation to run in-between \]^_`abGHI-,./03456>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`ab-0./GHJI3456KLMNOPQR,SUTVWXYZ[\BFEDC>?@A]^_`ab!>?@ABFEDCGHIJKLMNOPQRSTUVWXYZ[\]^_`abGHI Unsafec 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 c  is an instance of ), which effectively means that the label  of a c0 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.) e Label of c valued fExtracts the value from an  c, discarding the label and any  protection. g1Trusted constructor that creates labeled values. JTrusted K instance. LTrusted B instance. cdefgJLcdefgcdefgcdefgJL  Trustworthy hDIFC-aware functor instance. Since certain label formats may contain B integrity information, this is provided as a class rather than a G function. Such label formats will likely wish to drop endorsements in  the new labeled valued. iM6-like funciton that is aware of the current label and  clearance. jFunction to construct a c" 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 ]). k Constructs a c using privilege to allow the c'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 P to raise the clearance  first if you wish to create an c at a higher label than the  current clearance. l Within the 0 monad, this function takes a c and returns % the underlying value. Thus, in the 0 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 F.  However, you can use  to check if l will succeed  without throwing an exception. mExtracts the value of an c just like l, but takes a E privilege argument to minimize the amount the current label must be  raised. Function will throw F under the same  circumstances as l. n Relabels a c* value to the supplied label if the given ? privilege privileges permits it. It must be that the original C label and new label are equal, modulo the supplied privileges. In = other words the label remains in the same congruence class.  Consequently relabelP p l lv throws an D  exception if  " p l ( lv) && " p ( lv) ldoes not hold. oRaises the label of a c to the  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 c$ is already above the current thread's clearance. If ( the supplied label is not bounded then  taintLabeled will throw an  exception (see ]). pSame as o), 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. qDowngrades the label of a c as much as possible given the  current privilege. rSame as q' but uses the supplied privileges when - downgrading the label of the labeled value. NReturns label of a c type. hijklmnopqrN chijklmnopqr cjklmnopqrhi hijklmnopqrN Unsafe sAn LMVar+ is a labeled synchronization variable (an O) that 3 can be used by concurrent threads to communicate. uLabel of MVar. vAccess the underlying O, ignoring IFC. w)Trusted function used to create an empty LMVar, ignoring IFC. x#Trusted function used to create an LMVar with the supplied  value, ignoring IFC. yRead the contents of an s, ignoring IFC. zSame as  tryTakeLMVar, but ignorses IFC. {Put a value into an s, ignoring IFC. |Same as  tryPutLMVar, but ignorses IFC. }0Trusted function used to read (take and put) an s, ignoring IFC. ~%Trusted function that swaps value of s, ignoring IFC. Same as  isEmptyLMVar, but ignorses IFC. stuvwxyz{|}~P stuvwxyz{|}~ stuvwxyz{|}~ stuvwxyz{|}~P  TrustworthyECreate 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 ] 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 s&. Note that a take consists of a read 3 and a write, since it observes whether or not the s is full, and 8 thus the current label must be the same as that of the s (of E course, this is not the case when using privileges). Hence, if the  label of the s. 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  a8 will throw an exception if any of the IFC checks fail.  If the Finally, like MVars if the s 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  s is empty, otherwise it returns Just value, emptying the  s. Same as +, but uses priviliges when raising current  label. Puts a value into an s). Note that a put consists of a read and / a write, since it observes whether or not the s is empty, and so 3 the current label must be the same as that of the s (of course, 8 this is not the case when using privileges). As in the   case, if the label of the s$ 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 a throws an exception.  If the s 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  s7 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 just  put it back. As specified for readMVar, this operation is atomic & iff there is no other thread calling  for this s. Same as  except  readLMVarP takes a privilege object 1 which is used when the current label is raised. Takes a value from an s, puts a new value into the LMvar, . and returns the taken value. Like the other s operations it is  required that the label of the s 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 a throws an H exception if this cannot be accomplished. This operation is atomic iff " there is no other thread calling  for this s. Same as  except  swapLMVarP takes a privilege object 1 which is used when the current label is raised. Check the status of an s!, 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 s 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 _ and not a. 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 s  New value Source LMVar  New value  Taken value ssUnsafe2A labeled thread result is simply a wrapper for a s . A thread H can observe the result of another thread, only after raising its label  to the label of the result. !Thread executing the computation  Plecement of computation result QQ Trustworthy Get the  of the calling thread.  Execute an 0. computation in a new lightweight thread. The  * of the newly created thread is returned. 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. lFork> takes a label, which corresponds to the label of the result. E It is require that this label is above the current label, and below 5 the current clearance as enforced by the underlying ]. @ Moreover, the supplied computation must not read anything more G sensitive (i.e., with a label above the supplied label) --- doing so < will result in an exception (whose label will reflect this  observation) being thrown. 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 a 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. ;Suspend current thread for a given number of microseconds. Though in most cases using a  is sufficient, in 5 certain scenarios it is desirable to produce a pure c value G that is the result of other potentially sensitive values. As such, we  provide lBracket. lBracket is like , but rather than returning a  , it returns a c value. The key difference  between the two is that lBracket takes an additional parameter H specifying the number of microseconds the inner computation will take.  As such, lBracket/ will block for the specified duration and the $ result of the inner computation be forced. That is, if the  computation terminated cleanly, i.e., it did not throw an 7 exception and it finished in the time specified, then R the  result is returned, otherwise S is returned. CNote that the original LIO (before version 0.9) included a similar  " primitive" called  toLabeled. We have chosen to call this  lBracket6 in part because it is a more descriptive name and to # avoid confusion with the previous  toLabeled where time was not  considered. Same as +, but uses privileges when forking the new  thread. Label of result *Computation to execute in separate thread Labeled result Label of result (Duration of computation in microseconds *Computation to execute in separate thread Labeled result  Privileges Label of result (Duration of computation in microseconds *Computation to execute in separate thread Labeled result  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. Principal constructor. Clause constructor Logical True. Logical False. !Arbitrary formula from a clause. Is the component True. Is the component False. @Label constructor. Note that each component is first reduced to  CNF. DLabel contstructor. Note: the components should already be reduced. =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. #TUVWXYZTUVWXYZ Trustworthy[<Serialize labels by converting them to pairs of components. \0Serialize components by converting them to maybe's [\[\Unsafe<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 all privilege corresponds to logical False ]^_]^_Unsafe Label of file path "Unlabel a filepath, ignoring IFC. Filesystem errors Supplied file name is illegal. Object label is corrupt. +FSobjectcannot be created without a label. #Cannot create root, missing label. Root does not exists. Root already exists. $Root is invalid (must be absolute). Root structure is corrupt. "Constraintfor serializable labels `Synonym for lazy ByteString aSynonym for strict ByteString bContent written to magic key. cRoot of labeled filesystem. Get the root directory. ACreate a the file store (i.e., labeled file system) with a given ? label and root file path. The path must be an absolute path,  otherwise  initFSTCB throws . ESet the given file path as the root of the labeled filesystem. This  function throws a % if the directory does not contain a  valid label, and a  if the d attribute is  missing. CInitialize filesystem at the given path. The supplied path must be  absolute, otherwise  initFSTCB throw . If the FS has  already been created then  initFSTCB solely verifies that the root  directory is not corrupt (see "). Otherwise, a new FS is created  with the supplied label (see ). +This function performs several checks that  and  perform, A so when considering performance they should be called directly. eLabel attribute name. fHash-of-label attribute name. (Encode a label into an attribute value. (Encode a label into an attribute value. 'Descode label from an attribute value. 6Set the label of a given path. This function sets the e 1 attribute to the encoded label, and the hash to f. >Get the label of a given path. If the object does not have an C associated label or the hash of the label and stored-hash are not  equal, this function throws . 0Create a directory object with the given label. ACreate a file object with the given label and return a handle to  the new file. g.Convert lazy ByteString to strict ByteString. h.Convert strict ByteString to lazy ByteString. i*Compress with zlib (optimized for speed). %`adbcPath to the filesystem root Label of root efghijk`adbcefghijkSafeM !"#$%&,./03456>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abchijklmnopqrUnsafe 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 c to get a limited form of  flow-sensitivity. Label of the labeled l. Access the underlying l, ignoring IFC. =Trusted constructor that creates labeled references with the % given label without any IFC checks. ?Trusted function used to read the value of a reference without  raising the current label. :Trusted function used to write a new value into a labeled  reference, ignoring IFC. 1Trusted function that mutates the contents on an ,  ignoring IFC. =Trusted function used to atomically modify the contents of a " labeled reference, ignoring IFC. mGet the label of an . m m Trustworthy =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 ] 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 _ 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 ] 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 ] 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 a, 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  Trustworthy0Get the current UTC time from the system clock. -Get the local time together with a TimeZone. .Convert UTC time to local time with TimeZone. Pnopqrstuvwxyz{|}~ Trustworthy>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. !Privileges can be combined using  SafeConvert a type (e.g., , ) to a label component.  Convert to  Trivial synonym for . Convert to a . Conjunction of two -based elements.   infixl 6 /\ Disjunction of two -based elements.   infixl 7 \/ @Logical falsehood can be thought of as the component containing  every possible principal:  everybody = dcFalse <Logical truth can be thought of as the component containing  no specific principal:  anybody = dcTrue  Convert a  to a list of list of  s if the   does not have the value . In the latter case  the function returns S. 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  (in the form of a  ByteString)to . Convert singleton  to . Convert singleton  to .  Identity of .   Trustworthy %The monad for LIO computations using  as the label. 3 with underlying label being  Type synonym for .. DC $.  DC Labeled s. DC c values. DC Labeled exceptions. Default, starting state for a  computation. The current label  is public (i.e., ) and the current clearance is . Evaluate computation in the  monad. Evaluate computation in the  monad.  Similar to G', but catches any exceptions thrown by  untrusted code with S.  Similar to G, but catches all exceptions. *  Trustworthy, @Class used to abstract reading and writing from and to handles,  respectively.  Serialize . Same as G&, but takes two additional parameters C corresponding to the path of the labeled filesystem store and the D label of the root. If the labeled filesystem store does not exist, > it is created at the specified path with the root having the  supplied label. F If the filesystem does exist, the supplied label is ignored and thus A unnecessary. However, if the root label is not provided and the ( filesystem has not been initialized, a  exception  will be thrown. DGet the contents of a directory. The current label is raised to the H join of the current label and that of all the directories traversed to < the leaf directory. Note that, unlike the standard Haskell  0, we first normalise the path by collapsing all  the ..'s. The function uses unlabelFilePath when raising the C current label and thus may throw an exception if the clearance is  too low.  Note:4 The current LIO filesystem does not support links. Same as #, but uses privileges when raising  the current label. CCreate a directory at the supplied path with the given label. The H given label must be bounded by the the current label and clearance, as  checked by ]+. The current label (after traversing the D filesystem to the directory path) must flow to the supplied label, ? which must, in turn, flow to the current label as required by  a. Same as ', but uses privileges when raising the . current label and checking IFC restrictions. <Given a set of privileges, a (maybe) new label of a file, a H filepath, and the IO mode, open (and possibly create) the file. If the H file exists, the supplied label is not necessary; otherwise it must be E supplied. The current label is raised to reflect all the traversed D directories. Additionally the label of the file (new or existing) @ must be between the current label and clearance, as imposed by  ]:. If the file is created, it is further required that the F current computation be able to write to the containing directory, as  imposed by a. Same as &, but uses privileges when traversing ( directories and performing IFC checks. >Close a file handle. Must be able to write to the the labeled  handle, as checkd by a. Close a labeled file handle. >Flush a file handle. Must be able to write to the the labeled  handle, as checkd by a. Flush a labeled file handle. Read n6 bytes from the labeled handle, using privileges when , performing label comparisons and tainting. Same as 0, but will not block waiting for data to become < available. Instead, it returns whatever data is available. ? Privileges are used in the label comparisons and when raising  the current label.  >Read the entire labeled handle contents and close handle upon  reading EOF0. Privileges are used in the label comparisons % and when raising the current label. !'Read the a line from a labeled handle. "?Output the given (Byte)String to the specified labeled handle. ? Privileges are used in the label comparisons and when raising  the current label. # Synonym for ". $>Output the given (Byte)String with an appended newline to the < specified labeled handle. Privileges are used in the label 1 comparisons and when raising the current label. %CReads a file and returns the contents of the file as a ByteString. &Same as %) but uses privilege in opening the file. 'BWrite a ByteString to the given filepath with the supplied label. (Same as '. but uses privilege when opening, writing and  closing the file. )Set the buffering mode *Set the buffering mode +Get the buffering mode ,Get the buffering mode -Select binary mode () or text mode () .Select binary mode () or text mode () / End of file. 0 End of file. 1FIs handle open. 2FIs handle open. 3FIs handle closed. 4FIs handle closed. 5FIs handle readable. 6FIs handle readable. 7FIs handle writable. 8FIs handle writable. BGiven a pathname to a labeled filesystem object, traverse all the A directories up to the object, while correspondingly raising the G current label. Note that if the object or a parent-directory does not H exist, an exception will be thrown; the label of the exception will be @ the join of all the directory labels up to the lookup failure. Note:3 this function cleans up the path before doing the  lookup, so e.g., path foobar ..@ will first be rewritten to @foo  and thus no traversal to bar'. Note that this is a more permissive # behavior than forcing the read of .. from bar.   taintObjPath returns this cleaned up path. "Take a list of directories (e.g., ["a","b","c"] ) and return " all the subtrees up to the node (["a","ab\",\"ab/c"]).  Remove any !s from the front of a file path. -Cleanup a file path, if it starts out with a .., we consider this G invalid as it can be used explore parts of the filesystem that should 5 otherwise be unaccessible. Similarly, we remove any . from the path. 7     Filesystem root Label of root  LIO action Initial state  Privilege  Directory  Privilege Label of new directory Path of directory Label of file if created  File to open Mode  Privileges Label of file if created  File to open Mode  Privileges Labeled handle Number of bytes to read  !"#$%&'()*+,-./012345678 Privilege Path to object ;       !"#$%&'()*+,-./012345678;         !"#$%&'()*+,-./0123456780      !"#$%&'()*+,-./012345678 !"#$%&'()(*(+(,(-./0123456789:;<==>?@ABCDEFGHIJKLMNOOPQRSTUVWX Y Y Z [ \ ] ^ _ ` a b c d e f g h i j k l m n o p q r s t u v w x y z { | } ~           !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTAUVWXYZ[\]^_`ab c d e fXg hij klm nopqprstuvwxyz{|}~sis\]\] lio-0.9.1.2 LIO.HandleLIO.Concurrent.TCBLIO.Concurrent LIO.Privs.TCB LIO.Label LIO.PrivsLIO.GateLIO.TCBLIO.CoreLIO.Labeled.TCB LIO.LabeledLIO.Concurrent.LMVar.TCBLIO.Concurrent.LMVarLIO.DCLabel.CoreLIO.DCLabel.Privs.TCB LIO.FS.TCBLIO.LIORef.TCB LIO.LIORef LIO.Data.TimeLIO.DCLabel.PrivsLIO.DCLabel.DSL LIO.DCLabelLIO.DCLabel.SerializeLIObaseGHC.IO.Handle.TypesHandle GHC.Conc.SyncThreadIdGHC.IO.Exception StackOverflow HeapOverflow ThreadKilled UserInterruptAsyncException NoBuffering LineBufferingBlockBuffering BufferMode GHC.IO.IOModeReadMode WriteMode AppendMode ReadWriteModeIOModeMintTCBmintTCBPrivDescprivDescPrivTCBLabelOflabelOfLabelbottomtoplubglb canFlowTo upperBound lowerBoundNoPrivsPriv canFlowToPpartDowngradePGategatecallGateReadTCB readsPrecTCBreadTCBShowTCBshowTCBLabeledExceptionLabeledExceptionTCBMonadLIOliftLIOLIOTCBunLIOTCBLIOStatelioLabel lioClearancegetLIOStateTCBputLIOStateTCBupdateLIOStateTCBunlabeledThrowTCBcatchTCBioTCB rethrowIoTCBVMonitorFailuremonitorFailuremonitorMessageMonitorFailureCanFlowToViolationInsufficientPrivsCurrentLabelViolationClearanceViolationevalLIOrunLIO paranoidLIOtryLIOgetLabelsetLabel setLabelP getClearance setClearance setClearanceP withClearancewithClearancePthrowLIO catchLIOPcatchLIO onException onExceptionPfinallyfinallyPbracketbracketPevaluate guardAlloc guardAllocPtainttaintP guardWrite guardWritePLabeled LabeledTCBlabelOfLabeled unlabelTCBlabelTCBLabeledFunctorlFmaplabellabelPunlabelunlabelPrelabelLabeledP taintLabeled taintLabeledPuntaintLabeleduntaintLabeledPLMVarLMVarTCB labelOfLMVarunlabelLMVarTCBnewEmptyLMVarTCB newLMVarTCB takeLMVarTCBtryTakeLMVarTCB putLMVarTCBtryPutLMVarTCB readLMVarTCB swapLMVarTCBisEmptyLMVarTCB newEmptyLMVarnewEmptyLMVarPnewLMVar newLMVarP takeLMVar takeLMVarP tryTakeLMVar tryTakeLMVarPputLMVar putLMVarP tryPutLMVar tryPutLMVarP readLMVar readLMVarP swapLMVar swapLMVarP isEmptyLMVar isEmptyLMVarP LabeledResultLabeledResultTCBlresThreadIdTCB lresResultTCB myThreadIdforkLIOlForklForkPlWaitlWaitPtrylWait trylWaitP threadDelaylBracket lBracketPDCLabel dcSecrecy dcIntegrity Component DCFormula unDCFormulaDCFalseClauseunClause Principal principalName principalclausedcTruedcFalse dcFormulaisTrueisFalsedcLabeldcLabelNoReducedcPub dcImpliesdcAnddcOrdcReduceDCPriv DCPrivTCBunDCPriv DCPrivDesc allPrivTCB LFilePath LFilePathTCBlabelOfFilePathunlabelFilePathTCBFSErrorFSIllegalFileNameFSLabelCorruptFSObjNeedLabelFSRootNeedLabel FSRootNoExist FSRootExists FSRootInvalid FSRootCorruptSLabel getRootDirTCBmkFSTCBsetFSTCB initFSTCBlazyEncodeLabel encodeLabel decodeLabelsetPathLabelTCBgetPathLabelTCBcreateDirectoryTCB createFileTCBLIORef LIORefTCB labelOfLIORefunlabelLIORefTCB newLIORefTCB readLIORefTCBwriteLIORefTCBmodifyLIORefTCBatomicModifyLIORefTCB newLIORef newLIORefP readLIORef readLIORefP writeLIORef writeLIORefP modifyLIORef modifyLIORefPatomicModifyLIORefatomicModifyLIORefPgetCurrentTime getZonedTimeutcToLocalZonedTimenoPrivdcDelegatePrivdcOwns ToComponent toComponent dcPrivDesc/\\/ everybodyanybodytoListfromListDCDCStateMonadDCDCGateDCRef DCLabeledDCLabeledException defaultStateevalDCrunDCtryDC paranoidDC HandleOpshGethGetNonBlocking hGetContentshGetLinehPuthPutStr hPutStrLn LabeledHandle SMonadLIOevalWithRootFSgetDirectoryContentsgetDirectoryContentsPcreateDirectorycreateDirectoryPopenFile openFilePhClosehClosePhFlushhFlushPhGetPhGetNonBlockingP hGetContentsP hGetLinePhPutPhPutStrP hPutStrLnPreadFile readFileP writeFile writeFileP hSetBufferinghSetBufferingP hGetBufferinghGetBufferingPhSetBinaryModehSetBinaryModePhIsEOFhIsEOFPhIsOpenhIsOpenP hIsClosed hIsClosedP hIsReadable hIsReadableP hIsWritable hIsWritableP$fPrivlNoPrivs$fMonoidNoPrivs$fMintTCBNoPrivsNoPrivs$fPrivDescNoPrivsNoPrivs$fPrivTCBNoPrivsunGate Text.ReadreadGHC.Read readsPrecGHC.ShowShowghc-prim GHC.TypesIO$fExceptionLabeledException$fMonadLIOlLIOGHC.IOmask$fExceptionVMonitorFailure$fShowVMonitorFailure$fExceptionMonitorFailure$fReadTCBLabeledRead$fShowTCBLabeledGHC.Basefmap$fLabelOfLabeledGHC.MVarMVar$fLabelOfLMVar$fLabelOfLabeledResult Data.MaybeJustNothingS8$fLabelDCLabel $fShowDCLabel$fShowComponent $fShowClause $fOrdClause$fShowPrincipal$fSerializeDCLabel$fSerializeComponent$fMintTCBDCPrivComponent$fPrivDescDCPrivComponent$fPrivTCBDCPrivL8 magicContentrootDir magicAttr labelAttr labelHashAttr strictifylazyfycompress $fShowFSError$fExceptionFSError GHC.IORefIORef$fLabelOfLIORef time-1.4.0.1Data.Time.Format formatTimeformatCharacter FormatTimeData.Time.Format.Parse readsTimereadTime parseTime buildTime ParseTimeData.Time.LocalTime.LocalTimezonedTimeToUTCutcToZonedTimelocalTimeToUT1ut1ToLocalTimelocalTimeToUTCutcToLocalTimelocalTimeOfDaylocalDay LocalTime zonedTimeZonezonedTimeToLocalTime ZonedTimeData.Time.LocalTime.TimeOfDaytimeOfDayToDayFractiondayFractionToTimeOfDaytimeOfDayToTimetimeToTimeOfDaylocalToUTCTimeOfDayutcToLocalTimeOfDaymakeTimeOfDayValidmiddaymidnighttodSectodMintodHour TimeOfDayData.Time.LocalTime.TimeZonegetCurrentTimeZone getTimeZoneutctimeZoneOffsetStringtimeZoneOffsetString'hoursToTimeZoneminutesToTimeZone timeZoneNametimeZoneSummerOnlytimeZoneMinutesTimeZoneData.Time.Clock.UTCDiff diffUTCTime addUTCTimeData.Time.Clock.UTC utctDayTimeutctDayUTCTimeNominalDiffTimeData.Time.Calendar.GregorianaddGregorianYearsRollOveraddGregorianYearsClipaddGregorianMonthsRollOveraddGregorianMonthsClipgregorianMonthLength showGregorianfromGregorianValid fromGregorian toGregorianData.Time.Calendar.OrdinalDate isLeapYearData.Time.Calendar.DaysdiffDaysaddDaystoModifiedJulianDayModifiedJulianDayDayData.Time.Calendar.PrivateNumericPadOptionData.Time.Clock.ScalepicosecondsToDiffTimesecondsToDiffTimegetModJulianDate ModJulianDate UniversalTimeDiffTime$fMonoidDCPriv Data.Monoidmappend$fPrivDCLabelDCPriv$fToComponent[]String$fToComponentByteString$fToComponentPrincipal$fToComponentClause$fToComponentComponent$fLabeledFunctorDCLabelTrueFalse taintObjPathP allSubDirs stripSlashfilepath-1.3.0.1System.FilePath.Posix pathSeparator cleanUpPath$fHandleOpsLabeledbLIO$fHandleOpsHandleByteStringIO$fHandleOpsHandleByteStringIO0