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.

On run-time enforcement of authorization constraints in security-sensitive Workflows / dos Santos, D. R.; Ranise, S.. - 10469:(2017), pp. 203-218. (Intervento presentato al convegno 15th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2017 tenutosi a ita nel 2017) [10.1007/978-3-319-66197-1_13].

On run-time enforcement of authorization constraints in security-sensitive Workflows

Ranise S.
2017-01-01

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.
2017
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Germany
Springer Verlag
978-3-319-66196-4
978-3-319-66197-1
dos Santos, D. R.; Ranise, S.
On run-time enforcement of authorization constraints in security-sensitive Workflows / dos Santos, D. R.; Ranise, S.. - 10469:(2017), pp. 203-218. (Intervento presentato al convegno 15th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2017 tenutosi a ita nel 2017) [10.1007/978-3-319-66197-1_13].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333123
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact