Protecting Privacy using the Decentralized Label Model ====================================================== IFC Background, [= What's a lattice? What's a pre-order? Contrast with "access control" (i.e., DAC) What is decentralized? Bob and Preparer example Protect against release Sign off on result What is execution model? Code is written in a new laguage, Jif You have a trusted execution platform for Jif Functions annotated with integrity and authority Mutually distrustful principals, code limited authority who installed it All input data is labeled Labels stick to data, and propagate to variables All output channels are labeled Jif mostly statically checks programs Code written by untrusted people can then access sensitive data Jif guarantees it won't output protected data to improper channel What are principals in this paper? Represent users, roles, group Organized with run-time hierarchical acts for relation Acts for relation written p >= q (call it "p >= q" for ASCII notes) What is the Decentralized Label Model proposed? Labels (policies, owners, readers) Set of policies expressing privacy requirements stated by principals Each policy is written "owner: readers" Can move data only when *all* policies in label are satisfied Example: Fill in labels in Bob & preparer picture When can you relabel L1 to L2 (p. 9)? I.e., when do you have L1 [= L2? - If L2 has the same policies as L1 - If L2 is more restrictive than L1 (L1 [= L2) L2 removes readers from the policies in L1 L2 adds a new policy to L1 L2 adds a reader r' >= r where r is already in the same policy L2 replaces an owner o with an owner o' >= o - CANNOT assign if: L2 removes a component - In general, how do we determine if L2 is more restrictive than L1? For each policy I in L1, there must be a J in L2 that "covers" I J = {o2: R2} covers I = {o1: R1} iff o1 => o2 and for each p2 in R2 there's a p1 in R1 s.t. p1 => p2 Why not allow: {A: A, B; A: A, C} [= {A: A}? At run time, might introduce D where D >= B and D >= C So {A: A, D} [= {A: A, B; A: A, C}, but NOT {A: A, D} [= {A: A} How does declassification work (p. 20)? Write "declassify (variable, new-label)" Can remove any policies for which the code speaks for the owner If LA is {p:} for all principals code currently acts for, can declassify L1 to L2 if L1 sqsubseteq L2 \sqcup LA What is label polymorphism? Example: Fig 7 (p. 21) works regardless of user and password labels What happens when you compute a value from two values? E.g., say x1 has L1, x2 has L2, and you want z = x1 | x2 Label of z, L3, must be as restrictive as both previous labels I.e., must have L1 [= L3 and L2 [= L3 But want L3 to be the *least* such label So least upper bound or join of L1 and L2 (written L1 \sqcup L2) [Let U be union sign in ASCII, i.e., TeX \cup symbol] L1 \sqcup L2 = L1 U L2 with redundant labels removed E.g., Say L1 = {amy : bob}, L2 = {amy : bob, carl} then L3 = {amy : bob} (since carl cant satisfy L1 anyway) Declassification (p. 12) Why is restriction compile time, declassification run time? Why do labels not have a partial order? Can have redundant policies (p. 15) so L1 /= L2 but L1 [= L2 and L2 [= L1 Why not use "normal form" to make labels partial order, not pre-order? With polymorphic labels, can't always tell what policies redundant Doesn't seem to matter, anyway. Transitivity is what matters How does I/O work? Use channels, which are half-variables (intput or output) - Input channels must be properly labeled by people producing data - Anyone can create an output channel with the empty label {} - Can only write unrestricted data to such an output channel How to implement channel with non-default label? To output restricted data, must have permission to declassify it to {} Just wrap empty label in declassifier code Don't need universal consensus on who gets output channel--decentralized What is the difference between {A: A} and {B: A}? Why do you need latter? B wants A to read doc but not easily forward it System might label A's terminal as {root: A}, where root >= B Integrity What does an integrity label mean? Much the converse of secrecy. Now {o: w1, w2} says "o believes only w1 or w2 has written this" Most restrictive label is now {} -- no guarantee who created data Variable labeled {o:w1} can be written to {o:w1,w3}, but variable labeled {o:w1,w3} cannot "an integrity label most be assigned to each function" (p. 17). Why? label of f(x,y) becomes {f; x; y} -- why? Relabeling rules (p. 16) - Add a writer (always safe) - Remove a policy - Replace a writer (only if old writer acts for new) - Add a policy J identical to old policy I except o(I) acts for o(J) Declassification rule (p. 17) How do secrecy and integrity labels compose? If secrecy labels already a lattice, why use separate integrity labels? Want to have default somewhere in the middle of lattice, not top or bot When can you assign L1 to L2? What do language extensions look like? Labels written with braces int{root:} x; Can put a variable name in braces for same label: int{x} y; declassify operator allows restrictions to be weakened actsFor statement lets code check if p1 => p2 Variables and arguments can have special type label, for run-time checking switch label statement/protected type for manipulating run-time labels How are Jif labels analogous to type checking? With subtyping have both apparent (static) and actual (runtime) types Most code statically checked on apparent types, but can have dynamic cast With labels may have similar static partial knowledge actsFor (p1, p2) S, means you know p1 >= p2 In password example (Fig. 7), know {match}={root;user;password} Don't need actual runtime values to reason about these Why not just check labels dynamically? Bad for performance Bad for correctness (p. 19) x = 0; if (b) { x = 1; } What is solution? Jif associates a static label with the program counter (pc) The label of an expression must be at least as restrictive as pc