[cap-talk] - Bellizzomi - Capabilities and Shapiro's focus, Coyotos, etc.
Jed at Webstart
donnelley1 at webstart.com
Wed Nov 29 11:30:24 CST 2006
At 08:41 AM 11/29/2006, Mark S. Miller wrote:
>Karp, Alan H wrote:
> > While you can't prevent wall banging, you can prevent wall listening by
> > removing all forms of indeterminacy, such as access to the system clock.
> > Any process that is deterministically replayable meets this criterion.
> > Did I get that right, MarkM?
"prevent" is a strong word. Let's see how this works.
>In addition, once such processes are deafened, this can contribute towards
>alleviating wall banging in an indirect and imperfect way:
>The main wall banging channel is variable resource use.
That's my understanding.
>The main defense
>against such wall banging is preallocation of worst-case resources, and then
>wasting the slack -- the difference between actual and worst-case resource
>needs. Since typical resource needs can often be orders of magnitude
>worst case, this waste can be quite costly.
Agreed. Seems any effort to prevent "wall banging" (watching for shared
uses of resources such as CPU, disk, network, printer, etc., etc.) must
necessarily be quite wasteful. What it must amount to in my opinion is
essentially not doing sharing. One can of course set this up. Give
a program that you want to isolate it's own unshared resources. That
seems to me about the best you can do.
>However, if one has a bunch of deafened processes that could do useful batch
>work, one can run these in the slack.
Sorry, but I didn't catch what you meant by "deafened"?
>As deafened processes, they can't sense
>how much slack they're getting, or how this slack is spread over real time.
>By "batch" above, the key feature is that no one needs an answer from these
>promptly, so these answers can be delayed and aggregated. Revealing which
>answers are available at some future time does reveal some covert info, but
>hey, I said it was imperfect.
There you go - imperfect and to me such effort is not particularly well spent.
I've not seen any "proof"s in this area (covert channels). I quote
generally to me the source for a program is a proof that the program
will do what it
says it will do. Any effort at program proving amounts to trying to
an equivalence between a program written in one language with some other
language statement - typically a simpler one. Unfortunately, the simpler
statement often must leave out details that later prove to be relevant though
they have disappeared even from the model of the higher level language.
Once you've seen one "proof" to show that some software is, let's say,
'secure' and then find that the software isn't secure it puts the whole process
into question. Not to say it can't be a useful exercise, e.g. for
where learning can occur. Just to say that the emphasis on "proof", as if
the certainty of Mathematics could be applied to engineering, seems
often misplaced and a bit exaggerated to me.
More information about the cap-talk