Abstract
This paper deals with architectural designs that specify components of a system and the permitted flows of information between them. In the process of systems development, one might refine such a design by viewing a component as being composed of subcomponents, and specifying permitted flows of information between these subcomponents and others in the design. The paper studies the soundness of such refinements with respect to a spectrum of different semantics for information flow policies. These include Goguen and Meseguer’s purge-based definition, Haigh and Young’s intransitive purge-based definition, and some more recent notions TA-security, TO-security and ITO-security defined by van der Meyden. It is also shown that refinement preserves weak access control structure, an implementation mechanism that ensures TA-security.
Work supported by Australian Research Council Discovery grant DP0451529.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alves-Foss, J., Harrison, W.S., Oman, P., Taylor, C.: The MILS architecture for high-assurance embedded systems. International Journal of Embedded Systems 2(3/4), 239–247 (2006)
Barbosa, M.A.: A refinement calculus for software components and architectures. ACM SIGSOFT Software Engineering Notes, 30(5) (September 2005)
Bell, D.E., La Padula, L.J.: Secure computer system: unified exposition and multics interpretation. Technical Report ESD-TR-75-306, Mitre Corporation, Bedford, M.A. (March 1976)
Bibighaus, D.: Applying the doubly labeled transition system to the refinement paradox. PhD thesis, Naval Postgraduate School, Monterey (2006)
Bossi, A., Focardi, R., Piazza, C., Rossi, S.: Refinement operators and information flow security. In: Proc. Int. Conf. on Software Engineering and Formal Methods, pp. 44–53 (2003)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, Oakland, pp. 11–20 (1982)
Graham-Cunning, J., Sanders, J.: On the refinement of noninterference. In: Proc. IEEE Computer Security Foundations Workshop, pp. 35–42 (1991)
Haigh, J.T., Young, W.D.: Extending the noninterference version of MLS for SAT. IEEE Trans. on Software Engineering SE-13(2), 141–150 (1987)
Jacob, J.: On the derivation of secure components. In: Proc. IEEE Symp. on Security and Privacy, pp. 242–247 (1989)
JĂĽrjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005)
Mantel, H.: Preserving information flow properties under refinement. In: Proc. IEEE Symp. Security and Privacy, pp. 78–91 (2001)
van der Meyden, R.: A comparison of semantic models of intransitive noninterference (submitted for publication) (December 2007), http://www.cse.unsw.edu.au/~meyden
van der Meyden, R.: What, indeed, is intransitive noninterference? (submitted for publication, copy at http://www.cse.unsw.edu.au/~meyden – an extended abstract of this paper appears in Proc. ESORICS 2007) (January 2008)
Moriconi, M., Qian, X.: Correctness and composition of software architectures. In: Proc. 2nd ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 164–174 (1994)
Moriconi, M., Qian, X., Riemenschneider, R.A., Gong, L.: Secure software architectures. In: Proc. IEEE Symp. on Security and Privacy, pp. 884–893 (1997)
Moriconi, M., Qian, X., Riemenschneider, R.A.: Correct architecture refinement. IEEE Transactions on Software Engineering 21(4), 356–372 (1995)
O’Halloran, C.: Refinement and confidentiality. In: Fifth Refinement Workshop, pp. 119–139. British Computer Society (1992)
Philipps, J., Rumpe, B.: Refinement of information flow architectures. In: Proc. 1st IEEE Int. Conf. on Formal Engineering Methods, pp. 203–212 (1997)
Roscoe, A.W., Goldsmith, M.H.: What is intransitive noninterference? In: IEEE Computer Security Foundations Workshop, pp. 228–238 (1999)
Roscoe, A.W.: CSP and determinism in security modelling. In: Proc. IEEE Symp. on Security and Privacy, pp. 114–221 (1995)
Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical Report CSL-92-02, SRI International (December 1992)
Rushby, J.M., Randell, R.: A distributed secure system. IEEE Computer 16(7), 55–67 (1983)
Seehusen, F., Stolen, K.: Information flow property preserving transformation of UML interaction diagrams. In: Proc. ACM symposium on access control models and technologies, pp. 150–159 (2006)
Vanfleet, W.M., Beckworth, R.W., Calloni, B., Luke, J.A., Taylor, C., Uchenick, G.: MILS:architecture for high assurance embedded computing. Crosstalk: The Journal of Defence Engineering, 12–16 (August 2005)
Zhou, J., Alves-Foss, J.: Architecture-based refinements for secure computer system design. In: Proc. Policy, Security and Trust (November 2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van der Meyden, R. (2009). Architectural Refinement and Notions of Intransitive Noninterference . In: Massacci, F., Redwine, S.T., Zannone, N. (eds) Engineering Secure Software and Systems. ESSoS 2009. Lecture Notes in Computer Science, vol 5429. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00199-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-00199-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00198-7
Online ISBN: 978-3-642-00199-4
eBook Packages: Computer ScienceComputer Science (R0)