Non-Interference For Weak Observers
David Clark, Sebastian Hunt, Pasquale Malacaria · UCL Discovery (University College London) · 2004
We consider transformational programs, i.e. those which transform inputs into outputs, with two levels of confidentiality: high and low. Inspired by Giacobazzi and Mastroeni [GM04], we consider non-interference for the case that the low confidentiality user has only partial knowledge of low inputs and low outputs. We call such a user a weak observer. We first define a form of possibilistic non-interference for weak observers; then, after demonstrating that this is not strong enough, we define a probabilistic version. The basic idea behind our approach can be summed up thus: for a weak observer, even a deterministic program behaves non-deterministically. Non-interference (NI) was first proposed by Goguen and Messeguer in 1982 [GM82] for deterministic systems. There have subsequently been a number of definitions for NI for non-deterministic systems beginning with Sutherland’s definition of Non-deducibility (ND) in 1986 [Sut86]. This latter definition still admitted some influence of high level inputs on low ones, a flaw fixed by MucCullough’s definition of Generalized NI (GNI) in the following year [McC87]. Our possibilistic definition of NI for weak observers is closely related to GNI, at least in spirit. Gray subsequently extended MucCullough’s work to incorporate probabilistic considerations in 1990, defining the notion of P-restrictiveness in [WG90]. Our probabilistic definition of NI for weak observers is closely related to this.