Abstract
High assurance security is difficult to achieve in distributed computer systems and databases because of their complexity, non-determinism and inherent heterogeneity. The practical application of formal methods is the key to high assurance security in open, distributed environments. This paper proposes the use of formal methods and a special layered architecture to achieve secure interoperation of heterogeneous distributed objects. The foundation is provided by ROC, a process calculus tailored for concurrent objects. Lying above ROC in the layered architecture is a meta-object model for creating object models with various programming constructs, mega-programming facilities and security mechanisms. Successive layers of the architecture represent more sophisticated toolkits for modeling distributed objects. Since each layer inherits ROC’s formal foundation, it automatically has an unambiguous semantics and supports verification.
Chapter PDF
Similar content being viewed by others
References
Agha, G.A. (1986) ACTORS: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, Massachusetts.
Alves-Foss, J. and Levitt, K. (1991) Mechanical verification of secure distributed systems in higher order logic. Proceedings of the 1991 International Workshop on Higher Order Theorem Proving and its Applications, 263–278.
Bevier, W.R., Hunt, W.A., Moore, J.S. and Young, W.D. (1989) An approach to systems verification. Technical Report 41, Computational Logic, Inc., Austin, Texas.
Chien, A.A. (1993) Concurrent Aggregates. MIT Press, Cambridge, Massachusetts.
Church, A. (1940) A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 56–68.
Diller, A. (1990) Z: An Introduction to Formal Methods. John Wiley, New York.
Gong, L. and Qian, X. (1996) Computational issues in secure interoperation. IEEE Transactions on Software Engineering, 32, 43–52.
Gordon, M. and Melham, T.F. (eds.) (1993) Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, U.K.
Hinchey, M. and Bowen, J. (eds.) (1995) Applications of Formal Methods. Prentice Hall, New York.
Maclean, J. (1990) The specification and modeling of computer security. IEEE Computer, 23 (1), 34–46.
Maclean, J. and Meadows, C. (1989) Composable security properties. Proceedings of the Computer Security Workshop.
Melham, T.F. (1992) A mechanized theory of the π-calculus in HOL. Technical Report 244, University of Cambridge Computer Laboratory, Cambridge, U.K.
Milner, R., Parrow, J. and Walker, D. (1989) A calculus of mobile processes. Technical Report ECS-LFCS-89–85&86, University of Edinburgh, Edinburgh, U.K.
Mowbray, T.J. and Zahavi, R. (1995) The Essential CORBA: Systems Integration Using Distributed Objects. John Wiley, New York.
Nierstrasz, O. (1991) Towards an object calculus, in Proceedings of the ECOOP’91 Workshop on Object-Based Concurrent Computing (eds. M. Tokoro, O. Nierstrasz and R.A. Olsson ), Springer Verlag, Amsterdam, The Netherlands, 1–20.
Object Management Group and X/Open (1991) The common object request broker: Architecture and specification. Technical Report OMG Document No. 91.12. 1, Object Management Group and X/Open, Framingham, Massachusetts.
Open Systems Foundation (1992) The OSF distributed computing environment. Technical Report OSF-DCE-PD-1090–4, Open Systems Foundation, Cambridge, Massachusetts.
Rosenberry, W., Kenney, D. and Fisher, G. (1993) Understanding DCE. O’Reilly and Associates, Inc., Sebastopal, California.
Wing, J. (1990) A specifier’s introduction to formal methods. IEEE Computer, 23 (9), 8–21.
Zhang, C., Shaw, R., Heckman, M.R., Levitt, K. and Olsson, R.A. (1995) A hierarchical method for reasoning about distributed programming languages and applications. Proceedings of the 1995 International Workshop on Higher Order Logic Theorem Proving and its Applications.
Zhang, C., Shaw, R., Heckman, M.R., Benson, G.D., Archer, M., Levitt, K. and Olsson, R.A. (1994) Towards a formal verification of a secure distributed system and its applications. Supplementary Proceedings of the Seventh International Workshop on Higher Order Logic Theorem Proving and its Applications.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Hale, J., Threet, J., Shenoi, S. (1997). A Framework for High Assurance Security of Distributed Objects. In: Samarati, P., Sandhu, R.S. (eds) Database Security. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35167-4_7
Download citation
DOI: https://doi.org/10.1007/978-0-387-35167-4_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2900-8
Online ISBN: 978-0-387-35167-4
eBook Packages: Springer Book Archive