An Interpreter Secure for Timing Leaks

Johan Agat studied this problem in his doctoral thesis. He developed a tool that transforms a program secure against direct leaks (e.g. simply sending the secret data to the attacked in a message) into one secure against most timing leaks also. However, the transformation can blow up the code size, and moreover transformed programs are still vulnerable to leaks depending on the instruction cache, since different code may be executed depending on secret values.

The goal of this project is to implement a timing secure interpreter instead, which interprets a program in a secure way, based on the ideas in Johan Agat's transformation. Such an interpreter must fit in the instruction cache (so that differing execution paths do not lead to different cache behaviour), and must perform the same sequence of memory operations regardless of the secret data values. The basic idea is to simulate both branches of a conditional with a secret condition, but keep the effects of only one branch. A suitable language to interpret would be based on the while-language of Agat's thesis, roughly:

s ::= H | L
e ::= n | x | e op e | e[e] | e.x
c ::= x := e | let x S = inite in c | if (e) c else c
    | while (e) c | c; c

Suggested workplan:

• Implement a prototype interpreter in Haskell, to define its behaviour precisely and ensure it is well understood.
• Implement an interpreter in C (possibly using a Haskell front-end to translate programs to a convenient form).
• Perform experiments to verify that programs are run securely.