Failure to transform time-variant code

[casciand]

Hello,

It is stated in your paper that Lif "cannot transform a program that contains memory indexation data dependent on secret inputs", since such code is not publicly safe and cannot be made data invariant with control-flow linearization. However, I believe there are cases with data-dependent indexation that can be made operation invariant at the least. For example, the branch in the following code is not linearized by Lif even though, intuitively, it could be by using a ctsel primitive.

int main() {
  int data[2] = {0, 1};  // Public
  __attribute__((annotate("secret"))) int key = 1;  // Tainted

  if (data[key]) {  // Tainted branch is not linearized
    return 1;
  }

  return 0;
}

Of course, this example can be extended so that the code inside the branch performs more computation than a trivial return statement.

Lif reports the data-dependent index, but chooses not to linearize the branch. Is this intended behavior?

[luigidcsoares]

Hi @casciand,

Thanks for reporting this. What we meant by "cannot transform a program that contains memory indexation data dependent on secret inputs" is that this kind of code cannot be made safe just through control-flow linearization, as you said.

But, operation invariance should still be guaranteed. This is most likely a bug in the implementation of taint analysis. Looks related to issue #9, regarding dealing with loads and stores. See ghostrider/dijkstra for an example where the same (I think) issue happens and we had to deal with it manually.