Securing the SSA Transform

Preview

Lawton will present “Securing the SSA Transform” by Chaoqiang Deng and Kedar Namjoshi.

Summary

SSA form can sadly introduce information flow leaks. Take the following program, for example:

void foo() {
    int x;
    x = read_password();
    use(x);
    x = 0; // clear password
    other();
    return;
}

Its SSA form is:

void foo() {
    int x1, x2;
    x1 = read_password();
    use(x1);
    x2 = 0; // clear password
    other();
    return;
}

Now, the register allocator might put x1 and x2 into separate registers, leaving the password in the stack for the untrusted other function to see.

This paper presents a solution to this leakage problem that recombines any variables that might leak information. It requires access to the refinement/bisimulation relations that relate the program transformations to determine these variable groupings, which limits the kinds of SSA-to-SSA transformations you’re allowed to do. The common ones like constant propagation and loop unrolling still work, though.

Discussion

In addition to the contents of the paper, we talked about what SSA is and what it’s good for, and how to create refinement relations.