| Rather than reply individually to the messages from this thread, I'm
going to try to clarify some things here. I think a lot of good points
were brought up both with regards to the "taint" mechanism and timing
covert channels. IFC/tainting mechanism: The style of IFC we are proposing is not not the tainting style used
by more typical language-level systems. In particular, we're proposing
a mostly-coarse grained system: - A single label is associated with a context. A context can be the
main extension context or, more likely, a light-weight worker the
main extension context created. This single label is conceptually
the label on everything in scope. As such, when performing some I/O
this label is used by the IFC mechanism to check if the code is
allowed to perform the read/write. This coarse-grained approach
alleviates the need to keep track of tricky leaks due to control
flow: the branch condition has the label of the context so any
control flow within the context is safe. If you want to perform a
public computation after a secret computation, you need to
structure your program into multiple contexts (e.g. create a new
worker wherein you intend to perform the secret computation). - Labels can also be associated with values. A new constructor Labeled
is provided for this task. You can think of it as a boxing the value
and, by default, only allowing you to inspect the label of the
value. You can pass such labeled values around as you see fit (and
this is pretty useful in real applications). Importantly, however,
when you read the underlying (protected) value the IFC system taints
your context---i.e., it raises the context label to let you read the
value, but also restricts your code from writing to arbitrary
end-points since doing so may leak something about the newly-read
value. An important requirement of this IFC approach is that there be no
unlabeled (implicit) shared state between the different contexts. For
example, rand() in context A and B must not share an underlying
generator. This kind of isolation can be achieved in practice and is
an important detail when considering covert channels. Timing channels: It turns out that if you do IFC in this coarse-grained fashion you can
prevent leaks due to timing covert channels, if you are willing/able
to schedule contexts using a "secure scheduler." In [1] we showed how
to eliminate timing attacks of the style described in this thread
(internal timing channels) that are inherent to the more typical IFC
systems. In [2] we extended the system to deal with timing attacks due
to the CPU cache by using an instruction-based scheduler (IBS). IBS
and other techniques to deal with timing channels are nicely
described in [3]. (I'd be happy to expand here, but this is already a
long reply.) [1] http://www.scs.stanford.edu/~deian/pubs/stefan:2012:addressi...
[2] http://www.scs.stanford.edu/~deian/pubs/stefan:2013:eliminat...
[3] https://ssrg.nicta.com.au/projects/TS/timingchannels.pml |