Travails of the JVM type system (was: What is Expressiveness in a Computer Language)

[David Hopwood]

Chris Uppal wrote:
> Maybe you are thinking that I mean that /because/ the JVM does verification,
> etc, at "runtime" the system is hybrid ?
> 
> Anyway that is /not/ what I mean.  I'm (for these purposes) completely
> uninterested in the static checking done by the Java to bytecode translator,
> javac.  I'm interested in what happens to the high-level, statically typed, OO,
> language called "java bytecode" when the JVM sees it.  That language has a
> strict static type system which the JVM is required to check.  That's a
> /static/ check in my book -- it happens before the purportedly correct code is
> accepted, rather than while that code is running.
> 
> I am also completely uninterested (for these immediate purposes) in the run
> time checking that the JVM does (the stuff that results in
> NoSuchMethodException, and the like).  In the wider context of the thread, I do
> want to call that kind of thing (dynamic) type checking -- but those checks are
> not why I call the JVMs type system hybrid either.
> 
> Oh well, having got that far, I may as well take another stab at "hybrid".
> Since the JVM is running a static type system without access to the whole text
> of the program, there are some things that it is expected to check which it
> can't.   So it records preconditions on classes which might subsequently be
> loaded.

It does, but interestingly, it wasn't originally intended to. It was intended
to be possible to check each classfile based only on that class' explicit
dependencies, without having to record constraints on the loading of future
classes.

However, the designers made various mistakes with the design of ClassLoaders
which resulted in the original JVM type system being unsound, and hence insecure.
The problem is described in
<http://www.cis.upenn.edu/~bcpierce/courses/629/papers/Saraswat-javabug.html>
(which spells my name wrong, I just noticed).

The constraint-based approach, proposed by Liang and Bracha in
<http://www.cs.purdue.edu/homes/jv/smc/pubs/liang-oopsla98.pdf>, was adopted
in order to fix this. There were other, simpler, solutions (for example,
restricting ClassLoader delegation to a strict tree structure), but the
responsible people at Sun felt that they were insufficiently expressive.
I thought, and still think, that they were mistaken. It is important for the
type system to be no more complicated than necessary if there is to be any
confidence in the security of implementations.

In any case, as shown by
<http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=4670071>, current JVM
implementations do *not* reliably support the patterns of ClassLoader delegation
that were intended to be enabled by Liang and Bracha's approach.

[This "bug" (it should be classed as an RFE) is, inexplicably given how few
programs are affected by it, the most voted-for bug in Sun's tracking system.
I get the impression that most of the commentators don't understand how
horribly complicated it would be to fix. Anyway, it hasn't been fixed for
4 years.]

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>