[cap-talk] Re: Question on web calculus

[Tyler Close]

On 2/7/06, Olivier Lefevre <lefevrol at yahoo.com> wrote:
> > When developing a capability-based application, the developer is
> > constantly doing exactly this sort of analysis.
>
> Yes but it is a stretch to label that a "theoretical analysis". And I
> can guarantee you that most developers don't use the LC to reason about
> their programs ;-) Maybe they should but that is another story.

I said "when developing a capability-based application". Most
developers aren't doing capability-based design. I hope you aren't
going to make such an assertion about what I and others doing
capability-based design are thinking.

In the lambda-calculus, computation is only achieved through explicit
passing and invocation of functions. You can think of capability-based
security as basically just saying: "This MUST be the only way to
communicate". When analysing a capability-based application, you
assume that authority can only be passed along the reference graph and
focus your attention on where particular authorities are located in
the graph. If through analysis of a local sub-graph you determine that
the policy for accessing a particular authority is correctly
implemented, you then move on to the next authority. Since there are
no other channels for accessing the authority, you know you have
completed a full analysis. The computational model of the
lambda-calculus is crucial to enabling this workflow.

> > I built the Waterken Server toolkit to support developing
> > capability-based applications. I have built some fairly large,
> > security sensitive applications with it. [I showed] code
> > fragments to the audience that proved the software implemented
> > these guarantees.
>
> Still not a _theoretical_ analysis.

Since you did not attend the presentation, your assertion is unsupported.

Perhaps you could also clarify what you are looking for in a
"_theoretical_ analysis".

> > DARPA Browser + Joe-E
>
> These are clearly capability-based efforts but AFAIK not related to
> Waterken.

The DARPA Browser involved taming a Java API and the Joe-E project
involves checking Java code for compliance with capability programming
rules. The Waterken Server creates a network interface to server side
Java objects. The created interface effectively extends the reference
semantics across the network so that you can reason about a remote
client the same way you reason about a local client. Given this kind
of application server, the analysis that these projects apply to local
Java applications can now apply to distributed applications.

Tyler

--
The web-calculus is the union of REST and capability-based security:
http://www.waterken.com/dev/Web/

Name your trusted sites to distinguish them from phishing sites.
https://addons.mozilla.org/extensions/moreinfo.php?id=957