úÎzÀvZC      !"#$%&'()*+,-./0123456789:;<=>?@AB=GClass used to convert list of principals to a disjunction category and  vice versa. Given list return category. Given category return list.  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., a . 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, N for principals to be used in integrity labels or be ignoerd a corresponding  privilege ( 2) 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. HClass used to reduce labels to a unique label normal form (LNF), which J corresponds to conjunctive normal form of principals. We use this class - to overload the reduce function used by the , , etc. 0A label is a conjunction of disjunctions, where  MkLabelAll is @ the constructor that is associated with the conjunction of all  possible disjunctions. .Labels forma 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. Bottom of lattice, "¥ Top of lattice, "¤ Join of two elements, "” Meet of two elements, "“ Partial order relation, "‘ 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 "Á ...]} !"#"A category, i.e., disjunction, of  s.  The empty list '[]'3 corresponds to the disjunction of all principals.  Conceptually, [] = [P_1 "Á P_2 "Á ...] $%&KA label without any disjunctions or conjunctions. This label, conceptually I corresponds to the label consisting of a single category containing all  principals. Conceptually,   emptyLabel = <{[P_1 "Á P_2 "Á ...]}> ' The dual of &, ' consists of the conjunction of C all possible disjunctions, i.e., it is the label that implies all  other labels. Conceptually,   allLabel = <{[P_1] "À [P_2] "À ...}> C Predicate function that returns True if the label corresponds to  the &. DPredicate function that retuns True if the label corresponds to  the '. (DGiven two labels, take the union of the disjunctions, i.e., simply  perform an "and"0. Note the new label is not necessarily in LNF. )Given two labels, perform an "or". 4 Note that the new label is not necessarily in LNF. EDDetermines if a conjunction of disjunctions, i.e., a label, implies D (in the logical sense) a disjunction. In other words, it checks if  d_1 "À ... "À d_n => d_1.  Properties:  " X, ' `E` X = True  " X, X `E` & = True  " X"`&, & `E` X = False 2Note that the first two guards are only included E for safety; the function is always called with a non-ALL label and  non-null disjunction. *EDetermines if a label implies (in the logical sense) another label.  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 H categories from the label. To return a clean label, it sorts the label ! 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. 1,Given a list of categories, return a label. Given list return category. 2+Given a label return a list of categories. Given category return list. FTo/from Gs and #unction categories. HTo/from  s and #unction categories. ITCBPriv is an instance of J. K 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_2LEach = can be reduced a unique label representation in LNF, using  the  function. M Reduce a  to LNF.  First it applies  cleanLabel0 to remove duplicate principals and categories. ! Following, it removes extraneous/,redundant categories. A category is said to J be extraneous if there is another category in the label that implies it. NLabels have a unique LNF (see  ) form, and equality testing is " perfomed on labels of this form. 3  !"#$%&'()*+,-./0123#$% !"&' , ./-0()+*123   !"!"#$%$%&'()*+,-./0123Class used to create  s and  s. 4 Given element create privilege. 5KGiven privilege and new element, create (maybe) trusted privileged object. OClass used to create s. 6!Given two elements create label. P#Class used to create conjunctions. 7&Given two elements it joins them with "À Q#Class used to create disjunctions. 8&Given two elements it joins them with "Á R.Class used to create single-principal labels. 9Creates a singleton label. : Empty label. ; All label. SInstances using disjunctions. T+Instances using strings and not principals 3456789:; 87:;96345 345456789:;@  !"#$%&'()*+,-./012345O6P7Q8R9:;<A secrecy-only DC label. =<=<=<==>An integrity-only DC label. ?>?>?>??@Class used to create a U type of DCLabel-related types A Convert to U. B Render a @ type to a string. @AB@AB@AAB ,-123456789:;,91287:;6 -345V      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSOTUVWXYZ[\]^_`abc dclabel-0.0.1 DCLabel.CoreDCLabel.NanoEDSLDCLabel.SecrecyDCLabel.IntegrityDCLabel.PrettyShow DCLabel.TCB DCLabel.SafeDisjToFromList listToDisj disjToListOwnsowns CanDelegate canDelegateRelaxedLattice canflowto_pPrivTCBPriv MkTCBPrivpriv Principal MkPrincipalnameDCLabel MkDCLabelsecrecy integrityToLNFtoLNFLabelMkLabellabel MkLabelAllLatticebottomtopjoinmeet canflowtoConjMkConjconjDisjMkDisjdisj emptyLabelallLabel and_labelor_labelimplies cleanLabel principal delegatePrivnoPriv rootPrivTCB createPrivTCB listToLabel labelToListNewPrivnewPriv newTCBPrivnewDC./\..\/. singleton<>><SLabelMkSLabelILabelMkILabel PrettyShowpShow prettyShow isEmptyLabel isAllLabel impliesDisj$fDisjToFromList[]baseGHC.BaseString$fDisjToFromListPrincipal$fMonoidTCBPriv Data.MonoidMonoid$fLatticeDCLabel$fToLNFDCLabel $fToLNFLabel $fEqLabelNewDC ConjunctionOf DisjunctionOf Singleton$fConjunctionOfDisjDisj$fConjunctionOf[][]pretty-1.1.0.0Text.PrettyPrint.HughesPJDoc