Modular Verification of Information Flow Security in Component-Based Systems
Simon Greiner, Martin Mohr, Bernhard Beckert
We propose a novel method for the verification of information flow security in
component-based systems. The method is (a) modular w.r.t. services and
components, i.e., overall security is proved to follow from the security of
the individual services provided by the components, and (b) modular
w.r.t. attackers, i.e., verified security properties can be re-used to
demonstrate security w.r.t. different kinds of attacks. In a first step,
user-provided security specifications for individual services are verified
using program analysis techniques. In a second step, firstorder formulas are
generated expressing that component non-interference follows from
service-level properties and in a third step that global system security
follows from component non-interference. These first-order proof obligations
are discharged with a first-order theorem prover. The overall approach is
independent of the programming language used to implement the components. We
provide a soundness proof for our method and highlight its advantages,
especially in the context of evolving systems. As a proof of concept and to
demonstrate the usability of our method, we present a case study, where we
verify the security of a system implemented in Java against two types of
attackers. We apply the program verification system KeY and the program
analysis tool Joana for analyzing individual services; modularity of our
approach allows us to use them in parallel.