lac-dcc / lif Goto Github PK

Currently, we deliver operation invariance to all programs, since PCFL removes all branches controlled by sensitive information. However, this might introduce non-termination into programs that originally were guaranteed to terminate. Consider the following examples:

Example 1

int foo(int secret) {
    while (use(secret)) {
        // do something
    }
}

After PCFL, the loop exit controlled by secret will no longer exist. In this case, since there are no public exits, the loop will be disconnected from the rest of the CFG. This can be determined statically and reported back to the user.

Example 2

int bar(int public, int secret) {
    while (use(secret)) {
        // do something
        if (use(public)) break;
    }
}

In this example, the loop exit controlled by secret will be erased, by the other exit controlled by public will still exist after PCFL. Furthermore, there might be values of public such that use(public) never evaluates to true, leading to an infinite loop. Unfortunately, it is not possible to determine statically whether the loop will terminate or not.

One alternative solution is to follow an approach similar to that of Constantine: come up with an upper bound for the loop, potentially reducing the information leaked but not necessarily eliminating the side-channel completely. Constantine runs a dynamic analysis to "guess" an initial value for the upper bound and then adds code to update it whenever breached during execution. Instead of running a dynamic analysis, we can rely on non-determinism to define such an upper bound:

int bar_pcfl(int public, int secret) {
    int rlimit = random(k); // number from 0 to k, uniform distribution
    while (true) {
        // do something
        if (use(public)) break;
        // is_dummy is true when the loop should have exited
        // dummy_n is the number of dummy iterations executed so far
        if (is_dummy & dummy_n == rlimit) break;
    }
}

Originally, for a particular instance p of public, each value s of secret were mapped to exactly one trace of instructions. To simplify, we can replace "trace of instructions" with "loop exits at the i-th iteration". To illustrate, consider that there are only three possible values s_i of secret and each s_i causes the loop to exit at the i-th iteration. This can be represented as follows:

where rows are indexed by the secret (X) and columns by the last iteration of the loop (Y). Each cell represents the conditional probability p(x | y). We can quantify the amount of information leaked using Bayes vulnerability, which (assuming that the secrets are uniformly distributed) can be computed as the sum of the column maximums (see the "Science of Quantitative Information" book, multiplicative Bayes leakage, uniform prior):

1 + 1 + 1 = 3 (probability of guessing the secret right is 3x greater once the functions has been executed)

Now, consider that we choose a number from 0 to 2 (inclusive) as the upper limit for the dummy iterations of the loop (all numbers are equally likely to be picked). Then, when given s_1 as secret input the loop can terminate at the 1st, 2nd or 3rd iteration; when given s_2, at the 2nd, 3rd or 4th iteration; and, when given s_3, at the 3rd, 4th or 5th iteration. Notice that there are intersections between the possible last iterations. This can be represented as follows:

The multiplicative leakage is 5 * 1/3 = 1.67. Thus, the leakage after PCFL + upper limit was reduced, but not completely eliminated.

For side-channel verification, the taint analysis considers both data and control dependencies. However, by linearizing secret-dependent branches we remove control dependencies, so our taint analysis should consider only control dependencies that remain in the program after linearization (but we need the taint analysis in order to be able to linearize something, hence the "look-ahead" term).

Consider the following piece of code:

if (use(secret)) { 
  // do something 
} else {
  // do something else
}
// pdom

The predicate that controls the if statement is data dependent on a secret. Thus, that if statement will be linearized and any control dependency from the predicate to instructions inside the then or the else paths will be removed as long as the effects of such instructions don't escape the influence region of said predicate (i.e., they don't affect anything from pdom onwards). The question then is: when does something escape the influence region of a predicate?

To the best of my knowledge, there are only two scenarios to consider:

a) phi functions

if (use(secret)) {
  x0 = 0
} else {
  x1 = 1
}

x = phi x0, x1
if (use(x)) {
  // do something
}

We already handle phi functions!

b) store + load

if (use(secret)) {
  *x = 0
} else {
  *x = 1
}

if (use(*x)) {
  // do something
}

This is currently not implemented. There are benchmarks in our test suite that contain this pattern. One example is ghostrider/dijkstra. To circumvent this problem, we currently identify and mark variables as secret by hand. In the case of dijkstra, we had to mark the vectors vis and dis as secret. This process is done as follows:

#define secret __attribute__((annotate("secret")))
secret int secret_var;