Decentralized label model

Jif allows mutually distrusting entities to express information-flow security policies for confidentiality and integrity. Security policies are expressed using the decentralized label model (DLM) [ML00]. In this section, we describe the core concepts of the DLM: principals, policies, and labels, and present the syntax used to write labels in Jif programs.

Principals

A principal is an entity with some power to observe and change certain aspects of the system. The goal of Jif is to permit principals to express security requirements and to enforce them. Jif provides a flexible, open-ended mechanism for defining principals, which allows applications to model users, processes, user groups, or application-specific entities with security concerns.

A principal p may delegate authority to another principal q, in which case q is said to act for p, written q≽p. If the principal p acts for the principal q, any action taken by p is implicitly assumed to be authorized by q. Thus, the acts-for relation expresses trust relationships between principals. The acts-for relation is reflexive and transitive, and is similar to the speaks-for relation [LABW91] used in authentication logics. The hierarchy of principals is also similar to a role hierarchy [San96].

The acts-for relation can be used to model groups and roles conveniently. A group principal, such as students, is modeled by authorizing all of the principals representing members of the group to act for the group principal. That is, the group principal delegates its authority to all of the group members. A role, a restricted form of a user's authority, is modeled by authorizing the user's principal to act for the role principal.

Jif supports a top principal ⊤ able to act for all principals, and a bottom principal ⊥ that allows all principals to act for it.

Jif allows principals to be composed together to form conjunctive and disjunctive principals [LABW91,TZ05]. A conjunctive principal, written "p&q", is able to act for both the principals p and q. A disjunctive principal, written "p,q" delegates its authority to p and q, that is, p can act for p,q, and q can act for p,q. Conjunctions and disjunctions are associative, commutative and idempotent.

Confidentiality policies

Principals express their security concerns with labels containing security policies.

A reader policy allows the owner of the policy to specify which principals the owner permits to read a given piece of information. A reader policy is written o→r, where the principal o is the owner of the policy, and the principal r is the specified reader. A reader policy o→r says that o permits a principal q to read information only if q can act for either the owner of the policy or the specified reader r. As a formal semantics for reader policies, we define the function readers(p, c) to be the set of principals that principal p believes should be allowed to read information according to reader policy c:

A principal p believes that a reader policy c should restrict the readers of information only if the owner of the policy can act for p. The parameterization on p is important in the presence of mutual distrust, because it allows the significance of the policy to be expressed for every principal independently. If principal o owns a policy that restricts the readers of information, it does not necessarily mean that another principal p also believes those restrictions should apply. Thus, if o does not act for p, then readers(p, o→r) is the set of all principals; in other words, p does not credit the policy with any significance. While this semantics is expressed differently, it is consistent with the original DLM semantics [ML00].

Conjunction and disjunction. Greater expressiveness is achieved by allowing conjunctions and disjunctions of reader policies. We define confidentiality policies to be the smallest set containing all reader policies and closed under the binary operators ⊔ and ⊓. That is, if c and d are confidentiality policies, then both c⊓d and c⊔d are too.

The operator ⊔ is conjunction for confidentiality policies: c⊔d is the policy that enforces both c and d. The policy c⊔d permits a principal to read information only if both c and d allow it. Thus, c⊔d is at least as restrictive as both c and d. The operator ⊓ is disjunction for confidentiality policies: c⊓d allows a principal to read information if either c or d allows it. Thus, c⊓d is no more restrictive than either c or d.

We extend readers(p, c) for confidentiality policies. Since c⊔d enforces both c and d, the reader sets for c and d are intersected; for c⊓d the reader sets are combined.

Ordering confidentiality policies. Using the readers(∙, ∙) function, we can define a "no more restrictive than" relation ⊑_C on confidentiality policies. For two confidentiality policies c and d, we have c ⊑_C d if and only if for all principals p, readers(p, c) ⊇ readers(p, d). If c ⊑_C d then every principal p believes that c permits at least as many readers as d does. The confidentiality policy c is thus of lower (or equal) confidentiality than d, and so information labeled c can be used in at least as many places as information labeled d: policy c is no more restrictive than policy d.

The relation ⊑_C forms a pre-order over confidentiality policies, and its equivalence classes form a lattice. The operators ⊔ and ⊓ are the join and meet operators of this lattice. The least restrictive confidentiality policy is the reader policy ⊥→⊥, where ⊥ is a principal that all principals can act for, since all principals believe that information labeled ⊥→⊥ is allowed to be read by any principal. The most restrictive expressible confidentiality policy is ⊤→⊤, where ⊤ is a principal that can act for all principals; information labeled ⊤→⊤ is allowed to be read only by principal ⊤.

