Biblio

Security-sensitive workflows impose constraints on the control-flow and authorization policies that may lead to unsatisfiable instances. In these cases, it is still possible to find "least bad" executions where costs associated to authorization violations are minimized, solving the so-called Multi-Objective Workflow Satisfiability Problem (MO-WSP). The MO-WSP is inspired by the Valued WSP and its generalization, the Bi-Objective WSP, but our work considers quantitative solutions to the WSP without abstracting control-flow constraints. In this paper, we define variations of the MO-WSP and solve them using bounded model checking and optimization modulo theories solving. We validate our solutions on real-world workflows and show their scalability on synthetic instances.

Resiliency is a relatively new topic in the context of access control. Informally, it refers to the extent to which a multi-user computer system, subject to an authorization policy, is able to continue functioning if a number of authorized users are unavailable. Several interesting problems connected to resiliency were introduced by Li, Wang and Tripunitara [13], many of which were found to be intractable. In this paper, we show that these resiliency problems have unexpected connections with the workflow satisfiability problem (WSP). In particular, we show that an instance of the resiliency checking problem (RCP) may be reduced to an instance of WSP. We then demonstrate that recent advances in our understanding of WSP enable us to develop fixed-parameter tractable algorithms for RCP. Moreover, these algorithms are likely to be useful in practice, given recent experimental work demonstrating the advantages of bespoke algorithms to solve WSP. We also generalize RCP in several different ways, showing in each case how to adapt the reduction to WSP. Li et al also showed that the coexistence of resiliency policies and static separation-of-duty policies gives rise to further interesting questions. We show how our reduction of RCP to WSP may be extended to solve these problems as well and establish that they are also fixed-parameter tractable.