Modular Verification of Information Flow Security in Component-Based Systems:
Proofs and Proof of Concept
Simon Greiner, Martin Mohr, Bernhard Beckert
Distributed component-based systems engineering is a method that allows to
modularily implement large and complex systems where the functionality
provided by one component as so-called services, depends on functionality
provided by other components. Systems implemented according to the
component-based system paradigm allow high scalability. In the paper Modular
Verification of Information Flow Security in Component-Based Systems we
propose a sound and modular method that allows to identify and verify flows of
information caused by single services. We show how those individual flows can
be formalized as so-called dependency clusters, and how dependency clusters
can be used as building blocks to modularily construct system-wide security
specifications in a sound way.
This technical report accompanies the original paper and we assume the reader
to be familiar with the original work. We provide here the formal proofs for
the theorems discussed there. Further, we provide a detailed description of
the proof of concept addressed in the original work.