Conformance Verification of Privacy Policies
In this detailed presentation, Xiang Fu, an Assistant Professor at Hofstra University, explores the conformance verification of privacy policies and the framework for privacy properties in temporal logic verification. The content covers the challenges, PV framework, data models, examples, and actions involved in privacy verification in the context of web applications and online information handling.
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.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
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.
E N D
Presentation Transcript
Conformance Verification of Privacy Policies Xiang Fu Assistant Professor Department of Computer Science Hofstra University
Outline Motivation PV Framework Privacy Properties in Temporal Logic Verification using Alloy Conclusion
Web App: Consumer and Producer of INFORMATION Online Marketing Email SSN SSN Credit Card Medical Record Address Shopping Preference Identity Collection Web App Shopping Habits Business Partners
Privacy Verification Problem Your SSN never be forwarded CC destroyed after transaction Web App Function as PROMISED?
Challenges Servlets Servlets Business Procedures DB Ops P3P Privacy Policy Model Checker
PV Framework Privacy Verification Framework 1. Servlet Control/Data Flow 2. Information Flow 3. Data Operations
Data Model Operator Servlet Database Business Organization Stakeholder Atomic Real-Being Entity Countable Set CC Card SSN Med Record Transaction ID Name Primitive Type System Data Item Flattened Model
Example: Bookstore App Entities
Example: Bookstore App Data Types
Actions At any moment for any e and d, Know(e,d) is defined Know(e, d) entity Action: transition system expressed using first order on Know predicates data
Example: Charge Credit Card Free var, input variable CC ( cc know' ) know' ( ) DB,cc Bank,cc = { , } know' : ( ) know' ( ) x DB BANK d D x,d x,d All data All entities { : } cc d D know( = = know' ( ) ) know' ( ) know( ) DB,d DB,d Bank,d Bank,d
Modeling Privacy Policy Typical Examples: P3P and EPAL Defines: (1) What to protect? (2) Who can receive it? (3) How long?
Temporal Logic for P3P CTL-FO = CTL + First Order Quantifiers Credit Card Info Regularly Purged from DB & is not leaked AF( know( CC AG( : know( , ) ) d : , )) d DB x E x d for any credit card for any entities
Verification (1) Translate from PV to Alloy (2) Translate CTL-FO to Alloy Predicates (3) Verification using Alloy
Modeling World Schema module bookstore //1. world schema abstract sig Object {} abstract sig WA, Env, Data extends Object {} abstract sig Actions, Entities extends WA {} Set of All Data Items Web App. Servlets
Modeling System State Model the transition relation sig State{ know: (WA + Env) -> Data, prev: one State, actstate: Actions -> actionStatus }{ all x: Actions | some status: actionStatus | x -> status in actstate }
Modeling Action pred pChargeCC[s,s : State, d:CC]{ ChargeCC->READY in s.actstate and ( s .know = s.know + {DB->d} + {Bank->d} && s .prev=s && s .actstate = s.actstate - .. ) }
Modeling CTL-FO Formula pred ef[s:State, d:Data]{ some s : State | (CEO->d in s .know) && s in s .*prev } pred fa[s:State]{ all d: Data | (DB->d in s.know) => ef[s,d] } assert AGProperty{ all s: State | fa[s] }
Initial Experiments 20 Objects State Clauses Constr. Time (ms) 2203 7984 18782 - Solver Time (ms) 781 6266 40828 - 5 10 15 20 431k 1928k 4504k -
Conclusion PV Framework for Reasoning about Privacy Verification Paradigm using Alloy Problems
Future Directions (1) Static Program Analysis Path Transducer Model (Servlet) Information Flow (Business Rules, Access Right Policies) (2) Customized Relational Constraint Solvers
