Abstract
Formal methods in the industrial wild, outside the academic greenhouse, are still considered rather exotic, or even esoteric. Sometimes they are admired, more often smiled at, and most times simply ignored. There are some niches, though, where they display their abstract beauty. One of those places offering suitable environmental conditions is security. Which are the specific fertilizers there? Which particular sub-species have proven versatile and sturdy enough to survive in harsh industrial climate? Who recognizes the strong blessings of their hardly accessible blossoms? We share our grower’s experience with them in the security field.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
The AVISPA project homepage (2003), http://www.avispa-project.org/
Bell, D.E., LaPadula, L.: Secure Computer Systems: Mathematical Foundations (NTIS AD-770 768), A Mathematical Model (NTIS AD-771 543), A Refinement of the Mathematical Model (NTIS AD-780 528). Technical Report MTR 2547, Mitre Corporation, Bedford MA (1973)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos (1982)
Lotz, V., Kessler, V., Walter, G.: A Formal Security Model for Microprocessor Hardware. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 718–737. Springer, Heidelberg (1999)
Lynch, N., Tuttle, M.: An Introduction to Input/Output Automata. CWI Quarterly 2(3), 219–246 (1989), http://theory.lcs.mit.edu/tds/papers/Lynch/CWI89.html
Mantel, H.: A Uniform Framework for the Formal Specification and Verification of Information Flow Security. PhD thesis, Univ. d. Saarlandes (2003)
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL— A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002), See also: http://isabelle.in.tum.de/docs.html
von Oheimb, D.: Information flow control revisited: Noninfluence = Noninterference + Nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 225–243. Springer, Heidelberg (2004), http://ddvo.net/papers/Noninfluence.html
von Oheimb, D., Lotz, V.: Formal Security Analysis with Interacting State Machines. In: Klein, G. (ed.) Proc. NICTA Formal Methods Workshop on Operating Systems Verification, Sydney, Australia, pp. 37–72. National ICT Australia, Technical Report 0401005T-1 (2004), http://ddvo.net/papers/FSA_ISM.html
von Oheimb, D., Lotz, V., Walter, G.: Analyzing SLE 88 memory management security using Interacting State Machines. International Journal of Information Security 4(3), 155–171 (2005), http://ddvo.net/papers/SLE88_MM.html
Sandhu, R.S., Coyne, E.J., Feinstein, H.L., Youman, C.E.: Role-based access control models. IEEE Computer 29(2), 38–47 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
von Oheimb, D. (2006). Formal Methods in the Security Business: Exotic Flowers Thriving in an Expanding Niche. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_40
Download citation
DOI: https://doi.org/10.1007/11813040_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37215-8
Online ISBN: 978-3-540-37216-5
eBook Packages: Computer ScienceComputer Science (R0)