||Business processes, or workflows, are among the key intangible assets of a company. A workflow defines various activities of an enterprise in terms of certain
well-defined tasks. Users according to organizational rules execute these tasks.
A major concern in workflow execution is security; in case of process automation, where resources are readily accessible, it becomes even more important
to ensure that the right information is visible only for right people. As workflows and their results have enormous impact on the enterprise, they need to be
secured against external and internal security threats. Resilience to attacks usually comes in a form of assurance that certain security properties are satisfied.
Security properties of a system are expressed in terms of a security policy.
In this work we provide all the necessary ingredients of a framework that would
allow for checking if a workflow system is adhering to a specified security policy. Namely, we provide a formalism for modelling workflow systems, means
to specify and enforce security policy, and, finally, a methodology for checking
adherence to a security policy.
The first contribution of this work is that a fragment of BPEL, a language for
defining and executing business processes, is modelled in a process algebra which
we named KlaimWS; it belongs to the Klaim family of process calculi [16, 5, 8].
To ease the process of modelling, we equipped KlaimWS with structures whose
syntax and semantics closely matches the syntax and semantic of their BPEL
counterparts. The level of abstraction provided by KlaimWS allows to focus
solely on the core aspects of BPEL, omitting its cumbersome XML syntax.
Additionally, we consider AspectK, an extension of KlaimWS. AspectK
augments KlaimWS by introducing the notion of aspects as in Aspect Oriented Programming (AOP). The separation of concerns advocated by the AOP
paradigm permits clear separation between the application code and the security
policy. Security policies are encoded as aspects and then inlined into the main
code. The AspectK language structures are generic enough to allow expressing
various security models e.g. Role-Based Access Control (RBAC).
The second and main contribution of this work is the development of a static
analysis for checking adherence of workflow system to a security policy. The
analysis is specified using flow logic which is an approach to static analysis
that separates the specification of when an analysis estimate is acceptable for a
program from the actual computation of the analysis information . We also
establish two theoretical properties of the analysis. Namely, subject reduction
result and adequacy.