Vous êtes ici : Accueil / Documents / Rapports / PROVING REACHABILITY AND NON-INTERFERENCE IN B

Marc FRAPPIER and Amel MAMMAR (2011)

PROVING REACHABILITY AND NON-INTERFERENCE IN B

Université de Sherbrooke, Technical Report (034).

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, ie, to prove that other operations can be executed in interleave 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, proofs can be conducted on abstract machines rather than implementation code.

Actions sur le document