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;
}