Verification of policy compliance in workflows.

The Workflow Privacy Modeling Language (WPML) is a modeling language aimed for multi aspect design of information systems in the paradigm of the Service Oriented Architecture (SOA). The set of concepts describing system functionality is extended with organization and deployment aspects to allow for verification of multiple aspects of the system and generation of executable system and deployment instructions. The modeling language is provided with model interpreters to verify model correctness using the structural semantics approach, and HIPAA compliance checker facilitating the rules encoded in Prolog.

Language description:

The primary aspect of the WPML named Workflow is used to describe the data producers and consumers represented as Services and data passed between them represented as Messages. Services in the workflow are described using the external Web Service Definition Language documents specified in the WSDL attribute.
Messages in the workflow model represent the data transferred between the services. Messages define the structure of the data using predefined basic types and custom compound types. Additionally, message models carry semantic information about the data using the set of attributes {To, From, About, Type, Purpose, ReplyTo, ConsentedBy, Belief}.
Messages and services are composed using two types of associations: SendMessage and ReceiveMessage. The first is used to describe creation of the Message by a Service. The second denotes consumption of the Message by a Service. An example workflow model is presented in figure 1.

Figure 1 Simple producer consumer workflow model

A “producer” service creates “token” message which is consumed by the “consumer” service.

The design of the workflows is unconstrained and creation of cyclic message flows is allowed as shown in Figure 2.

Figure 2 Cyclic workflow model

Description of inter-organizational workflows requires abstractions to describe the relations between the communicating entities. In the Business Relations aspect services are bound to organizational units represented as Entities using the association Entity Mapping. This association represents the information about responsibilities of the organization for data producers and consumers, and transitively for the exchanged data.

Figure 3 Organization model

Figure 3 presents a simple organization model with two entities “ACME USA” and “ACME International” that are responsible for services “Producer” and “Consumer”. The Business relationship association carries additional information in the attribute purpose, which specifies what the objectives of the given relationship are. The Entity objects are described with the role attribute which allows specifying the role played by a given entity.Finally, the Deployment aspect is used to specify the deployment and network connectivity. In this aspect new object Node represents the platform on which services are deployed. The binding between the services and the nodes is represented using the Deployment association, and network connectivity is modeled using the Network Connection association. Currently nodes do not contain any additional information; however we plan on adding more details for describing the deployment process. The network connection contain Boolean value secure used to specify if the connection used between the nodes is secured (for example using SSL, VPN, the implementation details are irrelevant for this level of abstraction). An example network model is shown in the figure 4. The “Producer” service is deployed to “ACME Server” and the “Consumer” service is deployed to “ACME Client”. The nodes are connected using unsecure connection.

Figure 4 Deployment model

Example Model with privacy and security policies

The workflow model presented in Figure 5 represents a system used for monitoring patients outside of the hospitals. In this scenario two services are used to monitor patient vital signs: N800 web client and N800 sensor data collection service. The two services send out the data web service vitals and sensor vitals to the respective data gateway services – web service data gateway and sensor data gateway. Gateway services process the data and send processed information patient vitals to the service responsible for storing the information Data Access Object. The stored patient data may be accessed by the patient monitoring service CPM runtime environment using the message exchange: patient data request, collected patient information. The retrieved information is used to generate the recommendations for the patient sent in the recommendations for patient message. The model represents one more sub-workflow that may be initiated by the patient monitoring service which is denoted by the exchange of the messages assistance request and assistance response between the CPM runtime environment and Clinical Specialist.

Figure 5 Workflow model for the outpatient monitoring scenario

In figure 5 details of the message objects are not visible, however their attributes are set to reflect the carried information – for example the web service vitals message attributes are set as follows: {To=OutpatientServiceProvider, From=patient, About=patient, Type=PHI, Purpose=null, ReplyTo=null, ConsentedB=null, Belief=null}. This attributes will allow for the verification of the compliance of the messages exchanged in the workflow with the HIPAA rules and additional policies defined in the model.

The organization model represents the business relations between the entities and in the model depicted in figure 6 we specify roles played by the entities and purpose of the relationships. The patient entity has the following values of attributes {role=individual;adult} and this information is used for checking the HIPAA compliance of the workflows. The description of remaining objects is omitted for brevity.

Figure 6 Organization model for the example scenario

The deployment information is presented in the deployment aspect of the model. The example system is deployed onto multiple nodes connected in a network. The network in the example is not fully connected which reflects the network architecture with un-trusted client (ClientTablet), de-militarized zone gateway (WebService Server), and nodes on the internal network (DBServer, PhysicianPC, Consultant PC).

Figure 7 Deployment model with policy annotations

