Lightweight Formal Verification in Real World, A Case Study

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.