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 firstorder 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. © 2010 IEEE.
Automated validation of security-sensitive web services specified in BPEL and RBAC / Calvi, A.; Ranise, S.; Vigano, L.. - (2010), pp. 456-464. (Intervento presentato al convegno 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing tenutosi a Romania nel 23-26/09/2011) [10.1109/SYNASC.2010.75].
Automated validation of security-sensitive web services specified in BPEL and RBAC
Ranise S.;
2010-01-01
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 firstorder 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. © 2010 IEEE.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione