Auto Labeling for Fun and Profit Matt Elder Bill Harris University of Wisconsin Madison elder wrharris cs wisc edu CS 736 Advanced Operating Systems Final Presentation Introduction Flume Outline 1 Introduction 2 Flume 3 Boat Dataflow Constraints Specification Constraints 4 Evaluation 5 Conclusion Boat Evaluation Conclusion Introduction Flume Boat Evaluation Conclusion DIFC DIFC Decentralized Information Flow Control Approaches granularities of DIFC The variable level enforced by static analysis and type systems JIF JFlow taint analysis The process system object level enforced by OS mechanisms Asbestos HiStar Flume Introduction Flume Boat Evaluation Conclusion DIFC Mechanisms System 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 tags Add or subtract tags from labels Add or subtract privileges from processes Introduction A toy example Flume Boat Evaluation Conclusion Introduction Flume Boat Evaluation Conclusion A DIFiCult problem DIFC programmers must be conscious of the current label sets and privilege sets of all processes and files Guarantees that that code satisfies security and functionality requirements are difficult to think about Introduction Flume Boat Evaluation Our solution 1 Read a high level specification describing a security policy 2 Represent a specification as constraints over label variables 3 Solve the constraints 4 Rewrite source code incorporating solution Conclusion Introduction Flume Outline 1 Introduction 2 Flume 3 Boat Dataflow Constraints Specification Constraints 4 Evaluation 5 Conclusion Boat Evaluation Conclusion Introduction Flume Boat Evaluation Conclusion Flume background We ve implemented our programming system on top of Flume Flume is a complete DIFC system today we focus on sockets Introduction Flume Boat Evaluation Conclusion Sockets illustrated flume socketpair fd their tok spawn their tok write fd fd flume claim socket tok x read fd Introduction Flume Boat Evaluation Conclusion Flume Basics Flume always ensures that the file descriptor label equals the process label If P writes to Q it ensures that SP SQ Processes with privileges may add or drop security tags Introduction Flume Outline 1 Introduction 2 Flume 3 Boat Dataflow Constraints Specification Constraints 4 Evaluation 5 Conclusion Boat Evaluation Conclusion Introduction Flume Boat Evaluation Solution A slightly deeper look A multi phase solution 1 Generate constraints relating program points 2 Generate constraints representing the user specification 3 Munge those constraints together 4 Solve the constraints 5 Rewrite code reflecting the solution Conclusion Introduction Flume Boat Evaluation Intraprocess analysis pid spawn if write else spawn 1 For every relevant program point generate a variable 2 Use standard dataflow compile time analysis to determine relevant pairs u v 3 In above example 1 2 1 3 2 3 Conclusion Introduction Flume Boat Intraprocess constraints S is the set of positive privileges S is the set of negative privileges For each pair generate constraints v u S u v S Evaluation Conclusion Introduction Flume Boat Evaluation Conclusion Program Annotations Programs must be annotated with extra advice for the analysis a family name for each spawn program point and the destination family for each write spawn arglist becomes spawn familyname arglist write arglist becomes write familyname arglist familyname must be a constant in both instances Introduction Flume Boat Evaluation Specification Language Defines relationships between process families and across child 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 Conclusion Introduction Flume Boat Evaluation Specification Language more examples A B An A process can reach its B children A B An A process can never reach B processes that aren t its children Conclusion Introduction Flume Boat Evaluation Specification Constraint Generation First generate a forest of representative processes 1 Every family is represented by at least one process 2 Every process that might spawn a B process has two B children Conclusion Introduction Flume Boat Evaluation Conclusion Specification Constraint Generation If the spec file says that process P in this forest can reach process Q then generate the constraint u v for every pair of program points u in P and v in Q where P might write to Q If the spec file says that process P cannot reach Q then generate the constraint u 6 v for every pair of program points u in P and v in Q Introduction Flume Boat Evaluation Conclusion Solving Constraints Now have a set of constraints all of the form A B C or A B or A 6 B Work by Rehof and Mogenson directly implies that a solution is NP hard to find in general We cheat using extra knowledge from the problem domain Introduction Flume Boat Evaluation Solving Constraints 1 The constraints from analysis of the control flow graph and the analysis of the specification are combined and the resultant constraint system is solved Conclusion Introduction Flume Boat Evaluation Solving Constraints 1 The constraints from analysis of the control flow graph and the analysis of the specification are combined and the resultant constraint system is solved Conclusion Introduction Flume Outline 1 Introduction 2 Flume 3 Boat Dataflow Constraints Specification Constraints 4 Evaluation 5 Conclusion Boat Evaluation Conclusion Introduction Flume Boat Evaluation Implementation Implemented as Boat a CIL extension Consists of modules for Analyzing an annotated program Parsing a specification Solving constraints Rewriting code incomplete for now Conclusion Introduction Flume Boat Evaluation FlumeWiki FlumeWiki a security conscious version of MoinMoin Conclusion Introduction Flume Boat Evaluation Conclusion FlumeWiki code The 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 rc if spawn the CGI flume spawn legacy labs fdhandles send form information to cgi cgl form len rc write input Introduction Flume BoatWiki specification wikilaunch wiki wikilaunch wiki wikilaunch wiki wiki wiki Boat Evaluation Conclusion Introduction Flume Boat Evaluation Conclusion