The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures

Alessandro Armando; Wihem Arsac; Tigran Avanesov; Michele Barletta; Alberto Calvi; Alessandro Cappai; Roberto Carbone; Yannick Chevalier; Luca Compagna; Jorge Cuéllar; Gabriel Erzse; Simone Frau; Marius Minea; Sebastian Alexander Mödersheim; David Von Oheimb; Giancarlo Pellegrino; Serena Elisa Ponta; Marco Rocchetto; Michael Rusinowitch; Mohammad Torabi Dashti; Mathieu Turuani; Luca Viganò

doi:10.1007/978-3-642-28756-5_19

The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures

Alessandro Armando
, Wihem Arsac
, Tigran Avanesov
, Michele Barletta
, Alberto Calvi
, Alessandro Cappai
, Roberto Carbone
, Yannick Chevalier
, Luca Compagna
, Jorge Cuéllar
, Gabriel Erzse
, Simone Frau
, Marius Minea
, Sebastian Alexander Mödersheim
, David Von Oheimb
, Giancarlo Pellegrino
, Serena Elisa Ponta
, Marco Rocchetto
, Michael Rusinowitch
, Mohammad Torabi Dashti

Mathieu Turuani, Luca Viganò

University of Genoa
SAP Research
LORIA & INRIA Nancy Grand Est
University of Verona
Université de Toulouse
Siemens
Institute e-Austria Timisoara
Swiss Federal Institute of Technology Zurich

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Abstract

The AVANTSSAR Platform is an integrated toolset for the formal specification and automated validation of trust and security of service-oriented architectures and other applications in the Internet of Services. The platform supports application-level specification languages (such as BPMN and our custom languages) and features three validation backends (CL-AtSe, OFMC, and SATMC), which provide a range of complementary automated reasoning techniques (including service orchestration, compositional reasoning, model checking, and abstract interpretation). We have applied the platform to a large number of industrial case studies, collected into the AVANTSSAR Library of validated problem cases. In doing so, we unveiled a number of problems and vulnerabilities in deployed services. These include, most notably, a serious flaw in the SAML-based Single Sign-On for Google Apps (now corrected by Google as a result of our findings). We also report on the migration of the platform to industry.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems : 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings
Publisher	Springer
Publication date	2012
Pages	267-282
ISBN (Print)	978-3-642-28755-8
ISBN (Electronic)	978-3-642-28756-5
DOIs	https://doi.org/10.1007/978-3-642-28756-5_19
Publication status	Published - 2012
Event	18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012) - Tallinn, Estonia Duration: 24 Mar 2012 → 1 Apr 2012 http://www.etaps.org/2012/tacas

Conference

Conference	18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)
Country/Territory	Estonia
City	Tallinn
Period	24/03/2012 → 01/04/2012
Internet address	http://www.etaps.org/2012/tacas

Series	Lecture Notes in Computer Science
Volume	7214
ISSN	0302-9743

Access to Document

10.1007/978-3-642-28756-5_19

OpenUrl availability

Check availability in DTU Findit

Cite this

Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cuéllar, J., Erzse, G., Frau, S., Minea, M., Mödersheim, S. A., Von Oheimb, D., Pellegrino, G., Ponta, S. E., Rocchetto, M., Rusinowitch, M., ... Viganò, L. (2012). The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. In Tools and Algorithms for the Construction and Analysis of Systems: 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings (pp. 267-282). Springer. https://doi.org/10.1007/978-3-642-28756-5_19

Armando, Alessandro ; Arsac, Wihem ; Avanesov, Tigran et al. / The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. Tools and Algorithms for the Construction and Analysis of Systems: 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Springer, 2012. pp. 267-282 (Lecture Notes in Computer Science, Vol. 7214).

@inproceedings{0ec81d2e644c44b48288cba8c7e31f56,

title = "The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures",

abstract = "The AVANTSSAR Platform is an integrated toolset for the formal specification and automated validation of trust and security of service-oriented architectures and other applications in the Internet of Services. The platform supports application-level specification languages (such as BPMN and our custom languages) and features three validation backends (CL-AtSe, OFMC, and SATMC), which provide a range of complementary automated reasoning techniques (including service orchestration, compositional reasoning, model checking, and abstract interpretation). We have applied the platform to a large number of industrial case studies, collected into the AVANTSSAR Library of validated problem cases. In doing so, we unveiled a number of problems and vulnerabilities in deployed services. These include, most notably, a serious flaw in the SAML-based Single Sign-On for Google Apps (now corrected by Google as a result of our findings). We also report on the migration of the platform to industry. ",

author = "Alessandro Armando and Wihem Arsac and Tigran Avanesov and Michele Barletta and Alberto Calvi and Alessandro Cappai and Roberto Carbone and Yannick Chevalier and Luca Compagna and Jorge Cu{\'e}llar and Gabriel Erzse and Simone Frau and Marius Minea and M{\"o}dersheim, \{Sebastian Alexander\} and \{Von Oheimb\}, David and Giancarlo Pellegrino and Ponta, \{Serena Elisa\} and Marco Rocchetto and Michael Rusinowitch and \{Torabi Dashti\}, Mohammad and Mathieu Turuani and Luca Vigan{\`o}",

year = "2012",

doi = "10.1007/978-3-642-28756-5\_19",

language = "English",

isbn = "978-3-642-28755-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "267--282",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

note = "18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012) ; Conference date: 24-03-2012 Through 01-04-2012",

url = "http://www.etaps.org/2012/tacas",

}

