/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 73

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 73
" /> /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 78

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 78
" /> /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 96

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 96
"/> KIT - Application-oriented Formal Verification - <br /> <b>Warning</b>: Undefined array key "title" in <b>/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php</b> on line <b>99</b><br /> <br /> <b>Warning</b>: Attempt to read property "value" on null in <b>/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php</b> on line <b>99</b><br />
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.