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 qp. 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 or, where the principal o is the owner of the policy, and the principal r is the specified reader. A reader policy or 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:

readers(p, or) ≜ {q  |  if op then (qo or qr)}

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, or) 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 cd and cd are too.

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

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

readers(p, cd) ≜ readers(p, c) ∩ readers(p, d)
readers(p, cd) ≜ readers(p, c) ∪ readers(p, d)

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 cC d if and only if for all principals p, readers(p, c) ⊇ readers(p, d). If cC 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 ow allows the owner to specify which principals may have influenced ("written") the value of a given piece of information. The policy ow 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 ow describes the writers of information only if o can act for p.

writers(p, ow) ≜ {q  |  if op then (qo or qw)}

Dually to confidentiality policies, we denote disjunction for integrity policies with the operator ⊔, and conjunction with ⊓. The integrity policy cd is the conjunction of c and d, meaning that a principal p could have influenced information labeled cd 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 cd. The integrity policy cd is the disjunction of c and d; the writer set for cd is thus the union of the writer sets for c and d.

writers(p, cd) ≜ writers(p, c) ∩ writers(p, d)
writers(p, cd) ≜ writers(p, c) ∪ writers(p, 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 cI 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:

readers(p, {c;d}) ≜ readers(p, c)
writers(p, {c;d}) ≜ writers(p, d)

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 cC c' and dI d'. For labels L1 and L2, L1L2 holds if there are the same or more restrictions on uses of information labeled with L2 as there are on information labeled with L1.

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

L1L2 ≜ {C(L1) ⊔ C(L2) ; I(L1) ⊔ I(L2)}
L1L2 ≜ {C(L1) ⊓ C(L2) ; I(L1) ⊓ I(L2)}

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.

Symbol Jif syntax Example
Top principal * or  
Bottom principal _ or  
Conjunctive principal p&q p&q
  • Alice&Bob
  • Alice&(Bob,Chuck)&Dave
Disjunctive principal p,q p,q
  • Alice, Bob, Chuck
  • Alice, Bob&Chuck, Chuck&Dolores
Reader policy or o:r or o→r or o->r
  • _:_ is the least restrictive reader policy.
  • *:* is the most restrictive reader policy.
  • If no principal appears to the right of the colon, by default the top principal is used. Thus Alice: is equivalent to Alice:*.
Writer policy ow o!:w (deprecated) or o←r or o<-r
  • _←_ is the most restrictive (lowest integrity) writer policy.
  • *←* is the least restrictive (highest integrity) writer policy.
  • If no principal appears on the right-hand side, by default the top principal is used. Thus Alice← is equivalent to Alice←*.
Reader policy joins and meets or ⊔ o'r'
or ⊓ o'r'
o:r;o':r'
o:r meet o':r' or o:r ⊓ o':r'
  • Alice:; Bob:Chuck
  • Alice: meet Bob:Chuck
  • Alice: meet Bob:Chuck; Chuck: is the meet Alice: meet Bob:Chuck joined with Chuck:. Meets of joins of policies can be expressed using the label syntax below.
Writer policy joins and meets or ⊔ o'r'
or ⊓ o'r'
o←r;o'←r'
o←r meet o'←r' or o←r ⊓ o'←r'
  • Alice<-; Bob<-Chuck
  • Alice←⊤ meet Bob←Chuck
  • Alice!: meet Bob!:Chuck; Chuck!: is the meet Alice!: meet Bob!:Chuck joined with Chuck!:. Meets of joins of policies can be expressed using the label syntax below.
Labels {c;d} {c;d}
  • {Alice:Bob; Alice<-Chuck}
  • {Alice←Chuck; Alice→Bob ⊓ Bob→Bob; Chuck←} The order of policies appearing in the label does not matter. This label is equivalent to {Alice:Bob meet Bob:Bob; Alice!:Chuck; Chuck!:}, which has confidentiality policy Alice→Bob ⊓ Bob→Bob and integrity policy Alice←Chuck; Chuck←⊤.
  • {Alice:Bob} If no integrity policy is specified, then by default ⊥←⊥ is assumed. {Alice:Bob} is equivalent to {Alice→Bob; ⊥←⊥}.
  • {Bob<-Alice&Chuck} If no confidentiality policy is specified, then by default ⊥→⊥ is assumed. {Bob<-Alice&Chuck} is equivalent to {⊥→⊥; Bob<-Alice&Chuck}.
  • {} As neither a confidentiality policy or an integrity policy is specified, this label is equivalent to {⊥→⊥ ; ⊥←⊥}.
Label joins {c;d}⊔{c';d'} {c;c';d;d'} or {c;d}⊔{c':d'}  
Label meets {c;d}⊓{c';d'} {c;d} ⊓ {c';d'} or {c;d} meet {c';d'} or {c ⊓ c'; d ⊓ d'}
  • {Alice→Bob ⊓ Chuck→Dave; Alice←⊤ ⊓ Chuck←⊤}
  • {Alice→Bob; Alice←⊤} meet {Chuck→Dave; Chuck←⊤}. Braces are useful for specifying the order of label operations.
Grouping (L) {L}
  • {{Bob→*}⊔{Alice→*}}. This is the same as {Bob→* ; Alice→*}; the extra layer of braces has no effect.
  • {{Bob→⊤}⊔{Alice→⊤}}⊓{Chuck←Dave}
  • Grouping specifies the order of label operations.

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.

Jif label Meaning
{Alice:; L; Alice!:Bob} {Alice→⊤ ; Alice←Bob} ⊔ L
{*lbl1; x; L meet *lbl2} lbl1 ⊔ x ⊔ (L ⊓ lbl2)
No integrity or confidentiality policies appear in this label.
{*lbl1; Alice←} {⊥→⊥ ; Alice←⊤} ⊔ lbl1
Since an integrity policy appears, the default confidentiality policy ⊥→⊥ is used.
{*lbl1; Alice←Bob; Chuck←⊥; *lbl2; Alice→Chuck; Chuck→Dave} {Alice→Chuck ⊔ Chuck→Dave ; Alice←Bob ⊔ Chuck←⊥} ⊔ lbl1 ⊔ lbl2
The semicolon (;) is consistently interpreted as a join operation, for both confidentiality and integrity policies.
{*lbl1} lbl1
No integrity or confidentiality policy appears.
{*lbl1 meet Alice:} Error! Attempting to take the meet of a label (*lbl1) and a confidentiality policy (Alice:).
{*lbl1} meet {Alice:} {Alice→⊤ ; ⊥←⊥} ⊓ lbl1