Re: Mechanics of enhancing Java taming database?

Andy Fingerhut  wrote:
> If one wished to help enhance the Joe-E SafeJ database, what would the
> recommended mechanics be?  That is, should I check out the Subversion
> repository for Joe-E, edit one or more .safej files in the safej
> directory, make a diff/patch, and email it to this email list?  Or would
> some other method be preferable?

Yes, that would be wonderful.  I'd certainly be interested to see what
you come up with.

I would request that you make your patches available under the New BSD
license (the same license used for the rest of Joe-E).  Also, it would
be great if you could add comments to the safej files justifying the
taming decisions or explaining them in a way useful to users.  This will
help us review your patches; we'll probably want to try to find someone
to review any patches you come up with, before we commit them to the
Joe_E distribution.

See the Taming wiki page that Adrian pointed to for detailed information
on taming in Joe-E.

> Is this same SafeJ taming database also used for taming the Java library
> for other E variants, such as E-on-Java?  For creating the documentation
> at http://erights.org/javadoc/index.html ?

No, it is not the same taming database.  We use the same conceptual
approach and a very similar file format, but we built a new taming
database from scratch.  (I can't remember the details for sure, but I
think the file format is not exactly identical, for various reasons.)

Why didn't we just copy E's taming database over to Joe-E?  The
main reason was for increased assurance.  We thought we might get
higher assurance if we started from scratch, and made all our own
taming decisions, rather than just copying over E's taming database.
For more discussion, see e.g.,
  http://www.eros-os.org/pipermail/e-lang/2008-November/012938.html
This was based in part upon some experience with E's taming database
that left us concerned about the security risks of adopting E's
taming database wholesale
  http://www.combex.com/papers/darpa-review/security-review.html#taming
and in part based upon Mark Miller's urging.  The tradeoff is that,
as a result, Joe-E's taming database is far more limited.  Joe-E is
a research project, and we just don't have the software engineering
resources to do a good job of taming a large fraction of the Java
libraries.  We could have an interesting discussion about whether
that was the right design decision, but for better or worse, it was
the path we followed.

You might also find this thread on E vs Joe-E taming of interest:
  http://www.eros-os.org/pipermail/e-lang/2008-November/thread.html#12940

We used a separate tool for generating API documentation, namely,
the Joe-E Doc tool.  The Joe-E Doc tool is available here:
  https://code.google.com/p/joe-e-doc/ 
and the API documentation, annotated with taming decisions, is
available here:
  http://www.cs.berkeley.edu/~daw/joe-e/api/ 
I've updated the Taming page on the Joe-E wiki with all of these
links and information.