On Information Flow and Refinement−Closure
Gavin Lowe · 2007
Abstract. The question of information flow considers whether a highlevel user of a multi-level security system can pass information to a lowlevel user. One family of information flow properties is non-deducibility on compositions: that for all possible high-level behaviours, the low-level user’s view is the same. Unfortunately, this family suffers from the refinement paradox: that a process can be classified as secure, yet a refinement can be classified as insecure. In this paper we consider the property that classifies a process as secure if all of its refinements satisfy non-deducibility on compositions. This property correctly classifies all processes for which we have performed thought experiments. The property appears, at first sight, very difficult to test automatically, because of the quantifications over all high-level behaviours and all refinements. However, we prove that it is equivalent to an operational property, and hence derive a test that can be carried out using a model checker such as FDR. We also compare the property with existing properties. We show that it is stronger than Focardi and Gorrieri’s strong bisimulation non-deducibility on compositions, but weaker than Roscoe’s lazy independence property. Finally we show that the strength of the equivalence is independent of whether the low-level user’s ability to distinguish processes is based upon stable failures or bisimulation. 1