Re: The Joy of Java

At 6:51 PM 4/26/96, Bill Frantz wrote:
>Tim May and Mike Duvos have expresses an enthusiasm for Java which I share.
> There are a few practical issues which should be addresses.

And bear in mind that "enthusiasm" does not mean certitude. We've all
gotten enthusiastic at times about some Next Big Thing. I count this
enthusiasm as part of the larger Web picture, which is unlikely to fizzle
out.

>Tim says:
>>One interesting remark I read from someone was that the Java distribution
>>model returns us to an era of easier distribution of small programs. The
>>"application bloat" of very large programs may be at least partly fixed.
>>We'll see.
>
>I have my doubts about this one.  I think application bloat comes from
>market forces and from the kind of bundling you see in XYZCorpOffice
>products where you get 4 applications packaged together.  This marketing
>approach maximizes revenue by selling you products you don't need as a
>matter of convenience.  But, we shall see.

If you mean "Microsoft Office," I wasn't really thinking of this. The point
this person I cited (I don't remember who it was) was that this makes it
easier for a application to get "shelf space," because the shelf is the
Web. Payment is problematic, but distribution should be easy.

Obviously, Mosaic (and then Netscape) was a good example of this. A small
team, or even a single person, with a Good Idea, gets distribution. The Net
and Unix have long had this (with Unix tools and languages), but the Web
and applets may well extend this to a broader base.

We'll see.

>There are some features of Java which make it less than ideal for crypto
>applications.  These features can be overcome, but they will affect
>implementors and users.

I think the interesting target date to plan for is a year from now.

>(1) There are not many sources of high-quality entropy available to Java
>applets.  Keystroke timings and scribble windows are probably the best
>sources, but may represent an inconvenience for users.

Shouldn't be any worse or any better than with the status quo, right? I'm
not sure I see the Java issue. (I've been looking at SoundClip and
AudioClip, but only cursorily.)

By the way, Hal Finney is working on a bignum package.


--Tim May

Boycott "Big Brother Inside" software!
We got computers, we're tapping phone lines, we know that that ain't allowed.
---------:---------:---------:---------:---------:---------:---------:----
Timothy C. May              | Crypto Anarchy: encryption, digital money,
tcmay@got.net  408-728-0152 | anonymous networks, digital pseudonyms, zero
W.A.S.T.E.: Corralitos, CA  | knowledge, reputations, information markets,
Licensed Ontologist         | black markets, collapse of governments.
"National borders aren't even speed bumps on the information superhighway."

I wrote:

 > The complete specification of the Java Virtual Machine means
 > that the behavior of Java programs is perfectly
 > well-defined, and one does not have to tweek anything which
 > is processor or operating system dependent.

Scott Brickner <sjb@universe.digex.net> writes:

 > Unfortunately, this last statement isn't really true.  To
 > quote from the "Java Security" paper from some Princeton
 > researchers:

 >      The Java language has neighter a formal semantics nor
 >      a formal description of its type system.  We do not
 >      know what a Java program means, in any formal sense, so
 >      we cannot reason formally about Java and the security
 >      properties of the Java libraries written in Java. Java
 >      lacks a formal description of its type system, yet the
 >      security of Java relies on the soundness of its type
 >      system.

This is overly pessimistic.  Java primitive data types are fully
specified and Java operators are well-defined in the sense that
their results are unambiguous with specified input.  One
certainly does not have situations as one has in C, where things
like "int" or what happens to the sign bit on certain shifts is
left up to the implementor's discretion.  Even the typical "side
effects" tricks with passed parameters should be impossible with
Java programs.

While it is true that formal meta-language descriptions of Java
semantics and the universe of Java types are not currently
provided for the language, and the traditional kinds of formal
correctness proofs haven't been published, the language is
sufficiently simple and restricted to make it unlikely that major
loopholes will be discovered in this area.  I would be truly
surprised, for instance, if instruction sequences which
unbalanced the stack, wrote out of bounds, or accessed memory
locations as inconsistant types, were discovered to slip past a
bytecode verifier correctly implemented according to Sun's
recommendations.

Saying that the current specification does not support formal
proofs of correctness is far different than saying that the
language itself is broken.

 >      The Java bytecode is where the security properties
 >      must ultimately be verified . . . .  Unfortunately, it
 >      is rather difficult to verify the bytecode. . . .  The
 >      present type verifier cannot be proven correct, because
 >      there is not a formal description of the type system.

Again, he is not saying that the type verifier isn't correct,
merely that the materials with which to construct a proof have
not yet been dumped on top of his desk.

 >      Object-oriented type systems are a current research
 >      topic; it seems unwise for the system's security to
 >      rely on such a mechanism without a strong theoretical
 >      foundation.  It is not certain that an informally
 >      specified system as large and complicated as Java
 >      bytecode is consistent.

Not certain, but very very likely.  Due to the restricted nature
of Java and the bytecode, the checks that need to be done are
fairly simple transitive closures of relations involving local
program structure.  While the general theory of object-oriented
runtime structures can get hairy, Java's elimination of things
like multiple inheritance makes its own corner of this universe
considerably more tractable.

 >      We conclude that the Java system in its current form
 >      cannot easily be made secure.  Significant redesign of
 >      the language, the bytecode format, and the runtime
 >      system appear to be necessary steps toward building a
 >      higher-assurance system. . . . Execution of remotely-
 >      loaded code is a relatively new phenomenon, and more
 >      work is required to make it safe.

This summary might be a bit more impressive if the author had
included a bytecode fragment or two as a concrete example of
where such changes were necessitated.

 > I do think that the ideas embodied in Java are very
 > important, and will significantly shape the future of
 > computing, but Java itself may be just a stepping stone on
 > the way.

I think Java, as currently specified, is going to be around for
quite a while.  I further think that the concerns expressed above
will be addressed by augmentation of the existing specifications
and by construction of the necessary proofs of correctness, and
not by drastic surgery on the language and virtual machine as
they currently exist.

In any case, the anarchy of the free market rarely takes notice
of the theoretical musings of academicians.  Until Java
experiences a catastrophic and public train wreck, people will
continue to use it and its reputation will continue to grow.

--
     Mike Duvos         $    PGP 2.6 Public Key available     $
     mpd@netcom.com     $    via Finger.                      $