{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T11:01:58Z","timestamp":1777806118816,"version":"3.51.4"},"reference-count":51,"publisher":"SAGE Publications","issue":"6","license":[{"start":{"date-parts":[[2020,11,10]],"date-time":"2020-11-10T00:00:00Z","timestamp":1604966400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2020,11,27]]},"abstract":"<jats:p>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\u2019s 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. It is interesting to note that our results make non-trivial (and somewhat unconventional) uses of ideas from information flow research such as channel capacity and refinement order relation.<\/jats:p>","DOI":"10.3233\/jcs-191356","type":"journal-article","created":{"date-parts":[[2020,11,10]],"date-time":"2020-11-10T15:43:25Z","timestamp":1605023005000},"page":"607-634","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":0,"title":["Bucketing and information flow analysis for provable timing attack mitigation"],"prefix":"10.1177","volume":"28","author":[{"given":"Tachio","family":"Terauchi","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, Waseda University, Tokyo, Japan. E-mail:\u00a0"}]},{"given":"Timos","family":"Antonopoulos","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Yale University, New Haven, CT, U.S.A.. E-mail:\u00a0"}]}],"member":"179","published-online":{"date-parts":[[2020,11,10]]},"reference":[{"key":"ref001","doi-asserted-by":"crossref","unstructured":"J.\u00a0Agat, Transforming out timing leaks, in: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2000), ACM, 2000, pp.\u00a040\u201353.","DOI":"10.1145\/325694.325702"},{"key":"ref002","first-page":"21:1","volume":"1","author":"Aguirre A.","year":"2017","journal-title":"PACMPL"},{"key":"ref003","unstructured":"J.B.\u00a0Almeida, M.\u00a0Barbosa, G.\u00a0Barthe, F.\u00a0Dupressoir and M.\u00a0Emmi, Verifying constant-time implementations, in: USENIX Security Symposium, 2016, pp.\u00a053\u201370."},{"key":"ref004","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.10.008"},{"key":"ref005","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.26"},{"key":"ref006","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062378"},{"key":"ref007","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00022"},{"key":"ref008","doi-asserted-by":"crossref","unstructured":"A.\u00a0Askarov, D.\u00a0Zhang and A.C.\u00a0Myers, Predictive black-box mitigation of timing channels, in: Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS 2010), ACM, 2010, pp.\u00a0297\u2013307.","DOI":"10.1145\/1866307.1866341"},{"key":"ref009","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.18"},{"key":"ref010","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"ref011","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00031"},{"key":"ref012","doi-asserted-by":"crossref","unstructured":"N.\u00a0Benton, Simple relational correctness proofs for static analyses and program transformations, in: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), ACM, 2004, pp.\u00a014\u201325.","DOI":"10.1145\/964001.964003"},{"key":"ref013","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54455-6_13"},{"key":"ref014","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(4:5)2015"},{"key":"ref015","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"ref016","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99828-2_23"},{"key":"ref017","unstructured":"DARPA Space\/Time Analysis for Cybersecurity (STAC) program, 2017."},{"key":"ref018","doi-asserted-by":"publisher","DOI":"10.1145\/2756550"},{"key":"ref019","doi-asserted-by":"crossref","unstructured":"M.\u00a0Eilers, P.\u00a0M\u00fcller and S.\u00a0Hitz, Modular product programs, in: Proceedings of the 27th European Symposium on Programming (ESOP 2018), Lecture Notes in Computer Science, Vol.\u00a010801, Springer, 2018, pp.\u00a0502\u2013529.","DOI":"10.1007\/978-3-319-89884-1_18"},{"key":"ref020","doi-asserted-by":"crossref","unstructured":"H.\u00a0Eldib and C.\u00a0Wang, Synthesis of masking countermeasures against side channel attacks, in: Proceedings of the 28th International Conference on Computer Aided Verification (CAV 2014), Lecture Notes in Computer Science, Vol.\u00a08559, Springer, 2014, pp.\u00a0114\u2013130.","DOI":"10.1007\/978-3-319-08867-9_8"},{"key":"ref021","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44709-1_21"},{"issue":"2","key":"ref022","first-page":"1","volume":"6","author":"Gay R.","year":"2015","journal-title":"IJSSE"},{"key":"ref023","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"ref024","doi-asserted-by":"crossref","unstructured":"D.\u00a0Hedin and D.\u00a0Sands, Timing aware information flow security for a JavaCard-like bytecode, in: Proceedings of the 1st Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTE 2005), Electronic Notes in Theoretical Computer Science, Vol.\u00a0141, Elsevier, 2005, pp.\u00a0163\u2013182.","DOI":"10.1016\/j.entcs.2005.02.031"},{"key":"ref025","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45146-4_27"},{"key":"ref026","unstructured":"N.\u00a0Kobayashi and K.\u00a0Shirane, Type-based information analysis for low-level languages, in: Proceedings of the 3rd Asian Workshop on Programming Languages and Systems (APLAS 2002), 2002, pp.\u00a0302\u2013316."},{"key":"ref027","doi-asserted-by":"crossref","unstructured":"P.C.\u00a0Kocher, Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems, in: Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology (CRYPTO 1996), Lecture Notes in Computer Science, Vol.\u00a01109, Springer, 1996, pp.\u00a0104\u2013113.","DOI":"10.1007\/3-540-68697-5_9"},{"key":"ref028","doi-asserted-by":"crossref","unstructured":"P.C.\u00a0Kocher, J.\u00a0Jaffe and B.\u00a0Jun, Differential power analysis, in: Proceedings of the 19th Annual International Cryptology Conference on Advances in Cryptology (CRYPTO 1999), Lecture Notes in Computer Science, Vol.\u00a01666, Springer, 1999, pp.\u00a0388\u2013397.","DOI":"10.1007\/3-540-48405-1_25"},{"key":"ref029","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0397"},{"key":"ref030","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.21"},{"key":"ref031","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.11"},{"key":"ref032","doi-asserted-by":"crossref","unstructured":"P.\u00a0Malacaria, Assessing security threats of looping constructs, in: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), ACM, 2007, pp.\u00a0225\u2013235.","DOI":"10.1145\/1190216.1190251"},{"key":"ref033","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000649"},{"key":"ref034","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_5"},{"key":"ref035","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.34"},{"key":"ref036","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45418-7_17"},{"key":"ref037","unstructured":"J.C.\u00a0Reynolds, The Craft of Programming, Prentice Hall International Series in Computer Science, Prentice Hall, 1981."},{"key":"ref038","doi-asserted-by":"crossref","unstructured":"A.\u00a0Sabelfeld and A.C.\u00a0Myers, A model for delimited information release, in: Proceedings of the Software Security \u2013 Theories and Systems, Second Mext-NSF-JSPS International Symposium (ISSS 2003), Lecture Notes in Computer Science, Vol.\u00a03233, Springer, 2003, pp.\u00a0174\u2013191.","DOI":"10.1007\/978-3-540-37621-7_9"},{"key":"ref039","doi-asserted-by":"crossref","unstructured":"G.\u00a0Smith, On the foundations of quantitative information flow, in: Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS 2009), Lecture Notes in Computer Science, Vol.\u00a05504, Springer, 2009, pp.\u00a0288\u2013302.","DOI":"10.1007\/978-3-642-00596-1_21"},{"key":"ref040","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"ref041","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12459-4_9"},{"key":"ref042","doi-asserted-by":"crossref","unstructured":"T.\u00a0Terauchi and A.\u00a0Aiken, Secure information flow as a safety problem, in: Proceedings of the 12th International Symposium (SAS 2005), Lecture Notes in Computer Science, Vol.\u00a03672, Springer, 2005, pp.\u00a0352\u2013367.","DOI":"10.1007\/11547662_24"},{"key":"ref043","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17138-4_2"},{"key":"ref044","unstructured":"T.\u00a0Terauchi and T.\u00a0Antonopoulos, A formal analysis of timing channel security via bucketing, http:\/\/www.f.waseda.jp\/terauchi."},{"key":"ref045","doi-asserted-by":"crossref","unstructured":"S.\u00a0Tizpaz-Niari, P.\u00a0Cern\u00fd and A.\u00a0Trivedi, Quantitative mitigation of timing side channels, in: Proceedings of the 31st International Conference on Computer Aided Verification (CAV 2019), 2019, pp.\u00a0140\u2013160.","DOI":"10.1007\/978-3-030-25540-4_8"},{"key":"ref046","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-009-9049-y"},{"key":"ref047","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"ref048","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.9"},{"key":"ref049","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2011-0437"},{"key":"ref050","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2013.07.031"},{"key":"ref051","doi-asserted-by":"crossref","unstructured":"D.\u00a0Zhang, A.\u00a0Askarov and A.C.\u00a0Myers, Language-based control and mitigation of timing channels, in: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2012), ACM, 2012, pp.\u00a099\u2013110.","DOI":"10.1145\/2254064.2254078"}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-191356","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-191356","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-191356","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:24Z","timestamp":1777495524000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-191356"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,10]]},"references-count":51,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,11,27]]}},"alternative-id":["10.3233\/JCS-191356"],"URL":"https:\/\/doi.org\/10.3233\/jcs-191356","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,10]]}}}