Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels. Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI), June 2017.

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 demand-driven 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.

[ .pdf ]

  AUTHOR = {Timos Antonopoulos and Paul Gazzillo and Michael Hicks and Eric Koskinen and Tachio Terauchi and Shiyi Wei},
  BOOKTITLE = {Proceedings of the {ACM} Conference on Programming Language Design and Implementation (PLDI)},
  TITLE = {Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels},
  YEAR = 2017

This file has been generated by bibtex2html 1.69