[cap-talk] Video of Marc Stiegler's talk at Google : "The Lazy Programmer's Guide to Secure Computing"
toby.murray at comlab.ox.ac.uk
Wed Mar 31 18:42:32 PDT 2010
On 1 April 2010 11:20, David Wagner <daw at cs.berkeley.edu> wrote:
> - An *overt* communication channel is one that is guaranteed by
> the platform spec (or language spec) to work. A *covert* channel
> is one that might or might not work; if there exists at least
> one conforming implementation of the platform (or language)
> which allows information to flow across the channel, and one
> conforming implementation where no information flows, then the
> channel is *covert*. (This distinction/definition was proposed
> by Mark Miller.)
In some work on applying process-calculus information flow style
properties to object-capability patterns  I've adopted slightly
different definitions of overt vs. covert information flows in
Information flows overtly when it is passed in a message from one
object to another.
Information flows covertly when it is passed from one object to
another by some other (non-overt) means.
For most practical purposes, the two definitions tend to coincide.
However, consider the following scenario:
High and Low interact, mediated by an object DataDiode that sits
between them. DataDiode accepts "write" messages from Low, buffering
whatever data those messages contain. DataDiode accepts "read"
messages from High, in response to which DataDiode returns to High
whatever data is currently buffering and then clears its buffer.
In this way it allows Data to flow overtly from Low to High. Suppose
further that DataDiode accepts "read" messages only when its buffer is
not empty and accepts "write" message only when its buffer is empty.
Then High and signal to Low by choosing whether to "read" form
Under my definitions of covert and overt, this flow of data from High
to Low is covert. But I suspect that under yours (adopted from Mark
Miller) the flow would be considered overt. Is that right?
> In principle, some capability systems provide a way to solve the
> inward bit confinement, in some cases. Suppose we have a
> *deterministic* capability language (one where there is no ambient
> access to non-determinism). Suppose that we instantiate a component
> C, and avoid passing it any capabilities that would provide C with
> access to any sort of non-determinism (we don't pass it a capability
> to let it access a random number generator, or a clock, or the network,
> or anything else whose behavior fails to be fully deterministic).
> Then we can be confident that the behavior of C is a deterministic
> function of the inputs it was passed. As a result, it has no way
> to receive on any covert channel.
This requirement for objects to behave as a deterministic function of
their inputs (specifically a det function of the messages they have
sent and received to/from other objects in the system) is exactly the
assumption that we had to make in the paper mentioned above () in
order to talk snesibly about whether DataDiode allows unwanted (what i
would call covert) flows of data from High to Low. In particular, one
cannot talk about whether DataDiode allows data to propagate covertly
from High to Low (under my definition of covert) unless one can assume
that Low's behaviour is a deterministic function of its inputs.
In  we formalise this idea by static that a system is secure
precisely when an information flow property (such as a suitable
noninterference definition) holds for all /deterministic componentwise
refinements/ of the system, i.e. for all scenarios in which each
component in the system behaves as a deterministic function of its
More information about the cap-talk