Security (Hyper-)properties in Workflow Systems: From Specification to Verification.

Provable security guarantees for software systems are highly desirable. Our work aims at improving and integrating existing formal verification techniques into a framework for the specification and verification of typical security requirements of large-scale, distributed workflow systems. Challenges include the uniform modelling of different types of security requirements, the decomposition of global security requirements into requirements on subcomponents, and the refinement of an abstract specification towards an implementation. We focus our attention on workflow management systems due to their interesting security requirements and the widespread use of model-driven techniques in this area (e.g. using BPMN diagrams). We build upon existing verification techniques for a specific notion of information flow security, and intend to apply our results to concrete example systems such as a secure web-based conference management system.