Brief Review of Jif's Label
===========================

Recall that, in Jif, there are two kinds of labels: privacy labels and
integrity labels.  In both cases, a label consists of an open curly
bracket '{', followed by a (possibly list) of policies (separated by a
semicolon ';'), followed by a close curly brackets '}'.  
Each policy specifies a principal, followed by a colon ':', followed
by a (possibly empty) list of principals (separated by a comma ',').
To distinguish between the two kinds of labels, in the code fragments
below will prepend a 'P' or an 'I' to the list of policies, as
mnemonics for "Privacy" and "Integrity", respectively.
Using a BNF grammar, we can represent such syntax as follows:

  <privacy_label>   ::= '{' P/ [<policy> {; <policy>}] '}'
  <integrity_label> ::= '{' I/ [<policy> {; <policy>}] '}'
  <policy>          ::= <principal>: [ <principal> {, <principal> }]  

where <principal> is any principal in the system (e.g., unix
usernames, groupnames, etc.).

(Disclaimer: this is in no way a standard syntax! Again, it's for
illustration only.)

For example, the following label:

  {P/ alice: alice, bob}

is a privacy label that says "alice requires that only alice and bob
should be allowed to read data with this label."
Thus, in a privacy label, each policy specifies a requirement, which
is being demanded by the principal to the left of the colon ':'. 
The system should always enforce this requirement when running code
under the authority of any principal.

Now an example of integrity label:

  {I/ bob: charles}

This indicates that "bob believes that only charles has so far
influenced the data with this label."
Thus, policies in an integrity label indicate beliefs, in the eye of
the principal to the left of the colon ':' (in this case, bob).
The system should only trust this belief when running code under the
authority of the principal expressing such belief (bob in the example).  

For privacy labels, including several policies indicates a conjunction
of the requirements specified by the individual policies:

  {P/ alice: alice, bob; bob: bob}

Data labeled with the above privacy label should only be readable by
bob, since allowing alice to read it would violate the second policy.

For integrity labels, including several policies indicates a disjunction
of the beliefs specified by the individual policies:

  {I/ alice: alice, bob; bob: bob}

The meaning of the above label is a bit more obscure; it basically says that: 
1) when executing code under alice's authority, it is safe to believe
that data labeled with this label has not been modified by anybody,
except possibly for alice and bob; 
2) when executing under bob's authority, then the belief is stronger:
the system can trust that the data was influenced by bob only.

The above may look strange at first: is alice claiming she has
touched the data but in fact she has not, or is bob being naive and
not noticing that alice may have touched the data?
One may think that integrity labels like this do not make sense, and
should therefore not be allowed.  However, keep in mind that labels do
not need to make sense in all possible situations; if there is just one
scenario in which they could be useful, then they should be allowed.
In the specific case of the above label, consider the case that bob
trusts alice, but alice does not trust bob: then, alice would record
all possible principals that might have touched some piece of data,
and this could result in her belief "alice: alice, bob".  As for bob,
the fact that he trusts alice gets translated, in the language of
integrity labels, by stating that all changes that alice could have
are "as if bob had done them." Therefore, bob's belief can be written
as "bob: bob".

Enough talking about labels; let's see how they work via an adaptation
of the "Millionaires' Problem."

A Jif-based take to the Millionaires' Problem
=============================================

Two software developers, alice and bob, work at the same company, run
by mark.  Each month, mark records the salary of each employee in a
file in the /salary/ directory of the company file server; so
/salary/alice and /salary/bob report the amount in alice's and bob'a 
monthly paychecks, respectively.

The /salary/ directory (and each file therein) is writable by mark 
only; however, each employee has read permission for the file
corresponding to his/her name.  So, /salary/alice is readable only by
alice (and possibly by mark), whereas /salary/bob is readable by bob only. 

