Specifying and analyzing security automata using CSP-OZ

ABSTRACT

Security automata are a variant of Büchi automata used to specify security policies that can be enforced by monitoring system execution. In this paper, we propose using CSP-OZ, a specification language combining Communicating Sequential Processes (CSP) and Object-Z (OZ), to specify security automata, formalize their combination with target systems, and analyze the security of the resulting system specifications. We provide theoretical results relating CSP-OZ specifications and security automata and show how refinement can be used to reason about specifications of security automata and their combination with target systems. Through a case study, we provide evidence for the practical usefulness of this approach. This includes the ability to specify concisely complex operations and complex control, support for structured specifications, refinement, and transformational design, as well as automated, tool-supported analysis.

REFERENCES

• 1: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 2: B. Alpern and F. Schneider. Defining Liveness. Inf. Process. Lett., 21(4):181--185, 1985.
• 3: B. Alpern and F. Schneider. Recognizing Safety and Liveness. Distributed Computing, 2:117--126, 1987.
• 4: David Basin , Jürgen Doser , Torsten Lodderstedt, Model driven security: From UML models to access control infrastructures, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.1, p.39-91, January 2006 [doi>10.1145/1125808.1125810]
• 5: Lujo Bauer , Jay Ligatti , David Walker, Composing security policies with polymer, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 6: S. D. Brookes , C. A. R. Hoare , A. W. Roscoe, A Theory of Communicating Sequential Processes, Journal of the ACM (JACM), v.31 n.3, p.560-599, July 1984 [doi>10.1145/828.833]
• 7: M. Butler and M. Leuschel. Combining CSP and B for specification and property verification. In J. Fitzgerald, I. Hayes, and A. Tarlecki, editors, Formal Methods 2005, volume 3582 of LNCS. Springer, 2005.
• 8: Nicodemos Damianou , Naranker Dulay , Emil Lupu , Morris Sloman, The Ponder Policy Specification Language, Proceedings of the International Workshop on Policies for Distributed Systems and Networks, p.18-38, January 29-31, 2001
• 9: Roger Duke , Gordon Rose , Graeme Smith, Object-Z: a specification language advocated for the description of standards, Computer Standards & Interfaces, v.17 n.5-6, p.511-533, Sept. 30, 1995 [doi>10.1016/0920-5489(95)00024-O]
• 10: Ulfar Erlingsson , Fred B. Schneider, IRM Enforcement of Java Stack Inspection, Proceedings of the 2000 IEEE Symposium on Security and Privacy, p.246, May 14-17, 2000
• 11: D. Evans and A. Twyman. Flexible policy-directed code safety. In IEEE Symposium on Security and Privacy, pages 32--45, 1999.
• 12: Clemens Fischer, CSP-OZ: a combination of object-Z and CSP, Proceeding of the IFIP TC6 WG6.1 international workshop on Formal methods for open object-based distributed systems, p.423-438, January 1997, Canterbury, United Kingdom
• 13: C. Fischer. Combination and Implementation of Processes and Data: From CSP-OZ to Java. PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.
• 14: Clemens Fischer , Heike Wehrheim, Model-Checking CSP-OZ Specifications with FDR, Proceedings of the 1st International Conference on Integrated Formal Methods, p.315-334, June 28-29, 1999
• 15: Formal Systems (Europe) Ltd. Failures-Divergence Refinement --- FDR 2 User Manual, May 2003.
• 16: L. Freitas. Model Checking Circus. PhD thesis, University of York, October 2005.
• 17: Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Computability classes for enforcement mechanisms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.1, p.175-205, January 2006 [doi>10.1145/1111596.1111601]
• 18: Klaus Havelund , Grigore Roşu, Efficient monitoring of safety properties, International Journal on Software Tools for Technology Transfer (STTT), v.6 n.2, p.158-173, August 2004 [doi>10.1007/s10009-003-0117-6]
• 19: Klaus Havelund , Grigore Roşu, An Overview of the Runtime Verification Tool Java PathExplorer, Formal Methods in System Design, v.24 n.2, p.189-215, March 2004 [doi>10.1023/B:FORM.0000017721.39909.4b]
• 20: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 21: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 22: International Organization for Standardization. Information technology - Z formal specification notation - Syntax, type system and semantics, first edition, July 2002.
• 23: Gary T. Leavens , Yoonsik Cheon , Curtis Clifton , Clyde Ruby , David R. Cok, How the design of JML accommodates both runtime assertion checking and formal verification, Science of Computer Programming, v.55 n.1-3, p.185-208, March 2005 [doi>10.1016/j.scico.2004.05.015]
• 24: J. Ligatti, L. Bauer, and D. Walker. Edit automata: Enforcement mechanisms for run-time security policies. International Journal of Information Security, 4(1--2):2--16, 2005.
• 25: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 26: M. Möller, E.-R. Olderog, H. Rasch, and H. Wehrheim. Linking CSP-OZ with UML and Java: A Case Study. In E. Boiten, J. Derrick, and G. Smith, editors, Integrated Formal Methods, volume 2999 of LNCS, pages 267--286. Springer, 2004.
• 27: Carroll Morgan, Programming from specifications, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 28: E R Olderog , C A R Hoare, Specification-oriented semantics for communicating processes, Acta Informatica, v.23 n.1, p.9-66, April 1986 [doi>10.1007/BF00268075]
• 29: Ernst-Rüdiger Olderog , Stephan Rössig, A Case Study in Transformational Design of Concurrent Systems, Proceedings of the International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.90-104, April 13-17, 1993
• 30: A. W. Roscoe, Model-checking CSP, A classical mind: essays in honour of C. A. R. Hoare, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 31: A. W. Roscoe , C. A. R. Hoare , Richard Bird, The Theory and Practice of Concurrency, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 32: Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
• 33: P. E. Sevinç. and D. Basin. Controlling access to documents: A formal access control model. Technical report, ETH Zurich, 2006.
• 34: P. E. Sevinç, D. Basin, and E.-R. Olderog. Controlling access to documents: A formal access control model. In G. Müller and G. Schneider, editors, Proc. of ETRICS 2006, volume 3995 of LNCS, pages 352--367. Springer, 2006.
• 35: The Object-Z specification language, Kluwer Academic Publishers, Norwell, MA, 1999
• 36: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 37: Steve Schneider , Helen Treharne, Communicating B Machines, Proceedings of the 2nd International Conference of B and Z Users on Formal Specification and Development in Z and B, p.416-435, January 23-25, 2002
• 38: G. von Bochmann and J. Gecsei. A unified method for the specification and verification of protocols. In IFIP Congress, pages 229--234, 1977.
• 39: Jim Woodcock , Ana Cavalcanti, The Semantics of Circus, Proceedings of the 2nd International Conference of B and Z Users on Formal Specification and Development in Z and B, p.184-203, January 23-25, 2002
• 40: Jim Woodcock , Jim Davies, Using Z: specification, refinement, and proof, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages

General Terms:
Languages, Security, Verification

Keywords:
CSP-OZ, security automata