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

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

研究成果: Conference contribution

50 被引用数 (Scopus)

抄録

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

本文言語English
ホスト出版物のタイトルPLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
編集者Albert Cohen, Martin Vechev
出版社Association for Computing Machinery
ページ362-375
ページ数14
ISBN(電子版)9781450349888
DOI
出版ステータスPublished - 2017 6月 14
外部発表はい
イベント38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017 - Barcelona, Spain
継続期間: 2017 6月 182017 6月 23

出版物シリーズ

名前Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Part F128414

Other

Other38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017
国/地域Spain
CityBarcelona
Period17/6/1817/6/23

ASJC Scopus subject areas

  • ソフトウェア

フィンガープリント

「Decomposition instead of self-composition for proving the absence of timing channels」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル