A Formal Analysis of Timing Channel Security via Bucketing

Tachio Terauchi, Timos Antonopoulos

研究成果: Conference contribution

抄録

This paper investigates the effect of bucketing in security against timing channel attacks. Bucketing is a technique proposed to mitigate timing-channel attacks by restricting a system’s outputs to only occur at designated time intervals, and has the effect of reducing the possible timing-channel observations to a small number of possibilities. However, there is little formal analysis on when and to what degree bucketing is effective against timing-channel attacks. In this paper, we show that bucketing is in general insufficient to ensure security. Then, we present two conditions that can be used to ensure security of systems against adaptive timing channel attacks. The first is a general condition that ensures that the security of a system decreases only by a limited degree by allowing timing-channel observations, whereas the second condition ensures that the system would satisfy the first condition when bucketing is applied and hence becomes secure against timing-channel attacks. A main benefit of the conditions is that they allow separation of concerns whereby the security of the regular channel can be proven independently of concerns of side-channel information leakage, and certain conditions are placed on the side channel to guarantee the security of the whole system. Further, we show that the bucketing technique can be applied compositionally in conjunction with the constant-time-implementation technique to increase their applicability. While we instantiate our contributions to timing channel and bucketing, many of the results are actually quite general and are applicable to any side channels and techniques that reduce the number of possible observations on the channel.

元の言語English
ホスト出版物のタイトルPrinciples of Security and Trust - 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
編集者Flemming Nielson, David Sands
出版者Springer-Verlag
ページ29-50
ページ数22
ISBN(印刷物)9783030171377
DOI
出版物ステータスPublished - 2019 1 1
イベント8th International Conference on Principles of Security and Trust, POST 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, Czech Republic
継続期間: 2019 4 62019 4 11

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
11426 LNCS
ISSN(印刷物)0302-9743
ISSN(電子版)1611-3349

Conference

Conference8th International Conference on Principles of Security and Trust, POST 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019
Czech Republic
Prague
期間19/4/619/4/11

Fingerprint

Formal Analysis
Adaptive systems
Timing
Attack
Time Constant
Leakage
Decrease
Interval
Output

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

これを引用

Terauchi, T., & Antonopoulos, T. (2019). A Formal Analysis of Timing Channel Security via Bucketing. : F. Nielson, & D. Sands (版), Principles of Security and Trust - 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (pp. 29-50). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 11426 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-030-17138-4_2

A Formal Analysis of Timing Channel Security via Bucketing. / Terauchi, Tachio; Antonopoulos, Timos.

Principles of Security and Trust - 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. 版 / Flemming Nielson; David Sands. Springer-Verlag, 2019. p. 29-50 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻 11426 LNCS).

研究成果: Conference contribution

Terauchi, T & Antonopoulos, T 2019, A Formal Analysis of Timing Channel Security via Bucketing. : F Nielson & D Sands (版), Principles of Security and Trust - 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 巻. 11426 LNCS, Springer-Verlag, pp. 29-50, 8th International Conference on Principles of Security and Trust, POST 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, 19/4/6. https://doi.org/10.1007/978-3-030-17138-4_2
Terauchi T, Antonopoulos T. A Formal Analysis of Timing Channel Security via Bucketing. : Nielson F, Sands D, 編集者, Principles of Security and Trust - 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Springer-Verlag. 2019. p. 29-50. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-17138-4_2
Terauchi, Tachio ; Antonopoulos, Timos. / A Formal Analysis of Timing Channel Security via Bucketing. Principles of Security and Trust - 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. 編集者 / Flemming Nielson ; David Sands. Springer-Verlag, 2019. pp. 29-50 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{679a138d30f9489b81ae2a26f9677d8e,
title = "A Formal Analysis of Timing Channel Security via Bucketing",
abstract = "This paper investigates the effect of bucketing in security against timing channel attacks. Bucketing is a technique proposed to mitigate timing-channel attacks by restricting a system’s outputs to only occur at designated time intervals, and has the effect of reducing the possible timing-channel observations to a small number of possibilities. However, there is little formal analysis on when and to what degree bucketing is effective against timing-channel attacks. In this paper, we show that bucketing is in general insufficient to ensure security. Then, we present two conditions that can be used to ensure security of systems against adaptive timing channel attacks. The first is a general condition that ensures that the security of a system decreases only by a limited degree by allowing timing-channel observations, whereas the second condition ensures that the system would satisfy the first condition when bucketing is applied and hence becomes secure against timing-channel attacks. A main benefit of the conditions is that they allow separation of concerns whereby the security of the regular channel can be proven independently of concerns of side-channel information leakage, and certain conditions are placed on the side channel to guarantee the security of the whole system. Further, we show that the bucketing technique can be applied compositionally in conjunction with the constant-time-implementation technique to increase their applicability. While we instantiate our contributions to timing channel and bucketing, many of the results are actually quite general and are applicable to any side channels and techniques that reduce the number of possible observations on the channel.",
author = "Tachio Terauchi and Timos Antonopoulos",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-17138-4_2",
language = "English",
isbn = "9783030171377",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "29--50",
editor = "Flemming Nielson and David Sands",
booktitle = "Principles of Security and Trust - 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings",

}

