To 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 to a convenient amount, 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 a large scale EU funded project. The paper details the approach, the properties analysed, the lessons learned and concludes with possible recommendations for practitioners and designers about how to use lightweight formal verification in real world projects. © Springer International Publishing Switzerland 2014.
Lightweight formal verification in real world, a case study
Montanaro T.
2014-01-01
Abstract
To 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 to a convenient amount, 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 a large scale EU funded project. The paper details the approach, the properties analysed, the lessons learned and concludes with possible recommendations for practitioners and designers about how to use lightweight formal verification in real world projects. © Springer International Publishing Switzerland 2014.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
