Timed Abstract Non-Interference

By: Roberto Giacobazzi and Isabella Mastroeni

Roberto Giacobazzi
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
roberto.giacobazzi@univr.it

Isabella Mastroeni
Dept. of Computing and Information Sciences
KSU
234 Nichols Hall
Manhattan, KS 66506 (USA)
isabellm@cis.ksu.edu

Abstract:

In this paper, we introduce a timed notion of abstract non-interference. This is obtained by considering semantics which observe time elapsed in computations. Timing channels can be modeled in this way either by letting the attacker to observe time as a public variable or reckon the time elapsed by observing the computational traces' length, corresponding to observe the program counter. In the first case abstract non-interference provides a model for abstracting the information about time, namely we can for example consider models of attackers that can observe only intervals of time, or other more abstract properties. In the second case abstract non-interference provides a model for attackers able to observe properties of trace length, e.g., the public memory during the whole computation. We investigate when adding the observation of time does not increase the attacker's power in disclosing confidential information about data. This models the absence of timing channels in language-based security.
Related papers:
  • Adjoining Declassification and Attack Models by Abstract Interpretation (2004)
  • Modeling Information Flow Dependencies with Boolean Functions (WITS'04,2004)
  • Abstract Non-Interference - Parameterizing non-interference by Abstract Interpretation (POPL'04,2004)
  • Proving Abstract Non-Interference (CSL, 2004)

  • isabellm@cis.ksu.edu