Component-oriented verification of noninterference

Component-based software engineering often relies on libraries of trusted components that are combined to build dependable and secure software systems. Resource dependences, constraint conflicts, and information flow interferences arising from component combination that may violate security requirements can be revealed by means of the noninterference approach to information flow analysis. However, the security of large component-based systems may be hard to assess in an efficient and systematic way. In this paper, we propose a component-oriented formulation of noninterference that enables compositional security verification driven by system topology. This is realized by implementing scalable noninterference checks in the formal framework of a process algebraic architectural description language equipped with equivalence checking techniques.