Proving Non-interference on Reachability Properties: A Refinement Approach

This paper proposes an approach to prove interference freedom for a reach ability property of the form AG (ψ =>; EF Φ) in a B specification. Such properties frequently occur in security policies and information systems. Reach ability is proved by constructing using stepwise algorithmic refinement an abstract program that refines AG (ψ =>; EF Φ). We propose proof obligations to show non-interference, ie, to prove that other operations can be executed in interleaving with this program while preserving the reach ability 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 reach ability properties and non-interference, proofs can be conducted on abstract machines rather than implementation code.