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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione