TY - GEN
T1 - Decomposition instead of self-composition for proving the absence of timing channels
AU - Antonopoulos, Timos
AU - Gazzillo, Paul
AU - Hicks, Michael
AU - Koskinen, Eric
AU - Terauchi, Tachio
AU - Wei, Shiyi
PY - 2017/6/14
Y1 - 2017/6/14
N2 - We present a novel approach to proving the absence of timing channels. The idea is to partition the program's execution traces in such a way that each partition component is checked for timing attack resilience by a time complexity analysis and that per-component resilience implies the resilience of the whole program. We construct a partition by splitting the program traces at secret-independent branches. This ensures that any pair of traces with the same public input has a component containing both traces. Crucially, the per-component checks can be normal safety properties expressed in terms of a single execution. Our approach is thus in contrast to prior approaches, such as self-composition, that aim to reason about multiple (k ≥ 2) executions at once. We formalize the above as an approach called quotient partitioning, generalized to any k-safety property, and prove it to be sound. A key feature of our approach is a demanddriven partitioning strategy that uses a regex-like notion called trails to identify sets of execution traces, particularly those influenced by tainted (or secret) data. We have applied our technique in a prototype implementation tool called Blazer, based on WALA, PPL, and the brics automaton library. We have proved timing-channel freedom of (or synthesized an attack specification for) 24 programs written in Java bytecode, including 6 classic examples from the literature and 6 examples extracted from the DARPA STAC challenge problems. Copyright is held by the owner/author(s).
AB - We present a novel approach to proving the absence of timing channels. The idea is to partition the program's execution traces in such a way that each partition component is checked for timing attack resilience by a time complexity analysis and that per-component resilience implies the resilience of the whole program. We construct a partition by splitting the program traces at secret-independent branches. This ensures that any pair of traces with the same public input has a component containing both traces. Crucially, the per-component checks can be normal safety properties expressed in terms of a single execution. Our approach is thus in contrast to prior approaches, such as self-composition, that aim to reason about multiple (k ≥ 2) executions at once. We formalize the above as an approach called quotient partitioning, generalized to any k-safety property, and prove it to be sound. A key feature of our approach is a demanddriven partitioning strategy that uses a regex-like notion called trails to identify sets of execution traces, particularly those influenced by tainted (or secret) data. We have applied our technique in a prototype implementation tool called Blazer, based on WALA, PPL, and the brics automaton library. We have proved timing-channel freedom of (or synthesized an attack specification for) 24 programs written in Java bytecode, including 6 classic examples from the literature and 6 examples extracted from the DARPA STAC challenge problems. Copyright is held by the owner/author(s).
KW - Blazer
KW - Decomposition
KW - Subtrails
KW - Timing attacks
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=85025162380&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85025162380&partnerID=8YFLogxK
U2 - 10.1145/3062341.3062378
DO - 10.1145/3062341.3062378
M3 - Conference contribution
AN - SCOPUS:85025162380
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 362
EP - 375
BT - PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - Cohen, Albert
A2 - Vechev, Martin
T2 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017
Y2 - 18 June 2017 through 23 June 2017
ER -