However, the system used by mark's company does not use standard
unix-like access control; rather, it uses Jif's labels, so that the
permissions described so far actually mean that if a program ever
attempts to read a file, the content read from such file must go to
a variable labeled with a label that is at least as restrictive as the
permission specified for the file.  Recall that, assuming programs are
run within the trusted computing environment described in the Jif
paper, this won't cause any information leakage: in particular, if bob
open /salary/alice and reads in alice's salary, he won't be able to
print out the value to his terminal, since bob's terminal, in Jif's
model, is an output channel with privacy label {bob : bob}.

Now, let's go back to our example, and let's assume that alice and bob
have a common friend, charles, that they believe is trustworthy, but
courius.  In other words, both alice and bob believe that if they ask
charles to do something, charles will perform the assigned task
correctly: however, charlse will try to learn as much as possible
about what he is doing.  Now, alice and bob want to find out whom
(between the two of them) is getting paid the most, and they ask
charles to compare their salaries.  But, they don't want to disclose
their salary to charles; how can they do that? 

Part 1: Using Privacy Labels Only
=================================

Consider the following code fragment, run by charles:

  C1.  FileReader {alice: alice} fa = FileReader ("/salary/alice");
  C2.  FileReader {bob: bob} fb = FileReader ("/salary/bob");
  C3.  int {alice: alice} sa = fa.Getint ();
  C4.  int {bob: bob} sb = fb.Getint ();
  C5.  FileWriter {alice: alice; bob: bob} fmax = FileWriter ("/tmp/alice_and_bob");
  C6.  if (sa > sb) 
  C7.    fmax.PutString("alice");
  C8.  else
  C9.    fmax.PutString("bob");
  C10. fa.Close ();
  C11. fb.Close ();
  C12. fmax.Close ();

(Disclaimer: this *is not* real code you can actually run; the syntax
used is just meant to be suggestive of what is going on.)

Now, /tmp/alice_and_bob contains the name of whom, between alice and
bob, is making more money: however, since the data is labeled {alice:
alice; bob: bob}, nobody can dump its content to terminal (except
possibly for mark, if the principal hierarchy allows him to "act for"
both alice and bob). 

So, alice runs the following code fragment to declassify the data,
allowing bob to read the content:

  A1  FileReader {alice: alice; bob: bob} fmax = FileReader ("/tmp/alice_and_bob");
  A2. FileWriter {alice: alice, bob; bob: bob} fb =  FileWriter ("/tmp/bob");
  A3. String {alice: alice; bob: bob} max = fmax.GetString ();
  A4. String {alice: alice, bob; bob: bob} decl_max = 
        Jif.Declassify (max, {alice: alice, bob; bob: bob});
  A5. fb.PutString (decl_max);
  A6. fb.Close ();
  A7. fmax.Close ();  

The key point in the above fragment is the declassification on line
A4: since the above code is running with alice's authority, it is OK
to modify the label {alice: alice; bob: bob} (attached to the String
max) into the less restrictive label {alice: alice, bob; bob: bob},
which now allows bob to dump the content of /tmp/bob to his terminal.

However, this would not be fair, as alice still cannot read the
outcome of the computation; bob should declassifies /tmp/bob into 
/tmp/alice_or_bob:

  B1. FileReader {alice: alice, bob; bob: bob} fmax = FileReader ("/tmp/bob");
  B2. FileWriter {alice: alice, bob; bob: alice, bob} fb =  FileWriter ("/tmp/alice_or_bob");
  B3. String {alice: alice, bob; bob: bob} max = fmax.GetString ();
  B4. String {alice: alice, bob; bob: alice, bob} decl_max = 
        Jif.Declassify (max, {alice: alice, bob; bob: alice, bob});
  B5. fb.PutString (decl_max);
  B6. fb.Close ();
  B7. fmax.Close ();

It seems that now we should be done: the content of /tmp/alice_or_bob can
be dump by either of them, so they now who is getting richer.  Or do they?

What the use of privacy labels guarantees in the above example is just
that the content of /tmp/alice_or_bob can be read by alice, bob, and
nobody else.  However, nothing ensures that the content correctly
identifies the richest!  Even assuming that charles is honest, so that
he actually carried out the computation correctly, bob cannot tell
whether alice changed the content of the file while declassifying its
label.  Assuming that alice and bob had previously agreed that the
richer was going to offer a beer to the other party, then alice can
make sure she is going to drink on bob by changing one line in the
above pseudocode: 

  new-A4. String {alice: alice, bob; bob: bob} decl_max = "bob";

