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

[David Wagner]

Toby Murray  wrote:
>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?

That is right: I would consider those overt.

I think that in a simplified theoretical model where the only
language primitives are message sends, the two definitions might
tend to coincide.  I think that in real systems, there might be
more channels where the definitions would differ.  e.g.,

* Alice writes a value to a global variable.  Bob reads that
  global value.  I call that overt, even though the value never
  appeared in any method call (message send).

* Alice writes a value to a file.  Bob reads the file.  I call
  that overt (since the filesystem spec probably says that the
  value returned by a file-read operation is the last value
  written to the file -- or if it doesn't say that explicitly,
  everyone understands that to effectively be part of the spec
  for a filesystem), even though there is no object in the
  language that represents the state of the filesystem.

* Alice creates a file if her bit is 1, otherwise does not create
  it.  Bob tests for the existence of the file.  I call that overt
  (for similar reasons).

* Alice calls bob.set() if her bit is 1, else calls bob.clear()
  if her bit is 0.  I'd call that overt, even though her bit never
  appears in the method call parameters.

* Alice runs the following Java code

    Object o;
    do {
      o = new Object();
    } while ((o.hashCode() & 1) != alicebit);

  Alice passes o to Bob.  Bob computes o.hashCode() & 1 to
  recover Alice's bit.  I'd call that overt.

I'm not sure what you'd call these examples, but it sounds like
they might be classified as covert in your definition.  I suspect
these examples are unfair because your definition is intended to
apply to a pure system where the only allowed operation is message
sending, and where there are no libraries that provide access to
the external world (what Mark Miller's thesis calls "device drivers",
if I remember correctly), not to arbitrary languages.

>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.

Thanks for sharing the paper!

I've read many papers that prove noninterference properties of
simplified programming languages.  But in every case, their results do
not apply to widely used systems programming languages like C, Java, etc.,
typically because the papers fail to model some aspects of real languages
(e.g., threads, concurrency, exceptions, locks, timing variability,
memory allocation, resource exhaustion conditions, cache contention).
The unmodelled language constructs invariably provide many opportunities
for covert channels that are not covered by those papers.  So I've become
skeptical of that line of work, because I have yet to see an approach
that I believe will scale up to a full general-purpose programming
language while providing guarantees of the absence of covert channels.
Or to put it another way, I can imagine sophisticated static analysis
algorithms to detect some covert channels, but I can't imagine one that
would detect all possible covert channels (in a realistic language).
I don't see how object capabilities would change that conclusion.
Am I missing anything?  Am I being unfair?