Integrity policies

Integrity and confidentiality are well-known duals, and we define integrity policies dually to confidentiality policies. The set of integrity policies is formed by closing writer policies under conjunction and disjunction.

A writer policy o←w allows the owner to specify which principals may have influenced ("written") the value of a given piece of information. The policy o←w means that according to the owner o, a principal q could have influenced the value of the information only if q can act for the owner o or the specified writer w. Writer policies describe the integrity of information in terms of its provenance.

We define the function writers(p, c) to be the set of principals that principal p believes may have influenced information according to writer policy c. Like reader policies, a principal p believes that writer policy o←w describes the writers of information only if o can act for p.

Dually to confidentiality policies, we denote disjunction for integrity policies with the operator ⊔, and conjunction with ⊓. The integrity policy c⊓d is the conjunction of c and d, meaning that a principal p could have influenced information labeled c⊓d only if both c and d agree that p could have influenced it. The writer sets for c and d are thus intersected to produce the writer set for c⊓d. The integrity policy c⊔d is the disjunction of c and d; the writer set for c⊔d is thus the union of the writer sets for c and d.

The "no more restrictive than" relation ⊑_I on integrity policies is defined dually to the relation ⊑_C: for two integrity policies c and d, we have c ⊑_I d if and only if for all principals p, writers(p, c) ⊆ writers(p, d). Intuitively, information with a smaller writer set has higher integrity than information with a larger writer set, since fewer principals may have influenced the value of the former; the higher the integrity of information, the fewer restrictions on where that information may be used.

The relation ⊑_I forms a pre-order over integrity policies, and the equivalence classes form a lattice, with join and meet operators ⊔ and ⊓ respectively. The most restrictive integrity policy is ⊥←⊥, since all principals believe that any principal may have influenced the information. The policy ⊤←⊤ is the least restrictive expressible integrity policy, as all principals believe that only principal ⊤ (who can act for all other principals) has influenced the information.

Labels

A label is a pair of a confidentiality policy and an integrity policy. We write a label {c;d}, where c is a confidentiality policy, and d is an integrity policy. The confidentiality projection of {c;d}, written C({c;d}), is c, and the integrity projection I({c;d}) is d.

We extend the readers(∙, ∙) and writers(∙, ∙) functions appropriately:

Example. Consider the following label: {Alice→Bob,Chuck ; Alice←Chuck ⊔ Bob←Chuck,Dave}. The confidentiality policy of this label is a single reader policy, and the integrity policy is the disjunction of two writer policies. The reader policy is owned by Alice, and permits any principal that can act for Bob, Chuck, or Alice to read information. No other principal specifies a reader policy, so principals for whom Alice cannot act for allow all principals to read the information; principals that Alice can act for adhere to Alice's restrictions, and permit only principals that can act for Bob, Chuck, or Alice to read information. Of the two writer policies, one is owned by Alice and the other by Bob. Alice believes that only Chuck or Alice could have influenced the information, while Bob believes only principals that can act for any of Chuck, Dave, or Bob could have influenced the information. Principals that neither Alice nor Bob can act for implicitly believe that the information may have been influenced by any principal at all, and is thus completely untrustworthy. A principal that both Alice and Bob can act for believes that principals that can act for Alice, Bob, Chuck, or Dave may have influenced the information.

Ordering labels. We define the "no more restrictive than" relation ⊑ on labels using the relations ⊑_C and ⊑_I. In particular, {c;d} ⊑ {c';d'} if and only if c ⊑_C c' and d ⊑_I d'. For labels L₁ and L₂, L₁ ⊑ L₂ holds if there are the same or more restrictions on uses of information labeled with L₂ as there are on information labeled with L₁.

The relation ⊑ forms a pre-order, whose equivalence classes form a lattice. We use ⊔ and ⊓ for the join and meet operations over this lattice,

Label syntax in Jif

Labels are used to annotate types in Jif programs. The following table shows the appropriate syntax for writing principals, policies, and labels in Jif programs. Some non-ASCII characters may be used when writing Jif programs. See Lexical considerations for more information.

Jif extends the expressiveness of labels with several language mechanisms. Label parameters, dynamic labels, and polymorphic argument labels can all appear within labels. To interpret a label in which elements other confidentiality and integrity policies appear, the following algorithm is followed: (1) all integrity and confidentiality policies are separated and interpreted as a normal label, {c;d}; (2) other elements in the label are joined with {c;d}.

The following table gives examples of how to interpret Jif labels. L is a label parameter, x is an argument label, and lbl1 and lbl2 are dynamic labels.