Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC (Extended Version)

TL;DR

This paper presents a formal, automated approach for validating security-sensitive web services specified in BPEL and RBAC using SMT solvers, demonstrated through a prototype applied to an industrial case study.

Contribution

It introduces a novel formal analysis method combining decidable logic fragments and SMT solvers for web service validation, with a practical prototype implementation.

Findings

Effective validation of web services using SMT solvers

Prototype successfully applied to an industrial case study

Formal approach enhances security validation processes

Abstract

We formalize automated analysis techniques for the validation of web services specified in BPEL and a RBAC variant tailored to BPEL. The idea is to use decidable fragments of first-order logic to describe the state space of a certain class of web services and then use state-of-the-art SMT solvers to handle their reachability problems. To assess the practical viability of our approach, we have developed a prototype tool implementing our techniques and applied it to a digital contract signing service inspired by an industrial case study.