Architectural Refinement and Notions of Intransitive Noninterference

摘要

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.