IntroductionFlumeBoatDataflow ConstraintsSpecification ConstraintsEvaluationConclusionAuto-Labeling for Fun and ProfitMatt Elder Bill HarrisUniversity of Wisconsin - Madison{elder, wrharris}@cs.wisc.eduCS 736: Advanced Operating Systems Final PresentationIntroduction Flume Boat Evaluation ConclusionOutline1Introduction2Flume3BoatDataflow ConstraintsSpecification Constraints4Evaluation5ConclusionIntroduction Flume Boat Evaluation ConclusionDIFCDIFC: Decentralized Information Flow ControlApproaches, granularities of DIFC:The variable level, enforced by static analysis and typ esystems (JIF, JFlow), taint analysisThe process, system object level, enforced by OS mechanisms(Asbestos, HiStar, Flume)Introduction Flume Boat Evaluation ConclusionDIFC MechanismsSystem maintains a security label for every process, file.Label is a set of tags: randomly generated integers.An IPC instance from p to q depends on the labels of p and q.Processes can:Create tagsAdd or subtract tags from labelsAdd or subtract privileges from processesIntroduction Flume Boat Evaluation ConclusionA toy exampleIntroduction Flume Boat Evaluation ConclusionA DIFiCult problemDIFC programmers must be conscious of the current label setsand privilege sets of all processes and files.Guarantees that that code satisfies security and functionalityrequirements are difficult to think about.Introduction Flume Boat Evaluation ConclusionOur solution1Read a high-level specification describing a security policy.2Represent a specification as constraints over label variables.3Solve the constraints.4Rewrite source code, incorporating solution.Introduction Flume Boat Evaluation ConclusionOutline1Introduction2Flume3BoatDataflow ConstraintsSpecification Constraints4Evaluation5ConclusionIntroduction Flume Boat Evaluation ConclusionFlume backgroundWe’ve implemented our programming system on top of FlumeFlume is a complete DIFC system; today, we focus on socketsIntroduction Flume Boat Evaluation ConclusionSockets illustratedflume_socketpair(&fd,&their_tok)...spawn(&their_tok, ...)...write(fd)fd = flume_claim_socket(tok)...x = read(fd)Introduction Flume Boat Evaluation ConclusionFlume BasicsFlume always ensures that the file descriptor label equals theprocess label.If P writes to Q, it ensures that SP⊆ SQ.Processes with privileges may add or drop security tags.Introduction Flume Boat Evaluation ConclusionOutline1Introduction2Flume3BoatDataflow ConstraintsSpecification Constraints4Evaluation5ConclusionIntroduction Flume Boat Evaluation ConclusionSolution: A (slightly) deeper lookA multi-phase solution:1Generate constraints relating program points2Generate constraints representing the user specification3Munge those constraints together4Solve the constraints5Rewrite code reflec ting the s olutionIntroduction Flume Boat Evaluation ConclusionIntraprocess analysispid = spawn()if (...)write(...)else...spawn(...)1For every relevant program point, generate a variable.2Use standard dataflow (compile-time) analysis to determinerelevant pairs (u, v).3In above example: (1, 2), (1, 3), (2, 3).Introduction Flume Boat Evaluation ConclusionIntraprocess constraintsS+is the set of positive privilegesS−is the set of negative privilegesFor each pair, generate constraints:v ⊆ u ∪ S+u ⊆ v ∪ S−Introduction Flume Boat Evaluation ConclusionProgram AnnotationsPrograms must be annotated with extra “advice” for the analysis:a family name for each spawn program point and the destinationfamily for each write.spawn(arglist) becomesspawn("familyname", arglist)write(arglist) becomeswrite("familyname", arglist)"familyname" must be a constant in both instancesIntroduction Flume Boat Evaluation ConclusionSpecification LanguageDefines relationships between process families and acrosschild-parent relations.Examples:A : B: A processes may spawn B processes.A -> B: An A process can reach B processes.A !-> B: An A process can never reach B processes.B !-> B: Two B processes can never reach each other.Introduction Flume Boat Evaluation ConclusionSpecification Language (more examples)A -> *B: An A process can reach its B children.A !-> \B: An A process can never reach B processes thataren’t its children.Introduction Flume Boat Evaluation ConclusionSpecification Constraint GenerationFirst, generate a forest of representative processes:1Every family is represented by at least one process.2Every process that might spawn a B process has two Bchildren.Introduction Flume Boat Evaluation ConclusionSpecification Constraint GenerationIf the spec file says that process P in this forest can reachprocess Q, then generate the constraint (u ⊆ v) for every pairof program points u in P and v in Q where P might write toQ.If the spec file says that process P cannot reach Q, thengenerate the constraint (u 6⊆ v ) for every pair of programpoints u in P and v in Q.Introduction Flume Boat Evaluation ConclusionSolving ConstraintsNow have a set of constraints all of the form A ⊆ B ∪ C orA ⊆ B or A 6⊆ BWork by Rehof and Mogenson directly implies that a solutionis NP-hard to find in generalWe “cheat” using extra knowledge from the problem domainIntroduction Flume Boat Evaluation ConclusionSolving Constraints1The constraints from analysis of the control flow graph andthe analysis of the specification are combined, and theresultant constraint system is solved:Introduction Flume Boat Evaluation ConclusionSolving Constraints1The constraints from analysis of the control flow graph andthe analysis of the specification are combined, and theresultant constraint system is solved:Introduction Flume Boat Evaluation ConclusionOutline1Introduction2Flume3BoatDataflow ConstraintsSpecification Constraints4Evaluation5ConclusionIntroduction Flume Boat Evaluation ConclusionImplementationImplemented as Boat, a CIL extension. Consists of modules for:Analyzing an annotated programParsing a specificationSolving constraintsRewriting code (incomplete... for now)Introduction Flume Boat Evaluation ConclusionFlumeWikiFlumeWiki: a security conscious version of MoinMoin:Introduction Flume Boat Evaluation ConclusionFlumeWiki codeThe relevant snippet from the original cgilaunch.c:rc = flume_socketpair (&input, &fdhandles->val[0], ...);/* setup CGI’s labelset */S_label = label_alloc (1);rc = label_set (S_label, 0, S_handle);labs = labelset_alloc ();rc = labelset_set_S (labs, S_label);/* spawn the CGI */rc = flume_spawn_legacy (labs, fdhandles, ...);/* send form information to cgi */if (cgl_form_len ())