Automated Synthesis of Run-time Monitors to Enforce Authorization Policies in Business Processes

un-time monitors are crucial to the development of security-aware workflow management systems, which need to mediate access to their resources by enforcing authorization policies and constraints, such as Separation of Duty. In this paper, we introduce a precise technique to synthesize run-time monitors capable of ensuring the successful termination of workflows while enforcing authorization policies and constraints. An extensive experimental evaluation shows the scalability of our technique on the important class of hierarchically specified security-sensitive workflows with several hundreds of tasks.