Abstract
We give a formal specification and analysis of the security service of CORBA, the Common Object Request Broker Architecture specified by the Object Management Group, OMG. In doing so, we tackle the problem of how one can apply lightweight formal methods to improve the precision and aid the analysis of a substantial, committee-designed, informal specification. Our approach is scenario-driven: we use representative scenarios to determine which parts of the informal specification should be formalized and verify the resulting formal specification against these scenarios. For the formalization, we have speci.ed a significant part of the security service’s data-model using the formal language Z. Through this process, we have been able to sharpen the OMG-specification, uncovering a number of errors and omissions.
This work was partially supported by the Deutsche Forschungsgemeinschaft under grant BA 1740/5-1 “Formale Sicherheitsarchitekturen”.
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
J. Arndt and T. Österdahl. Network security in distributed systems using CORBA. Technical report, Ericsson Hewlett-Packard Telecommunications AB, 1998.
B. Blakley. CORBA Security. Addison-Wesley-Longman, 1999.
G. Brose. A Typed Access Control Model for CORBA. In F. Cuppens, Y. Deswarte, D. Gollmann, and M. Waidner, editors, Proceedings of ESORICS 2000, LNCS 1895, pages 88–105. Springer-Verlag, 2000.
G. Duval. Specification and veri.cation of an object request broker. In Proceedings of the 20th International Conference on Software Engineering (ICSE’98), pages 43–52. IEEE Computer Society Press, 1998.
D. Gollmann. Computer security. John Wiley & Sons, 1999.
J. Hall. Using Z as a speci.cation calculus for object oriented systems. In D. Bjorner, C. A. R. Hoare, and H. Langmaack, editors, Proceedings of VDM’90, LNCS 428, pages 290–318. Springer-Verlag, 1990.
I. Hayes. Specification Case Studies. Prentice-Hall International, 1993.
D. Jackson and J. Wing. Lightweight formal methods. IEEE Computer, 1996.
J. Jacky. The way of Z. Cambridge University Press, 1997.
M. Kamel and S. Leue. Formalization and Validation of the General Inter-ORB Protocol (GIOP) using Promela and Spin. Software Tools for Technology Transfer, 2:394–409, 2000.
G. Karjoth. Authorization in CORBA Security. Journal of Computer Security, 8(2–3):89–108, 2000.
Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/ HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Proceedings of TPHOLs’96, LNCS 1125, pages 283–298. Springer-Verlag, 1996.
D. Kreuz. Formal specification of CORBA services using Object-Z. In Proceedings of 2nd IEEE International Conference on Formal Engineering Methods (ICFEM’98). IEEE Computer Society Press, 1998.
D. Kreuz. Formale Semantik von Konnektoren. PhD thesis, Technische Universität Hamburg-Harburg, Germany, 1999. In German.
U. Lang. CORBA Security. Master’s thesis, Royal Holloway University of London, 1997.
OMG. http://www.omg.org.
OMG. CORBA/IIOP 2.2. OMG, 1998.
OMG Security Working Group. CORBAservices Security Service Specification v1.2. Technical report, Document: formal/98-12-17, OMG, 1998.
R. Orfali, D. Harkey, and J. Edwards. Instant CORBA. Addison-Wesley-Longman, 1998.
L. C. Paulson. Isabelle: a generic theorem prover. LNCS 828. Springer-Verlag, 1994.
D. Platt. Understanding COM+. Microsoft Press, 1999.
A. Pope. The CORBA Reference Guide. Addison-Wesley-Longman, 1998.
J.-C. Real. Object-Z speci.cation of the CORBA repository service. Technical Report 351, Université Libre de Bruxelles, 1997.
F. Rittinger. Formale Analyse des CORBA Sicherheitsdienstes. Diplomarbeit, Institut für Informatik, Albert-Ludwigs-Universität Freiburg, Germany, 2000. In German.
A. Roscoe. The Theory and Practice of Concurrency. Prentice Hall International, 1997.
G. Seshadri. Enterprise Java Computing. Cambridge University Press, 1999.
G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 1999.
J. Spivey. The Z Notation: A Reference Manual. Prentice Hall International, 2nd edition, 1992.
S. Stepney. Object Orientation in Z. Springer-Verlag, 1990.
H. Tej and B. Wolff. A corrected failure-divergence model for CSP in Isabelle/HOL. In J. Fitzgerald, C. Jones, and P. Lucas, editors, Proceedings of FME’97, LNCS 1313, pages 318–337. Springer-Verlag, 1997.
J. Woodcock and J. Davis. Using Z. Prentice Hall International, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basin, D., Rittinger, F., Viganó, L. (2002). A Formal Analysis of the CORBA Security Service. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds) ZB 2002:Formal Specification and Development in Z and B. ZB 2002. Lecture Notes in Computer Science, vol 2272. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45648-1_17
Download citation
DOI: https://doi.org/10.1007/3-540-45648-1_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43166-4
Online ISBN: 978-3-540-45648-3
eBook Packages: Springer Book Archive