Lead Institution: Vanderbilt University

Project Leader: Janos Sztipanovits

Research Progress

• Abstract
  The Policy Verification tool provides formal logic analysis capabilities for the policy models, use case models and their integration. The formal logic analysis is built on Microsoft Research FORMULA engine. Capabilities include checking consistency and entailment for policy sets, and formally proving that selected information use and disclosure models conform to selected privacy rules.

• Focus of the research/Market need for this project
  Current analysis of the consistency of privacy rules with models of actual information use and disclosure practices is not done or done manually. The system will provide an easy to use service for a wide range of health care organizations.

• Project Aims/Goals
  Establish a theoretical background for analyzing and verifying policy models with or without use case models and to provide a prototype implementation for such verification.

• Key Conclusions/Significant Findings/Milestones reached/Deliverables
  We have established the basic theoretical framework for policy verification using domain specific modeling, semantic anchoring and formal languages. The Policy Verification builds on both the PATRN Policy Authoring Environment and the UCAME Use Case Authoring and Modeling Environment and enables the models created in those environments to be analyzed and verified. The key concept that enables this analysis is semantic anchoring. With semantic anchoring it is possible to provide precise and formal semantics to the languages used in the modeling and composition. With the semantics anchored to the models it is possible to translate the models into a formal representation that can be reasoned on using a formal language analysis.

  

  Figure 3. The execution of a use case validation.

  We have created a prototype implementation of this policy verification paradigm that uses Microsoft Research’s FORMULA 2.0 as the verification engine. Using the Generative Integration Tool it is possible to generate FORMULA code from policy models and also from the use-case models. The GI Tool is capable of integrating the code generation from the use-case models and the policy models that are referenced in the use-case models. The generated FORMULA code is then transferred to the cloud deployment of the FORMULA engine and executed. The result of the analysis is then returned from the cloud to tool, which then displays the verification result to the user.

• Materials Available for Other Investigators/interested parties

  • The publication “A model-integrated authoring environment for privacy policies.” describing the theoretical framework is available online (see bibliography below).
  • The Policy Verification (POVER) engine prototype is available as part of the https://policyforge.org/ included in the project add-on tools for policy authoring and use case modeling with documentation in the policyforge help project.

• Market entry strategies
  PolicyForge.org is an open collaboration website that is similar to the established open source community sites such as SourceForge or GitHUB, but it is specifically tailored for policy formalization. We use the PolicyForge.org website to provide access to the prototype Policy Verification engine included in the Policy Authoring Environment and Use Case Modeling Environment. For more information see the Market Entry Strategy for the Policy Authoring Environment.

Bibliography
PolicyForge: A Collaborative Environment for Formalizing Privacy Policies in Health Care
Andras Nadas, Laszlo Juracz, Janos Sztipanovits, Mark E. Frisse, and Ann J. Olsen
Software Engineering in Health Care (SEHC), 5th International Workshop, May 2013

A Model-Integrated Authoring Environment for Privacy Policies
Andras Nadas, Tihamer Levendovszky, Ethan K. Jackson, Istvan Madari, and Janos Sztipanovits
Science of Computer Programming, January 2013

Modeling Privacy Aware Health Information Exchange Systems
Andras Nadas, Mark E. Frisse, and Janos Sztipanovits
The 1st International Workshop on Engineering EHR Solutions (WEES) at Amsterdam Privacy Conference 2012, Amsterdam, the Netherlands; October 2012