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 (Ψ → EF φ) 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 (Ψ → EF φ). 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.