[cap-talk] Video of Marc Stiegler's talk at Google : "The Lazy Programmer's Guide to Secure Computing"

[Mark Miller]

On Wed, Mar 31, 2010 at 6:42 PM, Toby Murray <toby.murray at comlab.ox.ac.uk>wrote:

> 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 [1] I've adopted slightly
> different definitions of overt vs. covert information flows in
> object-capability systems.
>
> 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
> DataDiode.
>
> 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?
>

Thanks for that example; it is very clear. I would definitely say that
information is flowing overtly from high to low in that example. I purposely
avoided such an interlock in the DataDiode in my thesis for exactly this
reason.



>
> > 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 ([1]) 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 [1] 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
> inputs.
>
> Cheers
>
> Toby
>
> [1] http://web.comlab.ox.ac.uk/publications/publication3202-abstract.html
>
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk
>



-- 
Text by me above is hereby placed in the public domain

   Cheers,
   --MarkM
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20100331/6f65e5a0/attachment.html