《Contextual Integrity and its Formalization：语境完整性及其形式化》由会员分享，可在线阅读，更多相关《Contextual Integrity and its Formalization：语境完整性及其形式化（54页珍藏版）》请在金锄头文库上搜索。
1、Contextual Integrity and its FormalizationAnupam Datta CMUFall 2007-08What do I do?uResearch Foundations (Modeling and Analysis) of Cryptographic protocols Privacy Secure systems Using methods from programming languages and cryptography Conferences: IEEE CSF, IEEE S andall negative norms are satisfi
2、edHIPAA Healthcare PrivacyHIPAA consists primarily of positive norms: share phi if some rule explicitly allows it (2), (3), (5), (6)Exception: negative norm about psychotherapy notes (4)COPPA Children Online PrivacyCOPPA consists primarily of negative norms children can share their protected info on
3、ly if parents consent (7) (condition)(8) (obligation future requirements)Sender roleSubject roleAttributeTransmission principleGLBA Financial InstitutionsRecipient roleFinancial institutions must notify consumers if they share their non-public personal information with non- affiliated companies, but
4、 the notification may occur either before or after the information sharing occursRelated LanguagesModelSenderRecipientSubjectAttributesPastFutureCombinationRBACRoleIdentityXACMLFlexibleFlexibleFlexibleooEPALFixedRoleFixedoP3PFixedRoleFixedooLPURoleRoleRoleLegend: unsupported opartially supported ful
5、ly supported LPU fully supports attributes, combination, temporal conditionsWhy Not Use P3P?uDifferent application P3P understood by web browsers LPU intended for internal policy enforcementuNot expressive enough P3P cannot express HIPAA, GLBA, COPPA Each policy only has one sender and one subject M
6、issing temporal conditions; only has simple opt-in / opt-outOutlineuMotivating Example uFramework uModel uLogic of Privacy and Utility uWorkflows and Responsibility uAlgorithmic Results uWorkflow Design assuming agents responsible uAuditing logs when agents irresponsible uConclusionsNurseSecretaryMy
7、HealthVanderbilt ImprovedPatientDoctorHealth AnswerHealth AnswerHealth QuestionAppointment RequestHealth QuestionNow that I have cancer, Should I eat more vegetables?Health QuestionYes! except broccoliHealth AnswerAssign responsibilities to roles & workflow engineDoctor should answer health question
8、sGraph-based WorkflowuGraph (R, R x R), where R is the set of roles uEdge-labeling functionpermit: R x R 2T, where T is the set of attributes uResponsibility of workflow engine Allow msg from role r1 to role r2 iff tags(msg) permit(r1, r2) uResponsibility of human agents in roles Tagging responsibil
9、ities ensure messages are correctly tagged Progress responsibilities ensure messages proceed through workflowMyHealth ResponsibilitiesuTagging Nurses should tag health questions G p, q, s, m. inrole(p, nurse) send(p, q, m) contains(m, s, health-question) tagged(m, s, health-question) uProgress Docto
10、rs should answer health questions G p, q, s, m. inrole(p, doctor) send(q, p, m) contains(m, s, health- question) F m. send(p, s, m) contains(m, s, health-answer)Abstract WorkflowuResponsibility of workflow engine LTL formula Feasible (enforceable) if is a safety formula without the contains() predic
11、ateuResponsibility of each role r LTL formula r Feasible if agents have a strategy to discharge their responsibilities p. inrole(p, r) rGraph-based workflows are a special caseOutlineuMotivating Example uFramework uModel uLogic of Privacy and Utility uWorkflows and Responsibility uAlgorithmic Result
12、s uWorkflow Design assuming agents responsible uAbstract workflows uAuditing logs when agents irresponsible uOnly graph-based workflows uConclusionsNurseSecretaryMyHealthVanderbilt ImprovedPatientDoctorHealth AnswerHealth AnswerHealth QuestionAppointment RequestHealth QuestionNow that I have cancer,
13、 Should I eat more vegetables?Health QuestionYes! except broccoliHealth AnswerMinimal disclosurePrivacy: HIPAA compliance+Utility: Schedule appointments, obtain health answersResponsibility: Doctor should answer health questionsWorkflow Design ResultsuTheorems: Assuming all agents act responsibly, c
14、hecking whether workflow achieves Privacy is in PSPACE (in the size of the formula describing the workflow) Utility is decidable uDefinition and construction of minimal disclosure workflowAlgorithms implemented in model-checkers, e.g. SPIN, MOCHADeciding PrivacyuPLTL model-checking problem is PSPACE
15、 decidableG |= tags-correct U agents-responsible privacy-policyG: concurrent game structureResult applies to finite models (#agents, msgs,) MyHealth PrivacyuMyHealthVanderbilt workflow satisfies this privacy conditionIn all states, only nurses and doctors receive health questionsG p1, p2, q, m send(
16、p1, p2, m) contains(m, q, health-question) inrole(p2, nurse) inrole(p2, doctor) uRun LTL model-checker, e.g. SPINDeciding UtilityuATL* model-checking of concurrent game structures is Decidable with perfect information Undecidable with imperfect information uTheorem: There is a sound decision procedure for de
