A formal data-model of the CORBA security service

ABSTRACT

We use the formal language Z to specify and analyze the security service of CORBA. 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, informal specification. Our approach is scenario-driven: we use representative scenarios to determine which parts of the informal specification should be formalized and then verify the formal specification against the requirements of these scenarios.

REFERENCES

• 1: D. Basin, F. Rittinger, and L. Vigano. A formal analysis of the CORBA security service. Technical Report 154, Institut f. ur Informatik, Albert-Ludwigs-Universit. at Freiburg, 2001.
• 2: Kolyang , Thomas Santen , Burkhart Wolff, A Structure Preserving Encoding of Z in Isabelle/HOL, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, p.283-298, August 26-30, 1996
• 3: OMG Security Working Group. CORBAservices Security Service Specification v1.2. Technical report, Document: formal/98-12-17, OMG, 1998.
• 4: F. Rittinger. Formale Analyse des CORBA Sicherheitsdienstes. Diplomarbeit, Institut fur Informatik, Albert-Ludwigs-Universit. at Freiburg, Germany, 2000. In German.
• 5: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
• 6: ZETA. http://uebb.cs.tu-berlin.de/zeta/.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

          Nouns: CORBA

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

          Nouns: Z

General Terms:
Security, Verification

Keywords:
CORBA security, Z, formal methods, specification