Organizer: Alexandra Weber, CROSSING, TU Darmstadt
Bucketing is a technique proposed to mitigate timing-channel attacks by restricting a system's outputs to only occur at designated time intervals, and thus 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 work, we formally investigate the effect of bucketing. Namely, we show the following results: (1) the insufficiency of bucketing to ensure security in general, (2) a condition, called secret-restricted side-channel refinement, that ensures that the security of a system decreases only by a limited degree by timing-channel observations, (3) a condition, called bounded low-input side-channel capacity, that ensures that the system would satisfy condition (2) when bucketing is applied and hence becomes secure against timing-channel attacks, and (4) a compositional application of condition (3) with timing channel non- interference. 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. Also, 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.
The results of this submission may be viewed at: https://intern.cysec.tu-darmstadt.de/drupal7/node/2760/submission/1167
Tachio Terauchi is a professor in the Department of Computer Science and Engineering at Waseda University. He received his M.S. and Ph.D. from University of California Berkeley in 2004 and 2006, and B.S. from Columbia University in 2000, all in computer science. Before joining Waseda, he was a professor at JAIST from 2014 to 2017, an associate professor at Nagoya University from 2011 to 2014, and an assistant professor at Tohoku University from 2007 to 2011. Terauchi is interested in techniques for building reliable computational systems. His work draws from, and contributes to the areas of programming languages, program analysis, program verification, program synthesis, type systems, mathematical logic, automated deduction, and security.
- The talk will be held online via Zoom
- Please contact Alexandra Weber (email@example.com-…) to obtain the Zoom Credentials