Decomposition instead of self-composition for proving the absence of timing channels

Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, Shiyi Wei

Research output: Chapter in Book/Report/Conference proceedingConference contribution

38 Citations (Scopus)

Abstract

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).

Original languageEnglish
Title of host publicationPLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsAlbert Cohen, Martin Vechev
PublisherAssociation for Computing Machinery
Pages362-375
Number of pages14
ISBN (Electronic)9781450349888
DOIs
Publication statusPublished - 2017 Jun 14
Externally publishedYes
Event38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017 - Barcelona, Spain
Duration: 2017 Jun 182017 Jun 23

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
VolumePart F128414

Other

Other38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017
CountrySpain
CityBarcelona
Period17/6/1817/6/23

Keywords

  • Blazer
  • Decomposition
  • Subtrails
  • Timing attacks
  • Verification

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Decomposition instead of self-composition for proving the absence of timing channels'. Together they form a unique fingerprint.

  • Cite this

    Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T., & Wei, S. (2017). Decomposition instead of self-composition for proving the absence of timing channels. In A. Cohen, & M. Vechev (Eds.), PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 362-375). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI); Vol. Part F128414). Association for Computing Machinery. https://doi.org/10.1145/3062341.3062378