This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A General Theory of Composition for a Class of "Possibilistic" Properties
January 1996 (vol. 22 no. 1)
pp. 53-67

Abstract—Since the initial work of Daryl McCullough on the subject, the security community has struggled with the problem of composing "possibilistic" information-flow properties. Such properties fall outside of the Alpern-Schneider safety/liveness domain, and hence, they are not subject to the Abadi-Lamport Composition Principle. This paper introduces a set of trace constructors called selective interleaving functions and shows that possibilistic information-flow properties are closure properties with respect to different classes of selective interleaving functions. This provides a uniform framework for analyzing these properties, allowing us to construct both a partial ordering for them and a theory of composition for them. We present a number of composition constructs, show the extent to which each preserves closure with respect to different classes of selective interleaving functions, and show that they are sufficient for forming the general hook-up construction. We see that although closure under a class of selective interleaving functions is generally preserved by product and cascading, it is not generally preserved by feedback, internal system composition constructs, or refinement. We examine the reason for this.

[1] M. Abadi and L. Lamport, "Composing specifications," Stepwise Refinement of Distributed Systems, J. W. de Bakker, W. P. de Roever, and G. Rosenberg, eds., Lecture Notes in Computer Science, vol. 430. Springer-Verlag, 1990.
[2] B. Alpern and F. Schneider, "Defining liveness," Information Processing Letters, vol. 21, no. 4, pp. 181-185, Oct. 1985.
[3] J. Goguen and J. Meseguer, "Security policies and security models," Proc. 1982 IEEE Symp. Research in Security and Privacy. IEEE Press, 1982.
[4] J. Graham-Cumming and J.W. Sanders, "On the refinement of non-interference," Proc. Computer Security Foundations Workshop IV. IEEE Press, 1991.
[5] J. Gray, "Toward a mathematical foundation for information flow security," J. Computer Security, vol. 1, nos. 3-4, pp. 255-294, 1992.
[6] J. Jacob, "On the derivation of secure components," Proc. 1989 IEEE Symp. Research in Security and Privacy. IEEE Press, 1989.
[7] M. Li and P. Vitányi, "Kolmogorov complexity and its applications," Handbook of Theoretical Computer Science, vol. A: Algorithms and Complexity, J. van Leeuwen, ed. MIT Press/Elsevier, 1990.
[8] D. McCullough, "Specifications for multi-level security and a hook-up property," Proc. 1987 IEEE Symp. Research in Security and Privacy. IEEE Press, 1987.
[9] J. McLean, "The specification and modeling of computer security," Computer, vol. 23, no. 1, pp. 9-16, 1990.
[10] J. McLean,"Security models and information flow," IEEE Symp. Security and Privacy, pp. 180-187,Oakland, Calif., May 1990.
[11] J. McLean, "Proving noninterference and functional correctness using traces," J. Computer Security, vol. 1, no. 1, pp. 37-57, 1992.
[12] J. McLean, "Models of confidentiality: Past, present, and future," Proc. Computer Security Foundations Workshop VI. IEEE Press, 1993.
[13] J. McLean, "A general theory of composition for trace sets closed under selective interleaving functions," Proc. 1994 IEEE Symp. Research in Security and Privacy. IEEE Press, 1994.
[14] J. McLean, "Security Models," Encyclopedia of Software Engineering, J. Marciniak, ed. John Wiley&Sons, 1994.
[15] C. Meadows, "Using traces based on procedure calls to reason about composability," Proc. 1992 IEEE Symp. Research in Security and Privacy. IEEE Press, 1992.
[16] J. Millen, "Hookup security for synchronous machines," Proc. Computer Security Foundations Workshop III. IEEE Press, 1990.
[17] C. O'Halloran, "A calculus of information flow," Proc. European Symp. Research in Computer Security,Toulouse, France, 1990.
[18] J.T. Wittbold and D. Johnson, "Information flow in nondeterministic systems," Proc. 1990 IEEE Symp. Research in Security and Privacy. IEEE Press, 1990.
[19] J. Rushby, "Design and verification of secure systems," Proc Eighth Symp. Operating System Principles. ACM, 1981.
[20] I. Sutherland, "A model of information," Proc. Ninth Nat'l Computer Security Conf.,Gaithersburg, Md., 1986.

Index Terms:
Computer security, security models, composition, information flow.
Citation:
John McLean, "A General Theory of Composition for a Class of "Possibilistic" Properties," IEEE Transactions on Software Engineering, vol. 22, no. 1, pp. 53-67, Jan. 1996, doi:10.1109/32.481534
Usage of this product signifies your acceptance of the Terms of Use.