Armando, A, Arsac, W, Avanesov, T, Barletta, M, Calvi, A, Cappai, A, Carbone, R, Chevalier, Y, Compagna, L, Cuéllar, J, Erzse, G, Frau, S, Minea, M, Mödersheim, SA, Von Oheimb, D, Pellegrino, G, Ponta, SE, Rocchetto, M, Rusinowitch, M, Torabi Dashti, M, Turuani, M & Viganò, L 2012, The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. in Tools and Algorithms for the Construction and Analysis of Systems: 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Springer, Lecture Notes in Computer Science, vol. 7214, pp. 267-282, 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Tallinn, Estonia, 24/03/2012. https://doi.org/10.1007/978-3-642-28756-5_19

The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. / Armando, Alessandro; Arsac, Wihem; Avanesov, Tigran et al.
Tools and Algorithms for the Construction and Analysis of Systems: 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Springer, 2012. p. 267-282 (Lecture Notes in Computer Science, Vol. 7214).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures

AU - Armando, Alessandro

AU - Arsac, Wihem

AU - Avanesov, Tigran

AU - Barletta, Michele

AU - Calvi, Alberto

AU - Cappai, Alessandro

AU - Carbone, Roberto

AU - Chevalier, Yannick

AU - Compagna, Luca

AU - Cuéllar, Jorge

AU - Erzse, Gabriel

AU - Frau, Simone

AU - Minea, Marius

AU - Mödersheim, Sebastian Alexander

AU - Von Oheimb, David

AU - Pellegrino, Giancarlo

AU - Ponta, Serena Elisa

AU - Rocchetto, Marco

AU - Rusinowitch, Michael

AU - Torabi Dashti, Mohammad

AU - Turuani, Mathieu

AU - Viganò, Luca

PY - 2012

Y1 - 2012

N2 - The AVANTSSAR Platform is an integrated toolset for the formal specification and automated validation of trust and security of service-oriented architectures and other applications in the Internet of Services. The platform supports application-level specification languages (such as BPMN and our custom languages) and features three validation backends (CL-AtSe, OFMC, and SATMC), which provide a range of complementary automated reasoning techniques (including service orchestration, compositional reasoning, model checking, and abstract interpretation). We have applied the platform to a large number of industrial case studies, collected into the AVANTSSAR Library of validated problem cases. In doing so, we unveiled a number of problems and vulnerabilities in deployed services. These include, most notably, a serious flaw in the SAML-based Single Sign-On for Google Apps (now corrected by Google as a result of our findings). We also report on the migration of the platform to industry.

AB - The AVANTSSAR Platform is an integrated toolset for the formal specification and automated validation of trust and security of service-oriented architectures and other applications in the Internet of Services. The platform supports application-level specification languages (such as BPMN and our custom languages) and features three validation backends (CL-AtSe, OFMC, and SATMC), which provide a range of complementary automated reasoning techniques (including service orchestration, compositional reasoning, model checking, and abstract interpretation). We have applied the platform to a large number of industrial case studies, collected into the AVANTSSAR Library of validated problem cases. In doing so, we unveiled a number of problems and vulnerabilities in deployed services. These include, most notably, a serious flaw in the SAML-based Single Sign-On for Google Apps (now corrected by Google as a result of our findings). We also report on the migration of the platform to industry.

U2 - 10.1007/978-3-642-28756-5_19

DO - 10.1007/978-3-642-28756-5_19

M3 - Article in proceedings

SN - 978-3-642-28755-8

T3 - Lecture Notes in Computer Science

SP - 267

EP - 282

BT - Tools and Algorithms for the Construction and Analysis of Systems

PB - Springer

T2 - 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)

Y2 - 24 March 2012 through 1 April 2012

ER -

Armando A, Arsac W, Avanesov T, Barletta M, Calvi A, Cappai A et al. The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. In Tools and Algorithms for the Construction and Analysis of Systems: 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Springer. 2012. p. 267-282. (Lecture Notes in Computer Science, Vol. 7214). doi: 10.1007/978-3-642-28756-5_19

The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this