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

[Mark Miller]

On Sat, Apr 5, 2008 at 6:15 AM, Pierre THIERRY
<nowhere.man at levallois.eu.org> wrote:
> Scribit Raoul Duke dies 04/04/2008 hora 22:08:
>
> > I'm guessing that there will be at least one or two tricky bugs or
>  > thinkos in any security system
>
>  That's why you need to think about security from the ground up. You
>  can't easily retrofit security on a huge system without risking to
>  forget to plug some holes.
>
>  This is one of the interesting features of a pure ocaps system, that you
>  only have to check two things:
>
>  - you implemented the ocaps [model] carefully,
>  - you adhere to capability discipline in the components you build on top
>   of it.
>
>  Theroetically,


As I read this thread, I worry that we may drown by filling the boat
with our own kool-aid. Let's please not get overconfident. Pierre's
"Theoretically" above needs to be taken much more seriously than this
thread seems to. Even using object-capabilities well, we still don't
know how to achieve security reliably and with confidence. I have
participated in two security reviews of object-capability systems: On
the DarpaBrowser (Wagner & Tribble attack MarkM & MarcS), and Waterken
(Wagner, Adrian, Tribble, MarcS, MarkM attack Tyler).

In both cases the attackers won. From these experiences, two things are clear
* We do not yet know how to build systems we can know are secure
* Capabilities help the situation tremendously, but not enough

I have also participated in the review of PVote (Wagner & Ping attack
a variety of security luminaries including Ian Goldberg, Matt Bishop,
Dan Wallach, as well as MarkM). This system is much simpler than a
capability system, with much less code (about 450 lines), with much
simpler claims, but with a much harder threat model which inverted the
normal roles: The attackers maliciously inserted bugs into PVote and
the defenders were the reviewers responsible for finding these bugs.
The attackers still won. In this case, no one found a bug in PVote
itself, but several of the maliciously inserted bugs went undetected
as well.

So PVote may well be secure, but our failure to find maliciously
inserted bugs means we should question our ability to know it is
secure.

The other interesting data point is the KeyKOS line of operating
systems. The KeyKOS kernel may very well be the most robustly secure
general purpose operating system kernel to be deployed commercially.
(I would be interested to see if anyone can offer counter-examples.)
However, Eric Northup did find a minor security bug in the KeyKOS
kernel design many years later. Shap and Charlie are of course working
towards even more carefully constructed successors, with Shap hoping
for a machine-checked proof of the Coyotos kernel implementation.

Even if Shap succeeds, this high level of confidence will apply only
to the kernel and perhaps a small amount of non-kernel TCB code. The
cost of achieving this level of confidence is soooo high per line of
code as to be unaffordable for normal application code. 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.


Bottom line: Capabilities today can make a system's security much more
robust against its own bugs. (Part 4 of my thesis, "Emergent
Robustness", explains what I mean in more depth.) But beyond this, we
should avoid making stronger claims, or sounding like we're making
stronger claims.


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

 Cheers,
 --MarkM