A Decentralized Model for Information Flow Control ================================================== What is the goal of this paper? - Controlling information flow - Very different environment from military/orange book setting What is the security model for this work? - Code is written in a new laguage, Jif - You have a trusted execution platform for Jif - Each process code runs on behalf of an owner principal Mutually distrustful principals--no hierarchy necessarily - 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 - Declassification now part of the security model Example: Bob and the preparer (Fig. 2) Hierarchy of principals - One principal can act for another: carl => manager, bob & amy => group - Hierarchy can be determined at run time What is a label in Jif? - Set of components expressing privacy requirements stated by principals - Each component is written "owner: readers" - Each component is a policy for use of the data - A user can read data only if the read obeys *all* policies in label - Example: Fill in labels in Bob & preparer picture When can you assign a value with label L1 to a variable with L2? - If L2 has the same policies as L1 - If L2 is more restrictive than L1 (L1 sqsubseteq L2) L2 removes readers from the policies in L1 L2 adds a new policy to L1 L2 adds a reader r' that already acts for an r in the same policy L2 replaces an owner o with an owner o' that speaks for 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 - No individual covers (p. 23) Say L1 = {o3:}, o1 => o3 and o2 => o3, and L2 = {o1: p1; o2: p2} What goes wrong if you assign data with L1 to variable with L2? Could introduce new principal p3, where p3 => p1 and p3 => p2 What happens when you compute a value from two values? - E.g., say x has L1, y has L2, and you want z = x1 | x2 - Label of z, L3, must be as restrictive as both previous labels L3 = L1 sqcup L2 = L1 cup 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) Straw man: Can you just check labels dynamically? - Bad for performance - Bad for correctness (p. 19) x = 0; if (b) { x = 1; } - Jif associates a label with the program counter (pc) - The label of an expression must be at least as restrictive as pc Syntax primer: - 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 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 about I/O? 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 - To output restricted data, must have permission to declassify it to {} Language properties - Allows privileges to be checked statically, But also authority (principal hierarchy) to be granted dynamically Analogy: Statically-typed language with subtyping - Label polymorphism allows re-usable code - Run-time label checking and first-class label values But static checking is done to make sure dynamic check doesn't leak info Example: Figure 7 - Automatic label inference -- saves user from writing many annotations Integrity - 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 - When can you relabel (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) Note functions now have integrity labels. label of f(x,y) becomes {f; x; y} -- why? When can you assign L1 to L2?