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 contributionpeer-review

65 Scopus citations

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
Pages362-375
Number of pages14
ISBN (Electronic)9781450349888
DOIs
StatePublished - 14 Jun 2017
Event38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017 - Barcelona, Spain
Duration: 18 Jun 201723 Jun 2017

Publication series

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

Conference

Conference38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017
Country/TerritorySpain
CityBarcelona
Period18/06/1723/06/17

Keywords

  • Blazer
  • Decomposition
  • Subtrails
  • Timing attacks
  • Verification

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