View source for Characterizations of the category of topological spaces

'''Information flow''' in an [[information theory|information theoretical]] context is the transfer of information from a [[Variable (mathematics)|variable]] <math>x</math> to a variable <math>y</math> in a given [[wikt:process|process]].
Not all flows may be desirable. For example, a system shouldn't leak any secret (partially or not) to public observers.

== Introduction ==

Securing the data manipulated by computing systems has been a challenge in the past years. Several methods to limit the information disclosure exist today, such as [[access control list]]s, [[Firewall (computing)|firewalls]], and [[cryptography]]. However, although these methods do impose limits on the information that is released by a system, they provide no guarantees about information ''propagation''.<ref name="sabelfeld03">Andrei Sabelfeld and Andrew C. Myers. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, 21(1), Jan. 2003.</ref> For example, access control lists of file systems prevent unauthorized file access, but they do not control how the data is used afterwards. Similarly, cryptography provides a means to exchange information privately across a non-secure channel, but no
guarantees about the confidentiality of the data are given once it is decrypted.

In low level information flow analysis, each variable is usually assigned a security level. The basic model comprises two distinct levels: low and high, meaning, respectively, publicly observable information, and secret information. To ensure confidentiality, flowing information from high to low variables should not be allowed. On the other hand, to ensure integrity, flows to high variables should be restricted.<ref name="sabelfeld03"/>

More generally, the security levels can be viewed as a [[Lattice (order)|lattice]] with information flowing only upwards in the lattice.<ref name="denning76">Dorothy Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236-242, 1976.</ref>

For example, considering two security levels <math>L</math> and <math>H</math> (low and high), if <math>L \le H</math>, flows from <math>L</math> to <math>L</math>, from <math>H</math> to <math>H</math>, and <math>L</math> to <math>H</math> would be allowed, while flows from <math>H</math> to <math>L</math> would not.<ref name="smith07">{{cite conference
  | first = Geoffrey
  | last = Smith
  | title = Principles of Secure Information Flow Analysis
  | booktitle = Advances in Information Security
  | volume = 27
  | pages = 291–307
  | publisher = Springer US
  | year = 2007}}</ref>

== Preliminaries ==

Throughout this article, the following notation is used:
* variable <math>l \in L</math> (low) shall denote a publicly observable variable
* variable <math>h \in H</math> (high) shall denote a secret variable

Where <math>L</math> and <math>H</math> are the only two security levels in the [[Lattice (order)|lattice]] being considered.

== Explicit Flows and Side Channels ==

Information flows can be divided in two major categories. The simplest one is explicit flow, where some secret is explicitly leaked to a publicly observable variable. In the following example, the secret in the variable ''h'' flows into the publicly observable variable ''l''.

 '''var''' l, h
 l := h

The other flows fall into the [[Side channel attack|side channel]] category. For example, in the [[timing attack]] or in the [[Power analysis|power analysis attack]], the system leaks information through, respectively, the time or power it takes to perform an action depending on a secret value.

In the following example, the attacker can deduce if the value of ''h'' is one or not by the time the program takes to finish:

 '''var''' l, h
 '''if''' h = 1 '''then'''
   (* do some time-consuming work *)
 l := 0

Another side channel flow is the implicit information flow, which consists in leakage of information through the program control flow. The following program (implicitly) discloses the value of the secret variable ''h'' to the variable ''l''. In this case, since the ''h'' variable is boolean, all the bits of the variable of ''h'' is disclosed (at the end of the program, ''l'' will be 3 if ''h'' is true, and 42 otherwise).

 '''var''' l, h
 '''if''' h = true '''then'''
   l := 3
 '''else'''
   l := 42

== Non-Interference ==
{{Main|Non-interference (security)}}

Non-interference is a policy that enforces that an attacker should not be able to distinguish two computations from their outputs if they only vary in their secret inputs.
However, this policy is too strict to be usable in realistic programs.<ref name="sabelfeld05"/> The classic example is a password checker program that, in order to be useful, needs to disclose some secret information: whether the input password is correct or not (note that the information that an attacker learns in case the program ''rejects'' the password is that the attempted password is ''not'' the valid one).

== Information flow control ==

A mechanism for ''information flow control'' is one that enforces information flow policies. Several methods to enforce information flow policies have been proposed. Run-time mechanisms that tag data with information flow labels have been employed at the operating system level and at the programming language level. Static program analyses have also been developed that ensure information flows within programs are in accordance with policies.

Both static and dynamic analysis for current programming languages have been developed. However, dynamic analysis cannot be sound as noninterference is a property concerning all execution paths.<ref>
Dennis M. Volpano. Safety versus Secrecy, Proc. of the 6th International Symposium on Static Analysis, 1999.</ref>

A prominent way to enforce information flow policies in a program is through a security type system: that is, a type system that enforces security properties. In such a sound type system, if a program type-checks, it meets the flow policy and therefore contains no improper information flows.

=== Security type system ===

In a programming language augmented with a security [[type system]] every expression carries both a type (such as boolean, or integer) and a security label.

Following is a simple security type system from <ref name="sabelfeld03"/> that enforces non-interference.
The notation <math>\;\vdash exp\;:\; \tau</math> means that the expression <math>exp</math> has type <math>\;\tau</math>. Similarly, <math>[sc] \vdash C</math> means that the command <math>C</math> is typable in the security context <math>sc</math>.

<math>
[E1-2] \quad \vdash exp : high \qquad \frac{h \notin Vars(exp)}{\vdash exp \;:\; low}
</math>

<math>
[C1-3] \quad [sc] \vdash \textbf{skip} \qquad [sc] \vdash h \;:=\; exp \qquad \frac{\vdash exp \;:\; low}{[low] \vdash l \;:=\; exp}
</math>

<math>
[C4-5] \quad \frac{[sc] \vdash C_1 \quad [sc] \vdash C_2}{[sc] \vdash C_1\; ;\; C_2} \qquad \frac{\vdash exp \;:\; sc \quad [sc] \vdash C}{[sc] \vdash \textbf{while}\ exp\ \textbf{do}\ C}
</math>

<math>
[C6-7] \quad \frac{\vdash exp \;:\; sc \quad [sc] \vdash C_1 \quad [sc] \vdash C_2}{[sc] \vdash \textbf{if}\ exp\ \textbf{then}\ C_1\ \textbf{else}\ C_2} \qquad \frac{[high] \vdash C}{[low] \vdash C}
</math>

Well-typed commands include, for example,
:<math>[low] \vdash\ \textbf{if}\ l = 42\ \textbf{then}\ h\;:=\; 3\ \textbf{else}\ l\;:=\;0</math>.

Conversely, the program
:<math>l\;:=\;0\ ;\ \textbf{while}\ l < h\ \textbf{do}\ l\;:=\;l + 1</math>
is ill-typed, as it will disclose the value of variable <math>h</math> into <math>l</math>.

== Declassification ==

As shown previously, non-interference policy is too strict for use in most real-world applications.{{Citation needed|date=March 2012}} Therefore, several approaches to allow controlled releases of information have been devised. Such approaches are called information declassification.

Robust declassification requires that an active attacker may not manipulate the system in order to learn more secrets than what passive attackers already know.<ref name="sabelfeld05">Andrei Sabelfeld and David Sands. Dimensions and Principles of Declassification. In Proc. of the IEEE Computer Security Foundations Workshop, 2005.</ref>

Information declassification constructs can be classified in four orthogonal dimensions: ''What'' information is released, ''Who'' is authorized to access the information, ''Where'' the information is released, and ''When'' is the information released.<ref name="sabelfeld05"/>

=== What ===

A ''what'' declassification policy controls which information (partial or not) may be released to a publicly observable variable.

The following code example shows a '''declassify''' construct from.<ref name="sabelfeld04">A. Sabelfeld and A. C. Myers. A model for delimited information release. In Proc. of International Symposium on Software Security (ISSS) 2003.</ref> In this code, the value of the variable ''h'' is explicitly allowed by the programmer to flow into the publicly observable variable ''l''.

 '''var''' l, h
 '''if''' l = 1 '''then'''
   l := '''declassify'''(h)

=== Who ===

A ''who'' declassification policy controls which [[Security principal|principals]] (i.e., who) can access a given piece of information. This kind of policy has been implemented in the Jif compiler.<ref>[http://www.cs.cornell.edu/jif/ Jif: Java information flow]</ref>

The following example allows Bob to share its secret contained in the variable ''b'' with Alice through the commonly accessible variable ''ab''.

 '''var''' ab                                ''(* {Alice, Bob} *)''
 '''var''' b                                 ''(* {Bob} *)''
 '''if''' ab = 1 '''then'''
   ab := '''declassify'''(b, {Alice, Bob})   ''(* {Alice, Bob} *)''

=== Where ===

A ''where'' declassification policy regulates where the information can be released, for example, by controlling in which lines of the source code information can be released.

The following example makes use of the '''flow''' construct proposed in.<ref name="matos05">A. Almeida Matos and G. Boudol. On declassification and the non-disclosure policy. In Proc. IEEE Computer Security Foundations Workshop 2005.</ref> This construct takes a flow policy (in this case, variables in H are allowed to flow to variables in L) and a command, which is run under the given flow policy.

 '''var''' l, h
 '''flow''' H <math>\prec</math> L '''in'''
   l := h

=== When ===

A ''when'' declassification policy regulates when the information can be released. These kind of policies can be used to verify programs that implement, for example, controlled release of secret information after payment, or encrypted secrets which should not be released in a certain time given polynomial computational power.

==References==

{{reflist}}

{{DEFAULTSORT:Information Flow (Information Theory)}}
[[Category:Information theory]]