To get around this problem, alice, bob and charles should use
Integrity labels, too.

Part 2: Using Privacy and Integrity Labels 
==========================================

Integrity labels can help to reason about the principals that may have
modified the content of the /tmp/alice_or_bob file.

Consider the following modification to charles code, where we attach
integrity labels by which charles says that he is the one to write
the content to /tmp/alice_and_bob: 

  C1'. FileReader {P/ alice: alice} {I/ charles: mark} fa = FileReader ("/salary/alice");
  C2'. FileReader {P/ bob: bob} {I/ charles: mark} fb = FileReader ("/salary/bob");
  C3'. int {P/ alice: alice} {I/ charles: mark} sa = fa.Getint ();
  C4'. int {P/ bob: bob} {I/ charles: mark} sb = fb.Getint ();
  C5'. FileWriter {P/ alice: alice; bob: bob} {I/ charles: charles, mark} fmax = 
         FileWriter ("/tmp/alice_and_bob");
  C6'. if (sa > sb)
  C7'.   fmax.PutString("alice");
  C8'. else
  C9'.   fmax.PutString("bob");
  C10'. fa.Close ();
  C11'. fb.Close ();
  C12'. fmax.Close ();

Now, the integrity label associated to /tmp/alice_and_bob is 
{I/ charles: charles, mark}, which express charles' belief that only
he and mark could have affected to content of /tmp/alice_and_bob.

Let's take a look at the new version of alice's code:

  A1'. FileReader {P/ alice: alice; bob: bob} {I/ charles: charles, mark} fmax = 
         FileReader ("/tmp/alice_and_bob");
  A2'. FileWriter {P/ alice: alice, bob; bob: bob} {I/ charles: charles, mark} fb =
         FileWriter ("/tmp/bob");
  A3'. String {P/ alice: alice; bob: bob} {I/ charles: charles, mark} max = fmax.GetString (); 
  A4'. String {P/ alice: alice, bob; bob: bob} {I/ charles: charles, mark} decl_max =
         Jif.Declassify (max, {P/ alice: alice, bob; bob: bob}); 
  A5'. fb.PutString (decl_max);
  A6'. fb.Close ();
  A7'. fmax.Close ();  

The most interesting line in alice's code is again the one dealing
with declassification, namely A4': observe that the integrity label of
decl_max does not mention alice as a writer.  Why is this so?  Because
by calling Jif.Declassify, alice is only altering the label, not the
content, of the variable max.

On the other hand, if alice attempted to change line A4' so that
/tmp/bob always contained "bob", her code wouldn't pass Jif's checks:

  new-A4'. String {P/ alice: alice, bob; bob: bob} {I/ charles: charles, mark} decl_max = "bob";

Indeed, when performing the assignment, the system would require that
the integrity label of decl_max (i.e. {I/ charles: charles, mark} gets
changed to {I/ charles: charles, mark, alice}).

For completeness, we also include bob's code with integrity labels added: 

  B1'. FileReader {P/ alice: alice, bob; bob: bob} {I/ charles: charles, mark} fmax = 
         FileReader ("/tmp/bob"); 
  B2'. FileWriter {P/ alice: alice, bob; bob: alice, bob} {I/ charles:charles, mark} fb =
         FileWriter ("/tmp/alice_or_bob");  
  B3'. String {P/ alice: alice, bob; bob: bob} {I/ charles: charles, mark} max =
          fmax.GetString ();
  B4'. String {P/ alice: alice, bob; bob: alice, bob} {I/ charles: charles, mark} decl_max = 
    Privacy.Declassify (max, {P/ alice: alice, bob; bob: alice, bob});
  B5'. fb.PutString (decl_max);
  B6'. fb.Close ();
  B7'. fmax.Close ();

Now that they are sure that they know who is richer, alice and bob can
happily go have a beer together and offer a drink to charles for the help ;)