TY - GEN

T1 - A Formal Analysis of Timing Channel Security via Bucketing

AU - Terauchi, Tachio

AU - Antonopoulos, Timos

PY - 2019/1/1

Y1 - 2019/1/1

N2 - This paper investigates the effect of bucketing in security against timing channel attacks. Bucketing is a technique proposed to mitigate timing-channel attacks by restricting a system’s outputs to only occur at designated time intervals, and has the effect of reducing the possible timing-channel observations to a small number of possibilities. However, there is little formal analysis on when and to what degree bucketing is effective against timing-channel attacks. In this paper, we show that bucketing is in general insufficient to ensure security. Then, we present two conditions that can be used to ensure security of systems against adaptive timing channel attacks. The first is a general condition that ensures that the security of a system decreases only by a limited degree by allowing timing-channel observations, whereas the second condition ensures that the system would satisfy the first condition when bucketing is applied and hence becomes secure against timing-channel attacks. A main benefit of the conditions is that they allow separation of concerns whereby the security of the regular channel can be proven independently of concerns of side-channel information leakage, and certain conditions are placed on the side channel to guarantee the security of the whole system. Further, we show that the bucketing technique can be applied compositionally in conjunction with the constant-time-implementation technique to increase their applicability. While we instantiate our contributions to timing channel and bucketing, many of the results are actually quite general and are applicable to any side channels and techniques that reduce the number of possible observations on the channel.

AB - This paper investigates the effect of bucketing in security against timing channel attacks. Bucketing is a technique proposed to mitigate timing-channel attacks by restricting a system’s outputs to only occur at designated time intervals, and has the effect of reducing the possible timing-channel observations to a small number of possibilities. However, there is little formal analysis on when and to what degree bucketing is effective against timing-channel attacks. In this paper, we show that bucketing is in general insufficient to ensure security. Then, we present two conditions that can be used to ensure security of systems against adaptive timing channel attacks. The first is a general condition that ensures that the security of a system decreases only by a limited degree by allowing timing-channel observations, whereas the second condition ensures that the system would satisfy the first condition when bucketing is applied and hence becomes secure against timing-channel attacks. A main benefit of the conditions is that they allow separation of concerns whereby the security of the regular channel can be proven independently of concerns of side-channel information leakage, and certain conditions are placed on the side channel to guarantee the security of the whole system. Further, we show that the bucketing technique can be applied compositionally in conjunction with the constant-time-implementation technique to increase their applicability. While we instantiate our contributions to timing channel and bucketing, many of the results are actually quite general and are applicable to any side channels and techniques that reduce the number of possible observations on the channel.

UR - http://www.scopus.com/inward/record.url?scp=85064920904&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85064920904&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-17138-4_2

DO - 10.1007/978-3-030-17138-4_2

M3 - Conference contribution

SN - 9783030171377

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 29

EP - 50

BT - Principles of Security and Trust - 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings

A2 - Nielson, Flemming

A2 - Sands, David

PB - Springer-Verlag

ER -