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.
Chapter PDF
Similar content being viewed by others
Keywords
References
Easterbrook, S., Callahan, J.: Formal methods for verification and validation of partial specifications: A case study. Journal of Systems and Software 40(3), 199–210 (1998)
Mundra, P., Shukla, S., Sharma, M., Pai, R.M., Singh, S.: Modeling and Verification of Kerberos Protocol Using Symbolic Model Verifier. In: 2011 International Conference on Communication Systems and Network Technologies, pp. 651–654. IEEE (June 2011)
Fuhrhop, C., Lyle, J., Faily, S.: The webinos project. In: Proceedings of the 21st International Conference Companion on World Wide Web - WWW 2012, p. 259. ACM Press, New York (2012)
Zave, P.: Using lightweight modeling to understand chord. ACM SIGCOMM Computer Communication Review 42(2), 49 (2012)
Taghdiri, M., Jackson, D.: A lightweight formal analysis of a multicast key management scheme. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 240–256. Springer, Heidelberg (2003)
Taghdiri, M.: Lightweight modelling and automatic analysis of multicast key management schemes. Master’s thesis. MIT (2002)
Easterbrook, S., Lutz, R., Covington, R., Kelly, J., Ampo, Y., Hamilton, D.: Experiences using lightweight formal methods for requirements modeling. IEEE Transactions on Software Engineering 24(1), 4–14 (1998)
Su, T., Lyle, J., Atzeni, A., Faily, S., Virji, H., Ntanos, C., Botsikas, C.: Continuous integration for web-based software infrastructures: Lessons learned on the webinos project. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 145–150. Springer, Heidelberg (2013)
webinos group: webinos authentication system specifications (2012), http://www.webinos.org/content/html/D033/Authentication.htm
Recordon, D., Reed, D.: OpenID 2.0. In: Proceedings of the second ACM workshop on Digital identity management - DIM 2006, p. 11. ACM Press, New York (2006)
Hammer-Lahav, E.: The OAuth 1.0 Protocol (2010), http://tools.ietf.org/html/rfc5849
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A reimplementation of SMV. In: Proc. STTT 1998, pp. 25–31 (1998)
von Ahn, L., Blum, M., Hopper, N.J., Langford, J.: CAPTCHA: Using hard AI problems for security. In: Biham, E. (ed.) EUROCRYPT 2003. LNCS, vol. 2656, pp. 294–311. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Atzeni, A., Su, T., Montanaro, T. (2014). Lightweight Formal Verification in Real World, A Case Study. In: Iliadis, L., Papazoglou, M., Pohl, K. (eds) Advanced Information Systems Engineering Workshops. CAiSE 2014. Lecture Notes in Business Information Processing, vol 178. Springer, Cham. https://doi.org/10.1007/978-3-319-07869-4_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-07869-4_31
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07868-7
Online ISBN: 978-3-319-07869-4
eBook Packages: Computer ScienceComputer Science (R0)