With all the information in the model one can define the system policies that will be represented as the structural constraints. The policies that will be applied to all the systems build in the domain should be injected into the domain description generated from the metamodel. The policies specific for a given instance should be introduced in the models in form of annotations. The presented example is a latter case – the textual representation of the policies is visible in the Figure 7 underneath the deployment diagram.
The policies used in the model are following the convention introduced in {EJackson structural semantics} and described in {JWernerMothis2008}. The policies are as follows:

1.  Messages containing protected health information may be sent only over secure network connections

2.  Messages containing protected health information may be sent only between the entities that have the contractual agreement

The first rule has the following representation in the syntax
no_entity_connection(E1,E2,R) :- R = entityconnection(_,E1,E2), (E1\==E2), \+ entityconnection(X,E1,E2),\+ entityconnection(X,E2,E1).
malform(message(M),R) :- message(M),sendmessage(MF,S1,M), receivemessage(MF2,M,S2),entitymapping(EM1,S1,E1), entitymapping(EM2,S2,E2),no_entity_connection(E1,E2,R).
The rule uses an auxiliary symbol no_entity_connection which is deduced from the terms generated from the models. This helper rule is used to show model correctness by
The second rule is encoded as follows:
networkconnected(M1,M2,NC) :- networkconnection(NC,M1,M2); networkconnection(NC,M2,M1).
insecure_link(M,R) :- R = secure(NC,'insecure network connection'), sendmessage(MF,S1,M),type(M,X), (X=='phi'), receivemessage(MF2,M,S2),deploymentconnection(DC1,S1,M1), deploymentconnection(DC2,S2,M2), networkconnected(M1,M2,NC), secure(NC,Y), (Y == 'false').
malform(message(M),R) :- insecure_link(M,R).
The second rule use two helper symbols networkconnected and insecure_link that are then used in the malform rule.

Model verification

To describe the policies for the workflows we have to generate the domain description using the structural semantics approach. To generate the domain definition one has to use the Prolog Domain Generator Interpreter available for the MetaGME metamodels. The first required step is to use the MetaGME MetaInterpreter to generate the domain definition, register it in the system and create the auxiliary files. Following that step one needs to invoke the domain generator interpreter and point it to the domain definition file (the auxiliary .xmp file). This step generates the domain definition in prolog. Modeling concepts are translated to set of terms and rules over them representing the structure of the modeling language. This definition will be used as a base to define policies applied to workflow models and verify the model correctness (in general, the logical representation of a domain allows for defining any constraints over the models in the domain). After registering the domain specific language and generating the logic definition of a domain designer can build the models in the domain and specify policies in form of domain constraints. We demonstrate the workflow development process on the example drawn from the clinical information systems domain. In the example we build a model of the outpatient monitoring system with non-trivial deployment and organization models and annotate the models with the structural constraints representing security and privacy policies. Additionally we demonstrate how the given model may be verified against the set of HIPAA rules encoded in Prolog and how the development tools suggest the changes to the model to make it conformant the rules.

Evaluation of the policies is performed using following steps:

-  Model is translated to set of terms in Prolog

-  Domain definition is loaded from the file generated from the language definition model

-  Model specific policies taken from the model annotations are injected into the domain definition.

-  Logical representation of the model is verified against a set of rules defining the domain using the Prolog solver, and the model is deemed correct if no symbols denoting that model stating incorrectness may be derived.

Figure 8 Results of stuctural constraints validation

The tool for model verification and the results for presented model are shown in the figure 8. The result of verification shows that model violate constraints: there are messages sent between the services over the insecure links. The model verification fails on the first rule presented above – protected health information is sent over insecure links. To fix this violation, model designer has to modify the network diagram and modify the network association attributes to {secure=true}. The organization model contains all the required associations between entities, consequently the second rule is never violated.

The introduction of the data metainformation in terms of attributes of messages, allows for the automated HIPAA compliance checking using the HIPAA policy encoding in Prolog.

Figure 9 Results of verification of HIPAA compliance


Biblography

Stanford University representation of HIPAA privacy rule in Prolog http://crypto.stanford.edu/privacy/HIPAA/

Jackson E.K., Sztipanovits J.: Towards a Formal Foundation for Domain Specific Modeling Languages, Proceedings of the 6th ACM International Conference on Embedded Software (EMSOFT’06), Seoul, South Korea, October 2006.

Werner J., Malin B, Lee Y., Ledeczi A, Sztipanovits J. "Integration of Clinical Workflows with Privacy Policies on a Common Semantic Platform", 2nd International Workshop on Model-Based Design of Trustworthy Health Information Systems (MOTHIS 2008), Toulouse, France, September 2008.