Solving Multi-Objective Workflow Satisfiability Problems with Optimization Modulo Theories Techniques

ABSTRACT

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.

References

1. M. Abadi. Logic in Access Control (Tutorial Notes). Springer, 2009.
2. A. Adriansyah, B. van Dongen, and N. Zannone. Controlling break-the-glass through alignment. ASE Science Journal, 2(4):198--212, 2013.
3. A. Armando and S.E. Ponta. Model checking of security-sensitive business processes. In Proc. of FAST, 2009.
4. D. Basin, S.J. Burri, and G. Karjoth. Optimal workflow-aware authorizations. In Proc. of SACMAT, 2012.
5. E. Bertino, E. Ferrari, and V. Atluri. The specification and enforcement of authorization constraints in workflow management systems. TISSEC, 2(1):65--104, 1999.
6. C. Bertolissi, D.R. dos Santos, and S. Ranise. Automated synthesis of run-time monitors to enforce authorization policies in business processes. In Proc. of ASIACCS, 2015.
7. A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without bdds. In Proc. of TACAS, 1999.
8. N. Bjørner, A. Phan, and L. Fleckenstein. (ν)z - an optimizing SMT solver. In Proc. of TACAS, 2015.
9. L. Compagna, D.R. dos Santos, S.E. Ponta, and S. Ranise. Cerberus: Automated synthesis of enforcement mechanisms for security-sensitive business processes. In Proc. of TACAS, 2016.
10. J. Crampton. A reference monitor for workflow systems with constrained task execution. In Proc. of SACMAT, 2005.
11. J. Crampton and G. Gutin. Constraint expressions and workflow satisfiability. In Proc. of SACMAT, 2013.
12. J. Crampton, G. Gutin, and D. Karapetyan. Valued workflow satisfiability problem. In Proc. of SACMAT, 2015.
13. J. Crampton, G. Gutin, D. Karapetyan, and R. Watrigant. The bi-objective workflow satisfiability problem and workflow resiliency. JCS, 25(1):83--115, 2017.
14. J. Crampton, G. Gutin, and R. Watrigant. On the satisfiability of workflows with release points. In Proc. of SACMAT, 2017.
15. J. Crampton, G. Gutin, and A. Yeo. On the parameterized complexity of the workflow satisfiability problem. In Proc. of CCS, 2012.
16. J. Desel and W. Reisig. Place or transition petri nets. In Lectures on Petri Nets I: Basic Models, Advances in Petri Nets. Springer, 1996.
17. The Sage Developers. SageMath, the Sage Mathematics Software System, 2017. http://www.sagemath.org.
18. R.M. Dijkman, M. Dumas, and C. Ouyang. Semantics and analysis of business process models in bpmn. Inf. and Soft. Tech., 50(12):1281 -- 1294, 2008.
19. D.R. dos Santos and S. Ranise. On run-time enforcement of authorization constraints in security-sensitive business processes. In Proc. of SEFM, 2017.
20. D.R. dos Santos and S. Ranise. A survey on workflow satisfiability, resiliency, and related problems. CoRR, abs/1706.07205, 2017.
21. D.R. dos Santos, S. Ranise, L. Compagna, and S. E. Ponta. Assisting the Deployment of Security-Sensitive Workflows by Finding Execution Scenarios. In Proc. of DBSec, 2015.
22. J. Dubrovin, T.A. Junttila, and K. Heljanko. Exploiting step semantics for efficient bounded model checking of asynchronous systems. Sci. Comput. Program., 77(10--11):1095--1121, 2012.
23. H.B. Enderton. A Mathematical Introduction to Logic. Academic Press, New York-London, 1972.
24. V.K. Garg. Maximal antichain lattice algorithms for distributed computations. In Proc. of ICDCN, 2013.
25. M. Gario and A. Micheli. pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms. In SMT Workshop, 2015.
26. J. Holderer, R. Accorsi, and G. Müller. When four-eyes become too much: a survey on the interplay of authorization constraints and workflow resilience. In Proc. of SAC, 2015.
27. D. Karapetyan, A. J. Parkes, G. Gutin, and A. Gagarin. Pattern-based approach to the workflow satisfiability problem with user-independent constraints. CoRR, abs/1604.05636, 2016.
28. M. Leitner and S. Rinderle-Ma. A systematic review on security in process-aware information systems--constitution, challenges, and future directions. Inf. and Soft. Tech., 56(3):273--293, 2014.
29. J.C. Mace, C. Morisset, and A. Moorsel. Quantitative workflow resiliency. In Proc. of ESORICS, 2014.
30. R.T. Marler and J.S. Arora. Survey of multi-objective optimization methods for engineering. Structural and Multidisciplinary Optimization, 26(6):369--395, 2004.
31. A. Roy, S. Sural, A.K. Majumdar, J. Vaidya, and V. Atluri. Minimizing organizational user requirement while meeting security constraints. ACM Trans. Manage. Inf. Syst., 6(3):12:1--12:25, 2015.
32. R. Sebastiani and P. Trentin. OptiMathSAT: A Tool for Optimization Modulo Theories. In Proc. of CAV, 2015.
33. W.M.P. van der Aalst, A.H.M. ter Hofstede, B. Kiepuszewski, and A.P. Barros. Workflow patterns. Distributed Parallel Databases, 14(1):5--51, 2003.
34. Q. Wang and N. Li. Satisfiability and resiliency in workflow authorization systems. TISSEC, 13, 2010.
35. M. Weske. Business Process Management: Concepts, Languages, Architectures. Springer, Secaucus, NJ, USA, 2007.

Index Terms

• Security and privacy

  • Formal methods and theory of security

  • Software and application security

    • Software security engineering