Nada Amin and Ross Tate recently published an excellent paper pointing out a soundness hole they found in the Java and Scala type systems. The actual mechanics of the bug are pretty close to an issue that comes up in type systems for functional languages, so I'm going to have a go at explaining it from that point of view (I still highly recommend reading the original paper, though).
In OCaml, you can write the type of equality witnesses, whose values represent evidence that two types are the same:
type ('a, 'b) eq = Refl : ('a, 'a) eq
(There's nothing OCaml-specific here except the syntax: the same type exists in Haskell, and both are a less powerful version of the equality types in dependently-typed languages)
The type ('a, 'b) eq
takes two parameters 'a
and 'b
, but you can
only make values of this type (Refl
) when you know that the two
parameters are equal. So, a value of type ('a, 'b) eq
is evidence
that 'a
and 'b
are the same type.
You can use this evidence to convert an 'a
to a 'b
:
let cast (type a) (type b) (eq : (a, b) eq) (x : a) : b=
match eq with Refl -> x
To cast x
from an a
to a b
, we match on eq
(applying our
evidence that a
and b
are the same type), then return x
which we
now know to be of type b
, since b = a
.
For this to be type safe, we need to know that Refl
is really the
only way of coming up with a value of type ('a, 'b) eq
. If we are
able to construct a value of type, say, (int, string) eq
, then type
safety breaks:
# let lies : (int, string) eq = Obj.magic 0;;
val lies : (int, string) eq = Refl
# cast lies 42;;
Segmentation fault
OCaml's type safety relies on not being able to construct an (int, string) eq
(at least, without using the unsafe intrinsics in Obj).
Amin and Tate follow the same path, starting with something that looks
like the ('a, 'b) eq
type:
static class Constrain<A, B extends A> {}
There are two differences from ('a, 'b) eq
. First, instead of
equality, this talks about subtyping (B extends A
rather than B = A
). This difference isn't terribly important here, since B extends A
is enough information to cast B
to A
.
The second difference is deeper: because this class exposes the B extends A
constraint, we can't even talk about the type
Constraint<Integer, String>
. With OCaml's ('a, 'b) eq
type, there
is always a type (t1, t2) eq
regardless of what t1
and t2
are. This separates the proposition (t1, t2) eq
, which is a
sentence saying "t1 and t2 are equal", from the proof Refl
, which
is evidence that the sentence is actually true.
Constrain<A, B>
doesn't give us that, because in Java Constrain<A, B>
is not even a type unless we already know that B extends A
. It's
a type error in Java to write a function taking a parameter of type
Constrain<Integer, String>
, because we don't know that String extends Integer
. By constrast, such a function is perfectly fine in
OCaml, but it can never be called because you'll never be able to
supply a suitable argument (without using unsafe functions like
Obj.magic
).
Amin and Tate find a nice way around this, using the type:
Constrain<U, ? super T>
This is a type regardless of what U
and T
are. In particular,
Constrain<Integer, ? super String>
is a type. But since we can only
have a Constrain<U, ? super T>
if the ?
extends U
, then we must
have T
extends ?
extends U
, so having an instance of this type
implies that T
extends U
.
It's even possible to write the cast
function that applies this
evidence to turn a T
into a U
, although we have to jump through a
few more hoops than the OCaml version does:
static <T, U> U cast(Constrain<U, ? super T> eq, T t) {
return new Bind<U>().upcast(eq, t);
}
static class Bind<A> {
<B extends A> A upcast(Constrain<A, B> constrain, B b) {
return b;
}
}
(The exact code needed to make cast
typecheck varies by compiler
version. I've adapted some code from Figure 1. of the paper, but they
give a few versions that work on different compilers).
By itself, there's nothing problematic about this function. It's able
to turn a T
into a U
, but only if you provide a Constrain<U, ? super T>
. We should only be able to come up with one of those if T
is in fact a subtype of T
, so this seems just as safe as the cast
function in OCaml.
The trouble is that Java types have more values than they should:
null
is a value of every reference type, and null
will happily act
as evidence for lies:
String zero = cast(null, 0);
Running this, we get fireworks, without using any unsafe features:
Exception in thread "main" java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
at Unsound.main(Unsound.java:12)
(The explosion is a bit less dramatic than in OCaml, because the JVM
doesn't actually trust the javac compiler's type checking of generics,
and inserts dynamic class checks in generic code. So, the effect is
that we see a ClassCastException
in a program containing no casts,
rather than a segfault).