In security oriented large-scale projects, formal verification is widely used to assure the satisfaction of claimed security properties. Although complete formal verification and validation requires a great amount of time and resources, applying lightweight formal methods to partial specifications reduces the required efforts, while can still uncover sensitive software design problems. This paper describes our experience of applying lightweight formal verification to the authentication system of webinos, a substantial cross-device software infrastructure developed in the homonymous EC-funded project. The paper details the approach, the properties analysed, the lessons learnt and concludes with possible recommendations for practitioners and designers about how to use lightweight formal verification in real world projects.

Lightweight Formal Verification in Real World, A Case Study / Atzeni, Andrea; Su, Tao; Montanaro, Teodoro. - STAMPA. - (2014), pp. 335-342. (Intervento presentato al convegno WISSE 2014: 4th International Workshop on Information Systems Security Engineering tenutosi a Thessaloniki (Greece) nel 17 June 2014) [10.1007/978-3-319-07869-4_31].

Lightweight Formal Verification in Real World, A Case Study

ATZENI, ANDREA;SU, TAO;MONTANARO, TEODORO
2014

Abstract

In security oriented large-scale projects, formal verification is widely used to assure the satisfaction of claimed security properties. Although complete formal verification and validation requires a great amount of time and resources, applying lightweight formal methods to partial specifications reduces the required efforts, while can still uncover sensitive software design problems. This paper describes our experience of applying lightweight formal verification to the authentication system of webinos, a substantial cross-device software infrastructure developed in the homonymous EC-funded project. The paper details the approach, the properties analysed, the lessons learnt and concludes with possible recommendations for practitioners and designers about how to use lightweight formal verification in real world projects.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/11583/2550539
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo