Information flow (information theory)
Encyclopedia
Information flow in an information theoretical
context is the transfer of information from a variable
to a variable 
in a given process.
Not all flows may be desirable. For example, a system shouldn't leak any secret (partially or not) to public observers.
s, 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. 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.
More generally, the security levels can be viewed as a lattice
with information flowing only upwards in the lattice.
For example, considering two security levels
and 
(low and high), if 
, flows from 
to 
, from 
to 
, and 
to 
would be allowed, while flows from 
to 
would not.
Where
and 
are the only two security levels in the lattice
being considered.
var l, h
l := h
The other flows fall into the side channel
category. For example, in the timing attack
or in the 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
However, this policy is too strict to be usable in realistic programs. 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).
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.
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.
every expression carries both a type (such as boolean, or integer) and a security label.
Following is a simple security type system from that enforces non-interference.
The notation
means that the expression 
has type 
. Similarly, 
means that the command 
is typable in the security context 
.
Well-typed commands include, for example,
.
Conversely, the program
is ill-typed, as it will disclose the value of variable
into 
.
Robust declassification requires that an active attacker may not manipulate the system in order to learn more secrets than what passive attackers already know.
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.
The following code example shows a declassify construct from. 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)
(i.e., who) can access a given piece of information. This kind of policy has been implemented in the Jif compiler.
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} *)
The following example makes use of the flow construct proposed in. 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
L in
l := h
Information theory
Information theory is a branch of applied mathematics and electrical engineering involving the quantification of information. Information theory was developed by Claude E. Shannon to find fundamental limits on signal processing operations such as compressing data and on reliably storing and...
context is the transfer of information from a variable
Variable (mathematics)
In mathematics, a variable is a value that may change within the scope of a given problem or set of operations. In contrast, a constant is a value that remains unchanged, though often unknown or undetermined. The concepts of constants and variables are fundamental to many areas of mathematics and...
to a variable in a given 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 listAccess control list
An access control list , with respect to a computer file system, is a list of permissions attached to an object. An ACL specifies which users or system processes are granted access to objects, as well as what operations are allowed on given objects. Each entry in a typical ACL specifies a subject...
s, firewalls
Firewall (computing)
A firewall is a device or set of devices designed to permit or deny network transmissions based upon a set of rules and is frequently used to protect networks from unauthorized access while permitting legitimate communications to pass....
, and cryptography
Cryptography
Cryptography is the practice and study of techniques for secure communication in the presence of third parties...
. However, although these methods do impose limits on the information that is released by a system, they provide no guarantees about information propagation. 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.
More generally, the security levels can be viewed as a lattice
Lattice (order)
In mathematics, a lattice is a partially ordered set in which any two elements have a unique supremum and an infimum . Lattices can also be characterized as algebraic structures satisfying certain axiomatic identities...
with information flowing only upwards in the lattice.
For example, considering two security levels
and (low and high), if , flows from to , from to , and to would be allowed, while flows from to would not.Preliminaries
Throughout this article, the following notation is used:- variable
(low) shall denote a publicly observable variable - variable
(high) shall denote a secret variable
Where
and are the only two security levels in the latticeLattice (order)
In mathematics, a lattice is a partially ordered set in which any two elements have a unique supremum and an infimum . Lattices can also be characterized as algebraic structures satisfying certain axiomatic identities...
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
Side channel attack
In cryptography, a side channel attack is any attack based on information gained from the physical implementation of a cryptosystem, rather than brute force or theoretical weaknesses in the algorithms...
category. For example, in the timing attack
Timing attack
In cryptography, a timing attack is a side channel attack in which the attacker attempts to compromise a cryptosystem by analyzing the time taken to execute cryptographic algorithms...
or in the power analysis attack
Power analysis
In cryptography, power analysis is a form of side channel attack in which the attacker studies the power consumption of a cryptographic hardware device...
, 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
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. 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.
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 systemType system
A type system associates a type with each computed value. By examining the flow of these values, a type system attempts to ensure or prove that no type errors can occur...
every expression carries both a type (such as boolean, or integer) and a security label.
Following is a simple security type system from that enforces non-interference.
The notation
means that the expression has type . Similarly, means that the command is typable in the security context .Well-typed commands include, for example,
.Conversely, the program
is ill-typed, as it will disclose the value of variable
into .Declassification
As shown previously, non-interference policy is too strict for use in most real-world applications. 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.
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.
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. 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 principalsSecurity principal
A principal in Computer Science is an entity that can be authenticated by a computer system or network. Authentication is the process of validating and confirming the identity of such an entity....
(i.e., who) can access a given piece of information. This kind of policy has been implemented in the Jif compiler.
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. 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
L inl := h