[cap-talk] T.120-like apps

[David Wagner]

Marc Stiegler:
>Joe-E is the 100% pure Java subset that is capability secure. It uses
>the Elib for communication. A big part that is not yet complete is the
>verifier that will confirm that a class does not use any authorities it
>does not receive as explicit messages, i.e., the verifier will verify
>that a class follows the rules laid by in E by the safej files (which
>specify which methods are suppressed, and which classes are considered
>unsafe, for capability discipline). Of course, static class mutables are
>also rejected by the verifier, as another example of verifier behavior.
>
>Joe-E programs will have approximately all the promise-pipelined
>object-capability properties of E [...]
>
>Anyway, David Wagner has a small project planned to carry that work to
>completion.

Right.  For the onlookers, a warning: Joe-E doesn't exist yet, and
I don't have anything to talk about just yet.  Sorry for the vaporware.

A little more background, for the curious.  My big goal is to define
a subset of Java that is well-suited for capability programming.
Our first task will be to identify a safe and reasonable subset of Java
(this is not totally trivial), and implement a verifier to reject code
that steps outside this subset.  The next task is to safely make some
class libraries available to such code.  This could take some time.

To let people know where we're going, we're focused mainly on standalone
systems right now.  We may leave the distributed systems / cross-host
communication stuff (e.g., promises), as well as the integration with
E (e.g., Elib) to someone else, or at the very least, to a later day.
You've got to start somewhere, and it's going to be a big task just to
get to something that works well on a single host.

We hope to have a spec for the language subset available to pass around
sometime in the next few months, and we'd very much welcome comments at
that time (or advice before then).

>For example Joe-E programs will probably be
>allowed to use integers, not just BigIntegers; the plan the last time I
>was involved was, you could check and reject integers with a lintlike
>tool, but it would not be a part of the core verifier).

Yup.  I think there is a lot of potential here for lint-like tools
to check for unsafe programming styles, potential violations of
capability discipline, etc., and we've got a bunch of ideas.  I'm
very interested in this.  But we'll work on the language subset first.

>Since it is pure
>Java (or Java with SWT, which is what Eclipse was designed for, and
>which has been tamed in the safej files along with Java), IDEs for Java
>should just work fine for JoeE.

Right.  This is an important design goal, and one of the arguments for
using a strict language subset rather than a re-design of Java.