4 ms·

I don't understand how lines 4 and 15 don't get caught by the compiler-- a String cannot extend an Integer? I'm not even sure how you would be able to write th

by mark242 10y ago

I don't understand how lines 4 and 15 don't get caught by the compiler-- a String cannot extend an Integer? I'm not even sure how you would be able to write this in Scala without violating rule number 1 of Scala, which is "never write the word null in your code".

partkyle 10y ago
In the article the author mentions that it's due to the null assignment in the first line of the `coerce` method. Look for the "Thanks, NULL!" section near the bottom.
- djsumdog 10y ago
  I wish Java had done more backwards comparability breakage. I wonder if we'd see the same issues if Java eliminated null in exchange for a Option/Maybe style monad and if generic types were saved instead of erased at compile time.
  - adrianN 10y ago
    You can't break backwards compatibility if you want to be a successful language for enterprise software development.
  - _old_dude_ 10y ago
    Java 9 is not fully compatible with Java 8. So we will soon see first hand if doing more backward compat breakage, for good they told, will be accepted or not. I predict there will be an internet outrage when Java 9 will be out.
batterseapower 10y ago
You can also inhabit any reference type in Scala, even without "null": by writing an infinite loop :-)
maxlybbert 10y ago
If I understand correctly, a constraint "? extends T" is checked at runtime, although in this case it could be checked at compile time (and, yes, it's easy to tell at compile time that String doesn't extend Number). Also the runtime check is performed on the actual value passed, which in this case is null, and therefore the check "can this cast be performed?" succeeds, but the actual cast fails. So, right now, nobody can show an exploit. But security researchers often manage to find exploits given this much to start with.
jcranmer 10y ago
Type constraint checking is done locally, and primarily relies on inductive reasoning to get soundness. Whenever you instantiate a generic instance, you need to provide a concrete type--be it a known class name, or a named type variable. This applies both to instantiation via new and to the inference of generic method arguments (you can't say Unsound.<?, ?>coerce(), for example). Since named type variables come from outer generic instances that need to be instantiated themselves, this provides the inductive proof. The first fly in the ointment is wildcard types. Wildcards are only legal as the type of a variable. They also don't work like you expect--each variable gets a different "capture" of wildcard types. Effectively, you use the capture conversion process to build up a complete set of constraints that a wildcard type must satisfy, and then you have to prove that it can be satisfied. The actual problem comes when we are asked to provide proof that there exists a type that satisfies the constraints. Normally, we would derive the value from something that forces an instantiation of a type. Instead, the example passes in literally a null proof: the null value, or I have no proof that such a type exists. Even then, it's not so bad, except we borrowed the "proof" provided by the null instantiation in a different context to prove that we could go from an Integer to a String. Put another way, the flow of the program works like this. The Constrain class is used to carry around in the compiler the notion the subclass constraint, and to provide the thing where wildcards get used. The upcast method is used to borrow the proof-of-existence from Constrain to actually do the cast. (The compiler doesn't complain here because it's all in terms of type variables--if there's a problem, it will be caught at the calling site). Since the coerce method declares no bounds on the type variables, there's no reason for line 15 to miscompile--all of the constraints between T and U have to work under the assumption that there is no axioms about their relationship. Line 10 compiles cleanly because all we're doing is stating that, to use this variable (store anything in it), there needs to exist a type between T and U. The use of null means we defer it to later. Line 11 has no problems whatsoever. In Line 12, we use the fact that ∃x: T ≤ x ≤ U to capture that x and so cast from type T to x to U without any problems. Fixing this is not easy. You somehow have to modify the type system to reflect the fact that a null value doesn't prove the existential qualifier, and it's not clear to me that there's a clean way to retrofit that into the way type checking is currently done in Java.

by mark242 10y ago

partkyle 10y ago

In the article the author mentions that it's due to the null assignment in the first line of the `coerce` method. Look for the "Thanks, NULL!" section near the bottom.

djsumdog 10y ago
I wish Java had done more backwards comparability breakage. I wonder if we'd see the same issues if Java eliminated null in exchange for a Option/Maybe style monad and if generic types were saved instead of erased at compile time.
- adrianN 10y ago
  You can't break backwards compatibility if you want to be a successful language for enterprise software development.
- _old_dude_ 10y ago
  Java 9 is not fully compatible with Java 8. So we will soon see first hand if doing more backward compat breakage, for good they told, will be accepted or not. I predict there will be an internet outrage when Java 9 will be out.

batterseapower 10y ago

You can also inhabit any reference type in Scala, even without "null": by writing an infinite loop :-)

maxlybbert 10y ago

If I understand correctly, a constraint "? extends T" is checked at runtime, although in this case it could be checked at compile time (and, yes, it's easy to tell at compile time that String doesn't extend Number). Also the runtime check is performed on the actual value passed, which in this case is null, and therefore the check "can this cast be performed?" succeeds, but the actual cast fails. So, right now, nobody can show an exploit. But security researchers often manage to find exploits given this much to start with.

jcranmer 10y ago

Type constraint checking is done locally, and primarily relies on inductive reasoning to get soundness. Whenever you instantiate a generic instance, you need to provide a concrete type--be it a known class name, or a named type variable. This applies both to instantiation via new and to the inference of generic method arguments (you can't say Unsound.<?, ?>coerce(), for example). Since named type variables come from outer generic instances that need to be instantiated themselves, this provides the inductive proof. The first fly in the ointment is wildcard types. Wildcards are only legal as the type of a variable. They also don't work like you expect--each variable gets a different "capture" of wildcard types. Effectively, you use the capture conversion process to build up a complete set of constraints that a wildcard type must satisfy, and then you have to prove that it can be satisfied. The actual problem comes when we are asked to provide proof that there exists a type that satisfies the constraints. Normally, we would derive the value from something that forces an instantiation of a type. Instead, the example passes in literally a null proof: the null value, or I have no proof that such a type exists. Even then, it's not so bad, except we borrowed the "proof" provided by the null instantiation in a different context to prove that we could go from an Integer to a String. Put another way, the flow of the program works like this. The Constrain class is used to carry around in the compiler the notion the subclass constraint, and to provide the thing where wildcards get used. The upcast method is used to borrow the proof-of-existence from Constrain to actually do the cast. (The compiler doesn't complain here because it's all in terms of type variables--if there's a problem, it will be caught at the calling site). Since the coerce method declares no bounds on the type variables, there's no reason for line 15 to miscompile--all of the constraints between T and U have to work under the assumption that there is no axioms about their relationship. Line 10 compiles cleanly because all we're doing is stating that, to use this variable (store anything in it), there needs to exist a type between T and U. The use of null means we defer it to later. Line 11 has no problems whatsoever. In Line 12, we use the fact that ∃x: T ≤ x ≤ U to capture that x and so cast from type T to x to U without any problems. Fixing this is not easy. You somehow have to modify the type system to reflect the fact that a null value doesn't prove the existential qualifier, and it's not clear to me that there's a clean way to retrofit that into the way type checking is currently done in Java.