[E-Lang] Java 2 "Security" (was: Re: WelcomeChrisSkalkaandScottSmith of Johns Hopkins)

David Wagner daw@mozart.cs.berkeley.edu
1 Feb 2001 05:28:16 GMT


Jonathan S. Shapiro wrote:
>Ultimately, the real problem with ACLs is neither delegation nor user
>identity. The real problem is that it has long since been formally shown
>[Ullman '74] that the ACL class of protection mechanism is broken. The
>"safety problem" is undecideable in an ACL system, from which it follows
>that the security of an ACL system cannot in general be shown.

I guess I have two questions:
  Doesn't the same result also apply to capabilities systems?
  Why should the undecidability bother me?

Note that the model of an access control system used in their paper
was agnostic about how access rights are stored.  (If they are stored
with the subject, you get a capabilities system; if stored with the
object, you get an ACL system.)  Thus, it seems to me that their
results apply equally to both capabilities and ACL systems.

In practice, whether you use a capabilities-based system or an
ACL-based system, you will modify and restrict it appropriately
until you can prove whatever theorems you want to prove.

Second, I'm not sure why undecidability should be a problem.
Undecidability says it's not possible to give a general algorithm
that statically says, for all possible systems, whether that system
is safe.  But in practice, we never need such an algorithm; we only
want (at most) to prove things about the single system we're building,
and we're willing to modify the implementation to enable us to find
proofs.

To argue that undecidability is fundamental in all security systems,
no matter how they are structured, consider this code fragment:
    [...]
    if (f())
      do something insecure
    [...]
where f() is a horrendously complicated function, and where "do
something insecure" might include broadcasting all your capabilities,
or whatever.  Deciding whether something insecure happens here is as
at least as hard as deciding whether f() terminates; since the halting
problem is undecidable, so is the "safety problem" in this setting.
In general, static analysis of any non-trivial property is undecidable
(Rice's theorem), so for every static analysis algorithm, there will be
some safe systems that you can't prove to be safe.