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

25 引用 (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
出版者Association for Computing Machinery
ページ362-375
ページ数14
Part F128414
ISBN(電子版)9781450349888
DOI
出版物ステータスPublished - 2017 6 14
外部発表Yes
イベント38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017 - Barcelona, Spain
継続期間: 2017 6 182017 6 23

Other

Other38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017
Spain
Barcelona
期間17/6/1817/6/23

Fingerprint

Decomposition
Chemical analysis
Acoustic waves
Specifications
Side channel attack

ASJC Scopus subject areas

  • Software

これを引用

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. : PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (巻 Part F128414, pp. 362-375). Association for Computing Machinery. https://doi.org/10.1145/3062341.3062378

Decomposition instead of self-composition for proving the absence of timing channels. / Antonopoulos, Timos; Gazzillo, Paul; Hicks, Michael; Koskinen, Eric; Terauchi, Tachio; Wei, Shiyi.

PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 巻 Part F128414 Association for Computing Machinery, 2017. p. 362-375.

研究成果: Conference contribution

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. : PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 巻. Part F128414, Association for Computing Machinery, pp. 362-375, 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, 17/6/18. https://doi.org/10.1145/3062341.3062378
Antonopoulos T, Gazzillo P, Hicks M, Koskinen E, Terauchi T, Wei S. Decomposition instead of self-composition for proving the absence of timing channels. : PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 巻 Part F128414. Association for Computing Machinery. 2017. p. 362-375 https://doi.org/10.1145/3062341.3062378
Antonopoulos, Timos ; Gazzillo, Paul ; Hicks, Michael ; Koskinen, Eric ; Terauchi, Tachio ; Wei, Shiyi. / Decomposition instead of self-composition for proving the absence of timing channels. PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 巻 Part F128414 Association for Computing Machinery, 2017. pp. 362-375
@inproceedings{d4981b167c444ba0b7319b5f4c929e00,
title = "Decomposition instead of self-composition for proving the absence of timing channels",
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).",
keywords = "Blazer, Decomposition, Subtrails, Timing attacks, Verification",
author = "Timos Antonopoulos and Paul Gazzillo and Michael Hicks and Eric Koskinen and Tachio Terauchi and Shiyi Wei",
year = "2017",
month = "6",
day = "14",
doi = "10.1145/3062341.3062378",
language = "English",
volume = "Part F128414",
pages = "362--375",
booktitle = "PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation",
publisher = "Association for Computing Machinery",

}

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

VL - Part F128414

SP - 362

EP - 375

BT - PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation

PB - Association for Computing Machinery

ER -