Program P(v, s) (use randomness)
- V = visible input (visible to adversary)
- S = secret input
Output includes every behavior the adversary can see
Does P leak info about s? Adversary can see EVERYTHING but s
Play a game with the adversary:
- Tell adv P
- Adversary chooses v, s_0, s_1 (secret 0 and secret 1).
- We flip a coin to get a choice b, which is 0 or 1
- We tell adversary P(v, s_b)
- Adversary guess b
To win, adversary must guess right > 50% of the time (do better than random guessing)
P leaks info iff there exists an adversary who can win.
P leaks info iff distributions P(v, s0) and P(v, s1) are distinguishable.
In other words: to avoid leakage, s should have no distinguishable impact on output.
How do you enforce this?
- Unlike previous properties, can�t enforce program flow by monitoring. Must think about all the what if�s.
- What if input were different?
- What if randomness had turned out differently?
In practice, you can�t demonstrate non-leakiness
- theoretically hard
- practical issues related to timing
So, assume all programs leak their inputs. �Contagion model�: when program sees input, it�s �infected,� and the output reveals something about inputs.
A failed model? General method for specifying/enforcing info flow policy.
Assumes contagion model
Relies on:
- Sets of labels: Labels on data (sensitivity level), Labels on people or programs (trust level)
- A lattice (L, <= operator) is a set L of labels, and a partial ordering <= on the members of L, such that for every two elements a, b in L, there is a �least upper bound� of a and b, and a �greater upper bound of a and b.
- a <= u and b <= u, and for all v in L, a <= v and b <= v, u <= v
- l <= a and l <= b, and for all k in L such that k <= a and k <= b, k <= L
A partial order is a relation that is:
- reflexive for all x <= x
- transitive for all x, y, z if x <= y and y <= z, then x <= z
- asymmetric for all x, y if x <= y and y <= x, then x = y
Examples of lattice labeling
- Linear chain of labels: Unrestricted <= confidential <= highly confidential
- Compartments: Label is a set of projects, a set of clients, or a set of topics from a predefined list
Ordering operation is a subset
- org chart: Label is a position on org chart of organization L1 <= L2 iff L1 reports to L2 (directly or indirectly).
- Combination of methods: Label is (a, b) where a is in S, b is in S, and (a1, b1) <= (a2, b2) iff a1 <= a2 and b1 <= b2.
Bell-LaPadula Theorem: Assume security labels for a lattice. Every file, every program has a label.
�No read up�: program P can read file f only if L(f) <= L(p). This is the idea of �clearance.�
�No write down�: Program P can modify file f only if L(p) <= L(f). Remember the contagion model: I can�t write to an unrestricted file b/c I might leak info that can be read by less privileged users.
Theorem: If L(f1) <= L(f2), and the 2 rules are enforced, then information from f2 cannot leak into f1.
- No info leaking out
- This covers confidentiality but not integrity. Bad/wrong info can still get in.
- Can�t enforce rigorously
- Need Exceptions
- Declassifying old data
- Aggregate data, anonymized data
- Policy decision that exception is OK
Example: a workstation that can know what�s classified and unclassified.
- What happens when you create a file?
- disk space
- results of ls should be what?
