Non-Interference with What-Declassification in Component-Based Systems

Component-based design is a method for modular design of systems. The structure of component-based systems follows specific rules and single components make assumptions on the environment that they run in. In this paper, we provide a noninterference property for component-based systems that allows for a precise specification of what-declassification of information and takes assumptions on the environment into consideration in order to allow a modular, precise and re-usable information-flow analysis. For precise analysis, components can be analyzed by separately analysing services provided by a component, and from our compositionality theorem non-interference of components follows.