A Formal Analysis of the CORBA Security Service

  • David Basin
  • Frank Rittinger
  • Luca Viganó
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


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.


Access Control Formal Analysis Security Requirement State Schema Security Service 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. Arndt and T. Österdahl. Network security in distributed systems using CORBA. Technical report, Ericsson Hewlett-Packard Telecommunications AB, 1998.Google Scholar
  2. 2.
    B. Blakley. CORBA Security. Addison-Wesley-Longman, 1999.Google Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    D. Gollmann. Computer security. John Wiley & Sons, 1999.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    I. Hayes. Specification Case Studies. Prentice-Hall International, 1993.Google Scholar
  8. 10.
    D. Jackson and J. Wing. Lightweight formal methods. IEEE Computer, 1996.Google Scholar
  9. 11.
    J. Jacky. The way of Z. Cambridge University Press, 1997.Google Scholar
  10. 12.
    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.zbMATHCrossRefGoogle Scholar
  11. 13.
    G. Karjoth. Authorization in CORBA Security. Journal of Computer Security, 8(2–3):89–108, 2000.Google Scholar
  12. 14.
    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.Google Scholar
  13. 15.
    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.Google Scholar
  14. 16.
    D. Kreuz. Formale Semantik von Konnektoren. PhD thesis, Technische Universität Hamburg-Harburg, Germany, 1999. In German.Google Scholar
  15. 17.
    U. Lang. CORBA Security. Master’s thesis, Royal Holloway University of London, 1997.Google Scholar
  16. 18.
  17. 19.
    OMG. CORBA/IIOP 2.2. OMG, 1998.Google Scholar
  18. 20.
    OMG Security Working Group. CORBAservices Security Service Specification v1.2. Technical report, Document: formal/98-12-17, OMG, 1998.Google Scholar
  19. 21.
    R. Orfali, D. Harkey, and J. Edwards. Instant CORBA. Addison-Wesley-Longman, 1998.Google Scholar
  20. 22.
    L. C. Paulson. Isabelle: a generic theorem prover. LNCS 828. Springer-Verlag, 1994.zbMATHGoogle Scholar
  21. 23.
    D. Platt. Understanding COM+. Microsoft Press, 1999.Google Scholar
  22. 24.
    A. Pope. The CORBA Reference Guide. Addison-Wesley-Longman, 1998.Google Scholar
  23. 25.
    J.-C. Real. Object-Z speci.cation of the CORBA repository service. Technical Report 351, Université Libre de Bruxelles, 1997.Google Scholar
  24. 26.
    F. Rittinger. Formale Analyse des CORBA Sicherheitsdienstes. Diplomarbeit, Institut für Informatik, Albert-Ludwigs-Universität Freiburg, Germany, 2000. In German.Google Scholar
  25. 27.
    A. Roscoe. The Theory and Practice of Concurrency. Prentice Hall International, 1997.Google Scholar
  26. 28.
    G. Seshadri. Enterprise Java Computing. Cambridge University Press, 1999.Google Scholar
  27. 29.
    G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 1999.Google Scholar
  28. 30.
    J. Spivey. The Z Notation: A Reference Manual. Prentice Hall International, 2nd edition, 1992.Google Scholar
  29. 31.
    S. Stepney. Object Orientation in Z. Springer-Verlag, 1990.Google Scholar
  30. 32.
    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.Google Scholar
  31. 33.
    J. Woodcock and J. Davis. Using Z. Prentice Hall International, 1995.Google Scholar
  32. 34.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • David Basin
    • 1
  • Frank Rittinger
    • 1
  • Luca Viganó
    • 1
  1. 1.Institut für InformatikAlbert-Ludwigs-Universität FreiburgFreiburgGermany

Personalised recommendations