Tutorial
This tutorial will give a brief introduction to
information flow control, and how it is implemented in JSFlow.
Usage
To start using JSFlow, download the
JSFlow package and unpack it. Ensure
NodeJS and
npm are installed. Once unpacked, enter the directory and execute
npm install
. This
should install all the necessary libraries. If that fail, manually install
esprima,
escodegen,
estraverse,
source-map and
underscore. It is recommended to use npm
to do this.
Programming towards JSFlow is similar to programming towards standard JavaScript, with the main difference being labeling primitives. In the unpacked directory, execute
./jsflow
to run an interactive shell, or execute
./jsflow filepath
, which will execute the JavaScript file pointed to by
filepath
.
Dynamic Information Flow Control
In our work, we work with dynamic information flow control (IFC). In dynamic IFC, all runtime values are augmented with a security label, which are copied and joined to reflect the computations of a program. The labels are drawn from a lattice, in litterature
usually denoted as
L and
H for
low (public) and
high (private) data.
When tracking the information flow during execution, a
program counter (pc) is used. As an example, the pc is upgraded when the program branches on a secret variable, and hence reflects the current
security context, i.e. the security level of the current computation.
For a program to be of any use, it must take inputs and produce outputs. We call inputs to a program
sources, and outputs from the program
sinks. With this, there are two types of flows to look for in IFC:
explicit and
implicit flows. In explicit flows, the data flow is used to leak information by writing from a private source to a public sink. As an example,
l := h
has an explicit flow from the private source
h
to the public
sink
l
. On the other hand, implicit flows use the control flow of a program to leak the secret to a public sink, without explicitly writing from the private source. To illustrate this, if we assume
h
is of boolean type,
l := false; if(h) l := true;
would leak the secret source
h
to the public sink
l
, without an explicit assignment between the source and the sink. With this, we can define a common security property for IFC, namely
noninterference Noninterference
states public output must not depend on private input. More intuitively, a program satisfies noninterference if, for all runs of a program, if the only difference between the runs are the private input, then the public output should remain the
same. One of the security models of noninterference is
termination insensitive noninterference(TINI), which guarantees noninterference for terminating executions of an application. In practice, this means applications that leak through
the termination behaviour of a program are allowed, given it is the termination behaviour only that produces the leak. As an example, have a look at the following example.
/* Assuming h is a secret variable of type Number defined elsewhere.
* Also assume the attacker can observe the output done by print. */
for(var i = Number.MIN_VALUE; i <= Number.MAX_VALUE; i++) {
print(i);
if(i == h) {
while(true) { }
}
}
Assuming
print
prints to a public sink which the attacker can observe, the secret value
h
is leaked. For each iteration, the variable
i
is public: it never depends on a secret. This means printing
i
to a public sink is always allowed. The only time the application will branch on a secret is in the if-statement
if(i == h)
. But branching there will make the application run an infinite loop, and never terminate, indicating
the last written output to the public sink will be the secret value. Since the leak only depends on the non-termination in the branch, this would be allowed for systems which employ TINI.
To help achieve noninterference, one must handle side-effects under secret control carefully. If security labels are allowed to change under secret control, there can be implicit flows into the labels. To help prevent this, there
is the concept of
no sensitive upgrade (NSU). NSU states that security labels are not allowed to change under secret control. What would be the effect if labels are allowed to change under secret control? The following example illustrate
this well.
/* For this example, we assume lo and tm to be public values.
* hi is a secret boolean value, defined elsewhere. */
var lo = true;
var tm = true;
if(hi === true) {
tm = false;
}
if(tm === true) {
lo = false;
}
Lets follow the execution, and assume that there is no NSU, i.e. labels are allowed to change freely under secret control. If
hi
is
true
, then the body of the if-statement
if(hi === true)
will
execute under secret control. When this happens,
tm
will be given the value
false
, and its label will be upgraded to the label of
hi
. Since
tm
now is
false
, the body of the if-statement
if(tm === true)
will not execute, leaving
lo
with the value
true
, and a public label.
On the other hand, if
hi
is
false
, the body of the if-statement
if(hi === true)
will never execute, leaving
tm
with the value
true
and a public label. This means the guard in the if-statement
if(tm === true)
is
true
, and the body will be executed.
However, since
tm
was public, the body is executed under public control, giving
lo
the value
false
with a public label.
In both instances, the value of
hi
is leaked to
lo
, with
lo
keeping a public label. But with NSU, the assignment
tm = false
is not allowed, as it would change the label of
tm
under secret control. If
hi
is false,
lo
would be
false
and public. This is a one-bit leak that cannot be prevented with NSU.
JSFlow
JSFlow is a JavaScript interpreter which is extended with security labels on the values. It supports all the standard libraries defined in the
Ecma v5 standard, but it does not support
strict mode. JSFlow has the security property of TINI, and uses NSU.
If not provided by the programmer of an application, JSFlow employs a two-level lattice: public and secret, where public values are allowed to flow to secret. In principle, the lattice in JSFlow is a subset lattice, meaning that the
label(s) of a sink must be a subset of the label(s) of the source. In order to label values, one must call the built-in function
lbl
which, given a value, will label the value. As an example,
var x = lbl(42);
will give
the variable
x
the value
42
, and the label
T
for Top, i.e. the top value of the lattice, which is secret. We can verify this by executing
print(x);
, which gives the output
(<>)42_<T>
,
indicating the pc is public (
(<>)
), the value is
42
, and its label is Top (
<T>
).
We can see the execution context change by having
if(x) print(x);
. Since
x
is defined, the body of the if-statement will be executed. When
print(x)
is executed, it will print
(<T>)42_<T>
.
This is due to branching on the secret variable
x
will upgrade the pc to sensitive.
In JSFlow, a pure explicit flow is allowed. As an example, imagine the secret variable
h
and the public variable
l
. If we execute the program
l = h
in JSFlow, the label of
l
would
simply be upgraded, as the execution context is public. Without any branching, this is always allowed.
If, however, we add an if-statement:
l = false; if(h) l = true;
, given
h
is defined to a value which can be interpreted as
true
, JSFlow would detect the implicit flow and prevent it.
On the other and, a combination of these can be allowed.
l = h; // This is allowed, and l will become secret.
if(h) {
l = 42; // This is allowed, since l is now secret, i.e. NSU will not trigger.
}
Although there is an implicit flow to
l
depending on the secret value
h
, since
l
has been upgraded on the first line, it is a safe implicit flow. Similarly, JSFlow would prevent the NSU example from before as well.
More advanced labeling in JSFlow
If the standard two-level lattice is not enough, one can use
lbl
to create their own labels for the values. As an example,
var x = lbl(42, "my-extremely-secret-value");
will label the variable
x
with the
label
my-extremely-secret-value
, and
var y = lbl(42, "secret-value", "extremely-secret-value");
will label
y
with both
secret-value
and
extremely-secret-value
. Since JSFlow employs a subset lattice, in order for
x
to be allowed to flow to
y
, the labels of
x
must be a subset of the labels of
y
.
This means the following is not allowed in JSFlow, due to the labels of
m
not being a subset of the labels of
h
.
var l = lbl(10, 'low');
var m = lbl(15, 'mid');
var h = lbl(20, 'high');
if(m === 15) {
/* This assignment is not allowed due to execution context containing the
label 'mid', which h does not have.*/
h = 25;
}
Instead, we must label the variable
h
to both
mid
and
high
in order for the assignment to be allowed. If
h
is labeled in this manner, the labels of
m
becomes a subset
of the labels of
h
.
var l = lbl(10, 'low');
var m = lbl(15, 'mid');
var h = lbl(20, 'mid', 'high');
if(m === 15) {
/* This assignment is allowed, since h has 'mid' as label (as well as 'high'),
so h is at least as sensitive as m. Note that h, after the assignment, will
only have label 'mid' (due to dynamic execution)*/
h = 25;
}