Proving Non-Interference on Reachability Properties: a Refinement Approach

This paper proposes an approach to prove interference freedom for a reachability property of the form AG (psi double right arrow EF phi) in a B specification. Such properties frequently occur in security policies and information systems. Reachability is proved by constructing using stepwise algorithmic refinement an abstract program that refines AG (psi double right arrow EF phi). We propose proof obligations to show non-interference, i. e., to prove that other operations can be executed in interleaving with this program while preserving the reachability property, to cater for the multi-user aspect of information systems. Proof obligations are discharged using conventional B provers (eg, Atelier B). Since refinement preserves these reachability properties and non-interference, proofs can be conducted on abstract machines rather than implementation code.