The security of service-oriented applications is crucial in several contexts such as e-commerce or e-governance. The design, implementation, and deployment of this kind of services are often so complex that serious vulnerabilities remain even after extensive application of traditional validation techniques, such as testing. Given the importance of security-sensitive service applications, the development of techniques for their automated validation is growing. In this paper, we illustrate our formal framework to the specification and validation of security-sensitive applications structured in two levels: the workflow level (dealing with the control of flow and the manipulation of data) and the policy level (describing trust relationships and access control). In our framework, verification problems are reduced to logical problems whose decidability can be shown under suitable assumptions, which permit the validation of practically relevant classes of services. As a by-product, it is possible to re-use state-ofthe-art theorem-proving technology to mechanize the verification process. This is the idea underlying our prototype validation tool WSSMT, "Web-Service (validation by) Satisfiability Modulo Theories", which has been successfully used on two industrial case studies taken from the FP7 European project AVANTSSAR. © 2010 IEEE.

WSSMT: Towards the automated analysis of security-sensitive services and applications / Barletta, M.; Calvi, A.; Ranise, S.; Vigano, L.; Zanetti, L.. - (2010), pp. 417-424. (Intervento presentato al convegno 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010 tenutosi a Romania nel 23-26/09/2010) [10.1109/SYNASC.2010.74].

WSSMT: Towards the automated analysis of security-sensitive services and applications

Ranise S.;
2010-01-01

Abstract

The security of service-oriented applications is crucial in several contexts such as e-commerce or e-governance. The design, implementation, and deployment of this kind of services are often so complex that serious vulnerabilities remain even after extensive application of traditional validation techniques, such as testing. Given the importance of security-sensitive service applications, the development of techniques for their automated validation is growing. In this paper, we illustrate our formal framework to the specification and validation of security-sensitive applications structured in two levels: the workflow level (dealing with the control of flow and the manipulation of data) and the policy level (describing trust relationships and access control). In our framework, verification problems are reduced to logical problems whose decidability can be shown under suitable assumptions, which permit the validation of practically relevant classes of services. As a by-product, it is possible to re-use state-ofthe-art theorem-proving technology to mechanize the verification process. This is the idea underlying our prototype validation tool WSSMT, "Web-Service (validation by) Satisfiability Modulo Theories", which has been successfully used on two industrial case studies taken from the FP7 European project AVANTSSAR. © 2010 IEEE.
2010
Proceedings - 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010
10662 LOS VAQUEROS CIRCLE, PO BOX 3014, LOS ALAMITOS, CA 90720-1264 USA
IEEE Computer Society
978-1-4244-9816-1
Barletta, M.; Calvi, A.; Ranise, S.; Vigano, L.; Zanetti, L.
WSSMT: Towards the automated analysis of security-sensitive services and applications / Barletta, M.; Calvi, A.; Ranise, S.; Vigano, L.; Zanetti, L.. - (2010), pp. 417-424. (Intervento presentato al convegno 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010 tenutosi a Romania nel 23-26/09/2010) [10.1109/SYNASC.2010.74].
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/333119
 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??? 1
  • OpenAlex ND
social impact