Skip to main content
SpringerLink
Log in

On Run-Time Enforcement of Authorization Constraints in Security-Sensitive Workflows

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10469))

Included in the following conference series:

Abstract

In previous work, we showed how to use an SMT-based model checker to synthesize run-time enforcement mechanisms for business processes augmented with access control policies and authorization constraints, such as Separation of Duties. The synthesized enforcement mechanisms are able to guarantee both termination and compliance to security requirements, i.e. solving the run-time version of the Workflow Satisfiability Problem (WSP). No systematic approach to specify the various constraints considered in the WSP literature has been provided. In this paper, we first propose a classification of these constraints and then show how to encode them in the declarative input language of the SMT-based model checker used for synthesis. This shows the flexibility of the SMT approach to solve the run-time version of the WSP in presence of different authorization constraints.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Notes

  1. 1.

    https://help.sap.com/hana-opint.

References

  1. Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. JSAT 8, 29–61 (2012)

    MathSciNet  MATH  Google Scholar 

  2. Alhaqbani, B., Adams, M., Fidge, C.J., ter Hofstede, A.H.M.: Privacy-aware workflow management. In: Proceedings of BPM, pp. 111–128. Springer, Heidelberg (2013)

    Google Scholar 

  3. Basin, D., Burri, S.J., Karjoth, G.: Dynamic enforcement of abstract separation of duty constraints. TISSEC 15(3), 13:1–13:30 (2012)

    Article  Google Scholar 

  4. Basin, D., Burri, S.J., Karjoth, G.: Obstruction-free authorization enforcement: Aligning security and business objectives. JCS 22(5), 661–698 (2014)

    Article  Google Scholar 

  5. Bell, D.: The bell-lapadula model. JCS 4(2), 3 (1996)

    Google Scholar 

  6. Bertino, E., Ferrari, E., Atluri, V.: The specification and enforcement of authorization constraints in workflow management systems. TISSEC 2(1), 65–104 (1999)

    Article  Google Scholar 

  7. Bertolissi, C., dos Santos, D.R., Ranise, S.: Automated synthesis of run-time monitors to enforce authorization policies in business processes. In: Proceedings of ASIACCS. ACM (2015)

    Google Scholar 

  8. Biba, K.: Integrity considerations for secure computer systems. Technical report, DTIC Document (1977)

    Google Scholar 

  9. Brewer, D., Nash, M.J.: The Chinese wall security policy. In: Proceedings of S&P. IEEE (1989)

    Google Scholar 

  10. Burri, S.J, Karjoth, G.: Flexible scoping of authorization constraints on business processes with loops and parallelism. In: Proceedings of BPMW. Springer (2012)

    Chapter  Google Scholar 

  11. Cohen, D., Crampton, J., Gagarin, A., Gutin, G., Jones, M.: Iterative plan construction for the workflow satisfiability problem. JAIR 51, 555–577 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  12. Cohen, D., Crampton, J., Gagarin, A., Gutin, G., Jones, M.: Algorithms for the workflow satisfiability problem engineered for counting constraints. J. Comb. Optim. 32(1), 3–24 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  13. Compagna, L., dos Santos, D.R., Ponta, S.E., Ranise, S.: Cerberus: Automated synthesis of enforcement mechanisms for security-sensitive business processes. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 567–572. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_36

    Chapter  Google Scholar 

  14. Crampton, J.: A reference monitor for workflow systems with constrained task execution. In: Proceedings of SACMAT. ACM (2005)

    Google Scholar 

  15. Crampton, J., Gagarin, A., Gutin, G., Jones, M., Wahlström, M.: On the workflow satisfiability problem with class-independent constraints for hierarchical organizations. TOPS 19(3), 81–829 (2016)

    Article  Google Scholar 

  16. Crampton, J., Gutin, G.: Constraint expressions and workflow satisfiability. In: Proceedings of SACMAT. ACM (2013)

    Google Scholar 

  17. Crampton, J., Gutin, G., Yeo, A.: On the parameterized complexity and kernelization of the workflow satisfiability problem. TISSEC 16(1), 4 (2013)

    Article  Google Scholar 

  18. Crampton, J., Huth, M., Kuo, J.: Authorized workflow schemas: deciding realizability through LTL(F) model checking. STTT 16(1), 31–48 (2014)

    Article  Google Scholar 

  19. Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 53–68. Springer, Heidelberg (2000). doi:10.1007/10722167_8

    Chapter  MATH  Google Scholar 

  20. Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Soft. Tech. 50(12), 1281–1294 (2008)

    Article  Google Scholar 

  21. dos Santos, D.R., Ranise, S., Ponta, S.E.: Modular synthesis of enforcement mechanisms for the workflow satisfiability problem: scalability and reusability. In: Proceedings of SACMAT. ACM (2016)

    Google Scholar 

  22. Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. LMCS 6(4) (2010)

    Google Scholar 

  23. Ghilardi, S., Ranise, S.: MCMT: A model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22–29. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14203-1_3

    Chapter  Google Scholar 

  24. Leitner, M., Mangler, J., Rinderle-Ma, S.: Definition and enactment of instance-spanning process constraints. In: Wang, X.S., Cruz, I., Delis, A., Huang, G. (eds.) WISE 2012. LNCS, vol. 7651, pp. 652–658. Springer, Heidelberg (2012). doi:10.1007/978-3-642-35063-4_49

    Chapter  Google Scholar 

  25. Li, N., Wang, Q.: Beyond separation of duty: An algebra for specifying high-level security policies. J. ACM 55(3), 121–1246 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  26. Nassr, N., Steegmans, E.: Mitigating conflicts of interest by authorization policies. In: Proceedings of SIN. ACM (2015)

    Google Scholar 

  27. Sandhu, R., Coyne, E., Feinstein, H., Youmann, C.: Role-based access control models. IEEE Comput. 2(29), 38–47 (1996)

    Article  Google Scholar 

  28. Sankaranarayanan, S., Sipma, H., Manna, Z.: Petri net analysis using invariant generation. In: Verification: Theory and Practice. Springer (2003)

    Google Scholar 

  29. Tan, K., Crampton, J., Gunter, C.A.: The consistency of task-based authorization constraints in workflow. In Proceedings of CSF. IEEE (2004)

    Google Scholar 

  30. van der Aalst, W.M.P., van Hee, K.M., ter Hofstede, A.H.M., Sidorova, N., Verbeek, H.M.W., Voorhoeve, M., Wynn, M.T.: Soundness of workflow nets: classification, decidability, and analysis. Formal Aspects Comp. 23(3), 333–363 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  31. Wang, Q., Li, N.: Satisfiability and resiliency in workflow authorization systems. TISSEC 13(4), 401–4035 (2010)

    Article  MathSciNet  Google Scholar 

  32. Warner, J., Atluri, V.: Inter-instance authorization constraints for secure workflow management. In: Proceedings of SACMAT (2006). ACM

    Google Scholar 

  33. Wolter, C., Schaad, A., Meinel, C.: Task-based entailment constraints for basic workflow patterns. ACM, In Proc. of SACMAT (2008)

    Book  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fondazione Bruno Kessler (FBK), Trento, Italy

    Daniel Ricardo dos Santos & Silvio Ranise

Authors
  1. Daniel Ricardo dos Santos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Silvio Ranise
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Daniel Ricardo dos Santos .

Editor information

Editors and Affiliations

  1. University of Trento, Trento, Italy

    Alessandro Cimatti

  2. Mälardalen University, Västerås, Sweden

    Marjan Sirjani

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

dos Santos, D.R., Ranise, S. (2017). On Run-Time Enforcement of Authorization Constraints in Security-Sensitive Workflows. In: Cimatti, A., Sirjani, M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science(), vol 10469. Springer, Cham. https://doi.org/10.1007/978-3-319-66197-1_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66197-1_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66196-4

  • Online ISBN: 978-3-319-66197-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation