{t}C      !"#$%&'()*+,-./0123456789:;<=>?@ABUnsafe'GClass used to convert list of principals to a disjunction category and  vice versa.  We say a  6 privilege object owns a category when the privileges H allow code to bypass restrictions implied by the category. This is the  case if and only if the   object contains one of the  s  in the #(. This class is used to check ownership DChecks if category restriction can be bypassed given the privilege. IClass used for checking if a computation can use a privilege in place of . the other. This notion is similar to the DLM " can-act-for". ,Can use first privilege in place of second. Class extending ), by allowing for the more relaxed label  comparison  canflowto_p. Relaxed partial-order relation 9Untrusted privileged object, which can be converted to a   with  -. >Privilege object is just a conjunction of disjunctions, i.e., . M A trusted privileged object must be introduced by trusted code, after which : trusted privileged objects can be created by delegation. LPrincipal is a simple string representing a source of authority. Any piece L of code can create principals, regarless of how untrusted it is. However, C for principals to be used in integrity components or be ignoerd a  corresponding privilege ( ') must be created (by trusted code) or  delegated. A DCLabel: is a pair of secrecy and integrity category sets, i.e.,  a pair of s. Integrity category set. Secrecy category set. GClass used to reduce labels and components to unique label normal form K (LNF), which corresponds to conjunctive normal form of principals. We use 8 this class to overload the reduce function used by the ,  , etc. 5A components is a conjunction of disjunctions, where MkComponentAll is 5 the constructor that is associated with the logical False. -Labels form a partial order according to the " relation. 2 Specifically, this means that for any two labels L_1 and L_2 there is a  unique label  L_3 = L_1 " L_2, known as the join , such that  L_1 " L_3 and L_2 " L_3&. Similarly, there is a unique label  L_3' = L_1 " L_2, known as the meet , such that  L_3 " L_1 and L_3 " L_2. This class defines a bounded 7 lattice, which further requires the definition of the bottom " and  top "$ elements of the lattice, such that " " L and  L " " for any label L. 6A category set, i.e., a conjunction of disjunctions.  The empty list '[]': corresponds to the single disjunction of all principals.  In other words, conceptually, [] = {[P_1 " P_2 " ...]}  Logically '[]' = True. #"A category, i.e., disjunction, of  s.  The empty list '[]'3 corresponds to the disjunction of all principals.  Conceptually, [] = [P_1 " P_2 " ...] &;A component without any disjunctions or conjunctions. This @ component, conceptually corresponds to the label consisting of A a single category containing all principals. Conceptually (in a  closed-world system),  emptyComponent = <{[P_1 " P_2 " ...]}>. - Logically, of course, this is equivalent to True. ' The dual of &, ' consists of the conjunction of C all possible disjunctions, i.e., it is the label that implies all 8 other labels. Conceptually (in a closed-world system),  allComponent = <{[P_1] " [P_2] " ...}> - Logically, of course, this is equivalent to False. (HGiven two components, take the union of the disjunctions, i.e., simply  perform an "and"4. Note the new component is not necessarily in LNF. )!Given two components, perform an "or". 8 Note that the new component is not necessarily in LNF. *@Determines if a component logically implies another component.  In other words, d_1 " ... " d_n => d_1' " ... " d_n'.  Properties:  " X, ' `*` X := True  " X"`', X `*` ' := False  " X, X `*` & := True  " X"`&, & `*` X := False +DRemoves any duplicate principals from categories, and any duplicate J categories from the component. To return a clean component, it sorts the + component and removes empty disjunctions. ,'Generates a principal from an string. -Given trusted privilege and a "desired" untrusted privilege, = return a trusted version of the untrusted privilege, if the * provided (trusted) privilege implies it. .1Privilege object corresponding to no privileges. /&Privilege object corresponding to the "root", or all privileges. N Any other privilege may be delegated using this privilege object and it must / therefore not be exported to untrusted code. 0?This function creates any privilege object given an untrusted  privilege  1. Note that this function should not be exported  to untrusted code. 10Given a list of categories, return a component. 2/Given a component return a list of categories. CTo/from  ByteStrings and #unction categories. DTo/from Es and #unction categories. FTo/from  s and #unction categories. GTCBPriv is an instance of H. I Elements of  form a bounded lattice, where:  " = <&, '> " = <', &>  <S_1, I_1> " <S_2, I_2> = <S_1 " S_2, I_1 " I_2>  <S_1, I_1> " <S_2, I_2> = <S_1 " S_2, I_1 " I_2>  <S_1, I_1> " <S_2, I_2> = S_2 => S_1 " I_1 => I_2JEach = can be reduced a unique label representation in LNF, using  the  function. K Reduce a  to LNF.  First it applies cleanComponent to remove duplicate principals 2 and categories. Following, it removes extraneous/ redundant E categories. A category is said to be extraneous if there is another , category in the component that implies it. L"Components have a unique LNF (see  ) form, and equality testing is " perfomed on labels of this form. GGiven list return category. Given category return list.  Bottom of lattice, " Top of lattice, " Join of two elements, " Meet of two elements, " Partial order relation, " !"#$%&'()*+,-./01Given list return category. 2Given category return list. MNOPQCDFRSTUVWGXIJKL3  !"#$%&'()*+,-./0123#$% !"&' , ./-0()+*12.   !"#$%&'()*+,-./012MNOPQCDFRSTUVWGXIJKL Trustworthy3Class used to create  s and  s. 4 Given element create privilege. 5KGiven privilege and new element, create (maybe) trusted privileged object. :#Empty component (logically this is True). ;!All component (logically this is False). YInstances using disjunctions. Z+Instances using strings and not principals +3456!Given two elements create label. 7&Given two elements it joins them with " 8&Given two elements it joins them with " 9Creates a singleton component. :;[\]^_`abcdefghijYklZmnopqrstuvwxyz 3456789:; 87:;96345%345:;[\]^_`abcdefghijYklZmnopqrstuvwxyz Safe-Infered<  !"#$%&'()*+,-./0123456789:; Trustworthy<A secrecy-only DC label. <={|}<=<=<={|} Trustworthy>An integrity-only DC label. >?~>?>?>?~ Trustworthy@Class used to create a  type of DCLabel-related types B Render a @ type to a string. @A Convert to . B@AB@AB @AB Trustworthy*  !"#$%,-.123456789:;+#$% !" ,91287:;6 -345.      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQMRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ dclabel-0.0.5 DCLabel.CoreDCLabel.NanoEDSLDCLabel.SecrecyDCLabel.IntegrityDCLabel.PrettyShow DCLabel.TCB DCLabel.SafeDisjToFromList listToDisj disjToListOwnsowns CanDelegate canDelegateRelaxedLattice canflowto_pPrivTCBPriv MkTCBPrivpriv Principal MkPrincipalnameDCLabel MkDCLabelsecrecy integrityToLNFtoLNF Component MkComponent componentMkComponentAllLatticebottomtopjoinmeet canflowtoConjMkConjconjDisjMkDisjdisjemptyComponent allComponent and_component or_componentimpliescleanComponent principal delegatePrivnoPriv rootPrivTCB createPrivTCBlistToComponentcomponentToListNewPrivnewPriv newTCBPrivnewDC./\..\/. singleton<>><SLabelMkSLabelILabelMkILabel PrettyShowpShow prettyShow$fDisjToFromListByteString$fDisjToFromList[]baseGHC.BaseString$fDisjToFromListPrincipal$fMonoidTCBPriv Data.MonoidMonoid$fLatticeDCLabel$fToLNFDCLabel$fToLNFComponent $fEqComponent$fSerializeDCLabel$fSerializeComponent$fSerializeConj$fSerializeDisj$fSerializePrincipal$fOwnsComponent $fOwnsDisj$fCanDelegateTCBPrivTCBPriv$fCanDelegateTCBPrivComponent$fCanDelegateComponentTCBPriv$fCanDelegateComponentComponent$fRelaxedLatticeDCLabel$fConjunctionOfDisjDisj$fConjunctionOf[][] $fNewPriv[]$fNewPrivPrincipal$fNewPrivComponent $fNewDC[][]$fNewDCComponent[]$fNewDC[]Component$fNewDCPrincipalPrincipal$fNewDCComponentPrincipal$fNewDCPrincipalComponent$fNewDCComponentComponent$fConjunctionOfDisj[]$fConjunctionOf[]Disj$fConjunctionOfDisjPrincipal$fConjunctionOfPrincipalDisj$fConjunctionOfComponentDisj$fConjunctionOfDisjComponent$fConjunctionOfComponent[]$fConjunctionOf[]Component!$fConjunctionOfComponentComponent!$fConjunctionOfComponentPrincipal!$fConjunctionOfPrincipalComponent!$fConjunctionOfPrincipalPrincipal$fDisjunctionOfComponent[]$fDisjunctionOf[]Component$fDisjunctionOf[][]!$fDisjunctionOfComponentComponent!$fDisjunctionOfComponentPrincipal!$fDisjunctionOfPrincipalComponent!$fDisjunctionOfPrincipalPrincipal$fSingletonByteString $fSingleton[]$fSingletonPrincipal$fRelaxedLatticeSLabel$fLatticeSLabel $fToLNFSLabel$fRelaxedLatticeILabel$fLatticeILabel $fToLNFILabelpretty-1.1.1.0Text.PrettyPrint.HughesPJDoc$fPrettyShowILabel$fPrettyShowSLabel$fPrettyShowTCBPriv$fPrettyShowPrincipal$fPrettyShowDCLabel$fPrettyShowComponent$fPrettyShowConj$fPrettyShowDisj