Automated Privacy Enforcement System Presentation
Explore a comprehensive overview of a language designed to automatically enforce privacy policies, presented by Jean Yang. The system aims to simplify the process of preserving user data confidentiality, addressing concerns such as displaying user locations, fine-grained policies, and programmer burdens. Learn about the challenges, solutions, and the state-of-the-art Jeeves system in privacy enforcement.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
A Language for Automatically Enforcing Privacy Jean Yang with KuatYessenov andArmando Solar-Lezama
Displaying User Locations to Other Users getLocation? Jean Yang @ POPL 2
No Privacy Concerns Whatever! A A Secret club getLocation Secret club Alice def getLocation (user: User): Location = user.location Jean Yang @ POPL 3
Simple policy Only my friends can see my location. getLocation A Owner Viewer Secret club A getLocation Alice Secret club Jean Yang @ POPL 4
Finer-Grained Policies Only members know this exists. Only my friends can see my location. Policy interaction? A A Secret club getLocation Diner Owner Locations Viewer Alice Which policies apply where? Jean Yang @ POPL Not a member! 5
Programmer Burden Output Context def getLocation (user: User) (viewer: User) : Location = { if (isFriends user viewer) { if (canSee user.location viewer) { user.location; } else { scrub(user.location, Diner ); } } else { undisclosedLocation; } } Views of sensitive values Policies Jean Yang @ POPL 6
Our Mission Make it easier for the programmer to preserve confidentiality of user data. Jean Yang @ POPL 7
Whats Hard? Data Function Programmer check/filter Functionality and policy are intertwined. Scrubbed data Function Programmer check/filter Scrubbed data Jean Yang @ POPL 8
Our Solution Separation of policies from functionality Policy Data Automatic enforcement Function Programmer check/filter Scrubbed data Tagged data Function Programmer check/filter Scrubbed data Jean Yang @ POPL 9
Jeeves Goal def getLocation (user: User) (viewer: User) : Location = { if (isFriends user viewer) { if (canSee user.location viewer) { user.location; } else { scrub(user.location, Work ); } } else { undisclosedLocation; } } State of the Art Jeeves def getLocation (user: User): Location = user.location Jean Yang @ POPL 10
Talk Outline Jeeves language How it works Coding in Jeeves Jean Yang @ POPL 11
Jeeves Language 1 2 Sensitive values Policies Policy Data 3 Automatic contextual enforcement Function Tagged data Function Scrubbed data Jean Yang @ POPL 12
Jeeves for Locations | Low confidentiality Secret club Diner High confidentiality A A Secret club Diner Jean Yang @ POPL 13
Using Jeeves Sensitive Values level a in { low, high } val location: String = < school | MIT >a Level variable High component Low component Policies policy a: context != alice low Core Functionality val msg: String = Alice is at + location Contextual Enforcement print {alice} msg /* Alice is at MIT */ print {bob} msg /* Alice is at school */ Jean Yang @ POPL 14
Talk Outline Jeeves language How it works Coding in Jeeves Jean Yang @ POPL 15
How Jeeves Works Constraints Symbolic values Symbolic evaluation Function Symbolic expressions Implicit parameter Function SMT solving Concrete value Jean Yang @ POPL 16
Representing Sensitive Values in Jeeves Without Jeeves Jeeves Name Alice Bob Claire Location MIT POPL POPL Name Location Alice ?|MIT a Bob POPL Claire ?|POPL b Policy Policy Jean Yang @ POPL 17
Symbolic Evaluation for Information Flow Name Location Alice | a Bob POPL Claire | b How many people are at POPL? Runtime Environment context != alice a = low b = low Outputs computed from sensitive values are symbolic & concretized under the policy 1 + ((x1 = POPL) ? 1 : 0) + ((x2 = POPL) ? 1 : 0) environment. Jean Yang @ POPL 18
Jeeves Non-Interference Guarantee Consider the sensitive value L |H a Level variable Low component High component Given a fixed L, all executions where a must be low produce equivalent outputs no matter the value of H. Jean Yang @ POPL 19
Standard Non-Interference H2 Hn H1 Hn-1 L a Does not depend on the H-value = low Program Does not depend on the H-value Output Jean Yang @ POPL 20
Jeeves Non-Interference H2 H1 Hn L Hn-1 a Depends on the H-value = low Program Cannot distinguish between H-values that imply a = low Output Jean Yang @ POPL 21
Jeeves Non-Interference L H a = low Program Program does not leak information about H. Programs to outputs? Output Jean Yang @ POPL 22
Language Restrictions Primitives and objects. No functions. Constraints Constraints Symbolic values Symbolic values Symbolic evaluation Boolean constraints with conditionals & implications. Arithmetic and Function Symbolic expressions No functions, quantifiers, or theory of lists. Function SMT solving Concrete value Jean Yang @ POPL 23
Static Checks Constraints Symbolic values Symbolic evaluation Function Function Symbolic values flow only where expected. Symbolic expressions expressions Symbolic Contexts are well-formed. Evaluation does not introduce nontermination. Function Function SMT solving Outputs are concrete. Concrete value Concrete value Jean Yang @ POPL 24
Stateful Policies Only people near me can see my location. policy a: (distance context alice > radius ) A low Secret club But Alice s location is changing Alice Jeeves: Delay policy evaluation until output. Jean Yang @ POPL 25
Jeeves System Policies Data Well-formed values. Evaluation produces well- formed values. Jeeves runtime Function Symbolic expressions Function Output Policies evaluated. Guarantee: outputs shown according to policies. Concrete value Jean Yang @ POPL 26
Scala Implementation Overload operators to create symbolic expressions. Use an SMT solver as a model finder. + SMT Solver v 3 print Delay evaluation of policies until output. = policy Runtime Environment v 2 Propagate policies. Jean Yang @ POPL 27
Talk Outline Jeeves language How it works Coding in Jeeves Jean Yang @ POPL 28
JConf Architecture Paper Title Author Reviews Tags Review Reviewer Content Policy Policy Context Viewer: User CStage: Stage Policy Policy Policy Policy User Policy Role Functionality Core Program Does not need to know about policies. Search papers. Display papers. Add and remove tags. Assign and submit reviews. Submission, review, rebuttal, decision, public Jean Yang @ POPL 29
Functionality vs. Policy File ConfUser.scala PaperRecord.scala 103 PaperReview.scala ConfContext.scala 6 Backend Total LOC Policy LOC 59 17 48 11 0 0 21 123 Frontend (Scalatra) 161 0 Total 473 76 Jean Yang @ POPL 30
Conclusions The Jeeves language: pushing responsibility of privacy to the runtime. How we designed a language with constraints using symbolic evaluation to provide execution guarantees. Evaluation of Jeeves in practice: conference management example. Website: Google Code:code.google.com/p/scalasmt Contact: jeanyang@mit.edu sites.google.com/site/jeevesprogramming Jean Yang @ POPL 31
