Non-interference (security)
   HOME

TheInfoList



OR:

Noninterference is a strict multilevel security policy model, first described by Goguen and Meseguer in 1982, and amplified further in 1984.


Introduction

In simple terms, a computer is modeled as a machine with inputs and outputs. Inputs and outputs are classified as either ''low'' (low sensitivity, not highly classified) or ''high'' (sensitive, not to be viewed by uncleared individuals). A computer has the noninterference property if and only if any sequence of low inputs will produce the same low outputs, regardless of what the high level inputs are. That is, if a low (uncleared) user is working on the machine, it will respond in exactly the same manner (on the low outputs) whether or not a high (cleared) user is working with sensitive data. The low user will not be able to acquire any
information Information is an abstract concept that refers to that which has the power to inform. At the most fundamental level information pertains to the interpretation of that which may be sensed. Any natural process that is not completely random, ...
about the activities (if any) of the high user.


Formal expression

Let M be a memory configuration, and let M_\text and M_H be the projection of the memory M to the low and high parts, respectively. Let be the function that compares the low parts of the memory configurations, i.e., M\ \ M^\prime iff M_\text = M_\text^\prime. Let (P,M) \rightarrow^* M^\prime be the execution of the program P starting with memory configuration M and terminating with the memory configuration M^\prime. The definition of noninterference for a deterministic program P is the following: \begin\forall M_1, M_2 :\; & M_1\ \ M_2 & \land\\ & (P,M_1) \rightarrow^* M_1^\prime & \land\\ &(P,M_2) \rightarrow^* M_2^\prime &\Rightarrow\\ &M_1^\prime\ \ M_2^\prime\end


Limitations


Strictness

This is a very strict policy, in that a computer system with
covert channels In computer security, a covert channel is a type of attack that creates a capability to transfer information objects between processes that are not supposed to be allowed to communicate by the computer security policy. The term, originated in 19 ...
may comply with, say, the
Bell–LaPadula model The Bell–LaPadula Model (BLP) is a state machine model used for enforcing access control in government and military applications. It was developed by David Elliott Bell and Leonard J. LaPadula, subsequent to strong guidance from Roger R. Sch ...
, but will not comply with noninterference. The reverse could be true (under reasonable conditions, being that the system should have labelled files, etc.) except for the "No classified information at startup" exceptions noted below. However, noninterference has been shown to be stronger than nondeducibility. This strictness comes with a price. It is very difficult to make a computer system with this property. There may be only one or two commercially available products that have been verified to comply with this policy, and these would essentially be as simple as switches and one-way information filters (although these could be arranged to provide useful behaviour).


No classified information at startup

If the computer has (at time = 0) any high (i.e., classified) information within it, or low users create high information subsequent to time=0 (so-called "write-up", which is allowed by many computer security policies), then the computer can legally leak all that high information to the low user, and can still be said to comply with the noninterference policy. The low user will not be able to learn anything about high user activities, but can learn about any high information that was created through means other than the actions of high users. (von Oheimb 2004) Computer systems that comply with the Bell–LaPadula Model do not suffer from this problem since they explicitly forbid "read-up". Consequently, a computer system that complies with noninterference will not necessarily comply with the Bell–LaPadula Model. Thus, the
Bell–LaPadula model The Bell–LaPadula Model (BLP) is a state machine model used for enforcing access control in government and military applications. It was developed by David Elliott Bell and Leonard J. LaPadula, subsequent to strong guidance from Roger R. Sch ...
and the noninterference model are incomparable: the Bell–LaPadula Model is stricter regarding read-up, and the noninterference model is stricter with respect to
covert channels In computer security, a covert channel is a type of attack that creates a capability to transfer information objects between processes that are not supposed to be allowed to communicate by the computer security policy. The term, originated in 19 ...
.


No summarisation

Some legitimate multilevel security activities treat individual data records (e.g., personal details) as sensitive, but allow statistical functions of the data (e.g., the mean, the total number) to be released more widely. This cannot be achieved with a noninterference machine.


Generalizations

The noninterference property requires that the system should not reveal any information about the high inputs from the observable output for various low inputs. However, one can argue that achieving noninterference is oftentimes not possible for a large class of practical systems, and moreover, it may not be desirable: programs need to reveal information that depends on the secret inputs, e.g. the output must be different when a user enters a correct credential vs. when she enters incorrect credentials. Shannon entropy, guessing entropy, and min-entropy are prevalent notions of quantitative information leakage that generalize noninterference.Boris Köpf and David Basin. 2007. An Information-theoretic Model for Adaptive Side-channel Attacks. In Proceedings of the 14th ACM Conference on Computer and Communications Security (CCS '07). ACM, New York, NY, USA, 286–296.


References


Further reading

* * {{DEFAULTSORT:Noninterference (Security) Computer security models