[cap-talk] Avoid overconfidence (was: Any hope in RSA 2008?)

[Jed Donnelley]

At 10:31 AM 4/5/2008, Toby Murray wrote:
>On Sat, 2008-04-05 at 08:00 -0700, Mark Miller wrote:
> > I remain
> > hopeful that further work on formal tools, like Fred's SCOLL and
> > Toby's Authodox, may bring these costs down much farther. But I also
> > remain skeptical. Formal tools for assuring program correctness have
> > been three weeks away for the last forty years.
>
>Just like the widespread deployment of capability-based systems that
>solve real world problems ;)
>
>(No this isn't a flame. I'm a strong believer in the virtues of both
>formal methods and capabilities. It's just ironic. I hope to see both
>"arrive".)
>
>I'm pretty sure Peter Neumann of PSOS fame (one of the first efforts to
>build a formally verified capability-based OS) has somewhere paraphrased
>the "capabilities are the way of the future and always will be" as
>"formal methods are the way of the future and always will be", in order
>to note that both are promising technologies that have yet to properly
>deliver.

Previously on this list the above statement was attributed to Butler
Lampson.  In fact Peter Neumann attributes it to Butler via David
Redell, e.g. in his:

"PSOS Revisited": http://www.csl.sri.com/users/neumann/psos03.pdf

"According to David Redell, Butler Lampson is credited
with saying somewhen in the 1970s that "Capability sys-
tems are the way of the future, and always will be." There
seems to be considerable truth in that statement, although
for reasons that may have little to do with the technical
merits of capabilities."

I wasn't able to find a direct quote from Butler on this
topic, though I previously noted a direct quote from him
to the effect that POLP is counter productive:

Lampson:
"I think, for example, that the Principle Of Least Privilege has done an
enormous amount of damage to security because what it encourages
you to do is to make everything fine grain and work out all the
dependencies very carefully and it's too complicated.  You can't keep
track of it.  You're bound to mess it up.  Even if you get it right today
it will be wrong three months from now.  Nobody will have the patience
to ever look at it again because there's just too much of it.  So I say
absolutely no to fine grain protection.  Everything should be as course
grain as possible because otherwise you won't be able to administer it.
That's a very unpopular position with most people.  I think there's a lot
of empirical evidence that tells us now that it's right."

As I recall the above came from his keynote address:

http://www.usenix.org/events/sec05/tech/

though I didn't take time to listen through it again.

The abstract for that talk suggests that Lampson knows
why computer security hasn't progressed significantly:
__________
After thirty years of work on computer security, why are almost all 
the systems in service today extremely vulnerable to attack? The main 
reason is that security is expensive to set up and a nuisance to run, 
so people judge from experience how little of it they can get away 
with. Since there's been little damage, people decide that they don't 
need much security. In addition, setting it up is so complicated that 
it's hardly ever done right. While we await a catastrophe, simpler 
setup is the most important step toward better security. In a 
distributed system with no central management like the Internet, 
security requires a clear story about who is trusted for each step in 
establishing it, and why. The basic tool for telling this story is 
the "speaks for" relation between principals that describes how 
authority is delegated, that is, who trusts whom. The idea is simple, 
and it explains what's going on in any system I know, although the 
many different ways of encoding this relation often make it hard to 
see the underlying order.
___________

though you can make your own judgement if you listen to it.

--Jed  http://www.webstart.com/jed-signature.html