An Interpreter Secure for Timing Leaks

Programs which manipulate both secret and public data can be induced to leak secrets to an attacker by supplying them with varying public inputs and measuring the time they take to respond. If the execution time depends at all on the secret values, then this dependence can be exploited to leak them. Even differences caused by cache behaviour, measured over an internet connection, are significant enough to enable a leak of several bits per minute -- fast enough to leak a credit card number in a realistic time. Thus secure programs must guarantee to execute in the same time, regardless of the secret values.

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:

Johan Agat will take part in the supervision. Success should lead to a publishable article.
Last modified: Wed Jan 31 11:40:50 MET 2001