[cap-talk] Forgeable capabilities

[Toby Murray]

Here's how I can  do it in CSP.  (You might refer to "Authority
Analysis ..." paper for some background if you're  interested

http://web.comlab.ox.ac.uk/oucl/work/toby.murray/papers/AALPE.pdf


S(t) = getAuthority?login?password ->
  if login == X and password == Y then
     return!t -> S(t)
  else
     return!null -> S(t)

Alice(login,password) = getAuthority.login.password -> return?cap ->
Alice(login,password)


Now if we instantiate Alice as Alice(X,Y) and then check whether Alice
can ever acquire t (using a safety analysis check) then we'd find she
could.

If we instantiate Alice otherwise (i.e. she doesn't know X and Y) she
won't be able to acquire such permissions.

This doesn't even require an authority analysis -- it's just an
acquirable permission analysis. 

Many traditional frameworks have trouble reasoning about knowledge. But
some are more expressible than others. Hopefully the above indicates
that CSP is such an expressive framework that reasoning about this sort
of thing is indeed possible and simple.


On Sat, 2007-07-07 at 10:34 -0700, David Wagner wrote:
> Pierre writes:
> >I was wondering how forgeable capabilities are modeled in
> >object-capabilities frameworks.
> 
> If it's forgeable, it's not a capability.
> 
> For the rest of the message I'm going to assume you wrote
> "authentication tokens" instead of "forgeable capabilities".
> 
> >For example, if I have an object S that has a grantAuthority(credential)
> >method, where credential is a couple (login, password), this couple
> >constitutes [an authentication token].  If a call to grantAuthority
> >with the adequate credential returns a capability to an object T, is it
> >possible to model authority to S in another way than considering that
> >authority to call S->grantAuthority is equivalent to authority to call
> >T? That is, to model authority to S less conservatively.
> 
> Reasoning about this requires reasoning about both behavior and
> knowledge.  You have to reason about (a) the behavior of
> grantAuthority() (i.e., under what conditions will it return the
> cap to T?), and (b) the knowledge available to all parties in the
> system (i.e., under what circumstances can they come to know or
> guess the authentication token?).  In general, reasoning about
> knowledge is very difficult, and my experience is that object
> capabilities don't help much with that task.
> 
> You could look at information flow systems for some attempts to
> reason about knowledge, though in my opinion I'd call them closer
> to failed attempts rather than successful attempts.
> 
> For this reason, my advice is to try to avoid structuring your system in
> a way that demonstrating its security requires doing a lot of reasoning
> about knowledge.  Firewall or segregate off the knowledge-based stuff
> (e.g., crypto, password checking, etc.) into its own little island so
> that it is as encapsulated as possible and so that you can reason about
> as much as possible of the rest of your application without needing to
> reason about knowledge.  That will maximize the effectiveness of the
> object capability approach to reasoning about security.
> 
> Finally, I'll point out that cleartext passwords have many known problems
> and one should think carefully about using them in new systems for
> authentication, especially if it is a distributed system.
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk