Recently and I discovered that and Scala are unsound. We submitted the finding and related discussion to OOPSLA, an academic conference on object-oriented . It has been great to see the paper making rounds in industrial circles, but there also seems to be a lot of confusion and I think that’s our fault. The paper was written for academics, and so it doesn’t discuss the issue from industry’s perspective. I’m crunching on a deadline right now, so let me write an abridged version of the industry-targeted paper here, focusing just on Java. Nada Amin Java programming What Does “Unsound” Mean? Most type systems aim to provide some sort of guarantee about how a well-type program will behave. For example, in many languages all memory accesses are “safe” in well-typed programs. A type system is sound if it actually succeeds at providing that guarantee. Thus informally a type system is sound if it ensures what its designers intended it to ensure. This is much like programming: a program is correct if it does what it is supposed to do. Java’s type system is intended to ensure that if a method asks for an Integer, then it will only ever be given Integers, never Strings. Thus the following pseudo-code is rejected by the type system: public Integer increment(Integer i) { return i + 1; }String countdown = increment(“98765432”); Sure, in JavaScript this might make sense, but Java is implemented very differently, and allowing this code could really mess up the heap (or even stack if you’ve ever enjoyed some C/C++ memory mismanagement errors). Now you might already know that Java’s type system has some unsound qualities. For example, for historical reasons Java has covariant arrays, making this code type check: String[] strs = { "NaN" };Object[] objs = strs;objs[0] = 1;String one = strs[0]; And when generics were added, Java used “raw types” so that genericized code could be compatible with pre-generics code. Consequently the following type checks: List<Integer> ints = Arrays.asList(1);List raw = ints;List<String> strs = raw;String one = strs.get(0); Thus both of these examples seem like they allow to contain an despite the fact that it is declared to have type . one Integer String Now this brings us back to intent. The designers the type system to allow this behavior. This is because, although these examples are clearly bad, there are many examples where this permissiveness is useful. After all, untyped languages are all about allowing bad things to happen so that more cool things can happen as well. And because this behavior was intentional, the designers planned for it. Every time you assign a value into an array (of a reference type), the runtime looks up the array value’s actual element type and throws an if it’s incompatible. So in the above sample, the assignment fails before the seemingly unsound assignment can be reached. Similarly, whenever is called on a , the runtime checks if the returned value is actually a in case a raw type was misused, throwing a otherwise. intended ArrayStoreException objs[0] = 1; String one = strs[0]; get List<String> String ClassCastException So Java’s type system seems to be as sound as it was intended to be, though maybe not as sound as you would like it to be. And since generics were introduced, it was believed to be “truly” sound so long as you didn’t use these intentional backdoors. “True” Unsoundness Here’s our “true” unsoundness example that has been making the rounds most recently. It assigns an instance to a variable. According to the Java specification, this program is well-typed, and according to the Java specification it should execute (unlike the aforementioned backdoors) and assign the instance to the variable, violating the intended behavior of well-typed programs. Thus it illustrates that Java’s type system is unsound. Integer String without exception actually Integer String Now you, like many others, might be confused by this example and might have already done some things to make yourself even more confused. So let me first name each common point of confusion: People don’t understand why this type checks or even actively believe it should type check. not If you copy this into your own Java compiler at hand, the compiler might say the program does not type check, contradicting my claim. If your compiler does type check it and then you run it, you get a , also contradicting my claim. ClassCastException You also wonder why this matters, especially since you and your colleagues are unlikely to ever write code like this. I’ll address all of these concerns, though out of order. “But It Doesn’t Compile” If your compiler doesn’t type-check our example, I have news for you. No, your compiler isn’t catching the bug. In fact, your compiler itself has a bug. Your compiler is broken. The Java specification says this example should type check and compile. Your compiler is supposed to implement that specification, and it’s failing here. It’s failing because it didn’t anticipate the corner case we created here. “But It’s Just a Corner Case” How many bugs have you dealt with have been corner cases? A good programmer is supposed to anticipate and handle corner cases, not just excuse a bug because it is hard to create. Sure, sometimes resources are constrained and you might decide that the bug is low priority, but you can only assess its priority after you identify it. So even if this bug turns out to be low priority, which I’ll get to in a bit, it’s still important to know it exists. “But an Exception is Thrown” And thank god one is, and purely due to some good luck! Remember how a call to on a secretly checks that the returned value is actually a ? This secret check is done for backwards compatibility with raw types. It shouldn’t be necessary when there are no raw types in the program. But thanks to it, a is always thrown when our example is run (if your compiler is smart enough to compile it). get List<String> String ClassCastException So had history been a little different, either with Sun deciding to throw out backwards compatibility after adding generics, or with Sun adding generics into the JVM, or with Java first being released with generics, then this exception would not be thrown. Instead I could cast anything into an and get direct access to the raw bytes of many objects, which I could then use to inject arbitrary code (using to bypass security measures). int[] return-oriented programming “But No One Would Ever Write This” You probably would never write this, and your colleagues would never write this. That reasoning is good to apply in many situations. I in fact do this ; it’s a huge part of my research agenda. But you have to be careful where you apply it. Soundness is a security guarantee, not a usability concern. What matters is if can write this, because then that someone can get around the security measures that people have placed their confidence in and do whatever they would like to do. In the case of soundness, it’s the malicious programmer you should be worried, not just you and your friends. all the time someone “But The Code Shouldn’t Type-Check” Many people call out the type and say it should be invalid because requires its second type argument to be a subtype of its first, but , and every supertype of , is not a subtype of . But this reasoning confuses invalidity and uninstantiability. It’s actually faulty reasoning that’s been around in both industry and academia for at least as long as I’ve been out of high school (which has been a while). Constrain<U,? super T> Constrain T T U Here’s a simpler version of the fallacy: class Foo<T extends Number> {Number foo(T t) { return t; }} Is it safe for to be a valid type? For example, is the following code safe: Foo<String> Number bar(Foo<String> foos) { return foos.foo("NaN"); } The conventional wisdom up until now, and probably your gut instinct, would say this is unsafe, since it turns a into a , but the fact is that it’s completely safe. Here’s an equivalent program that illustrates why: String Number interface IFoo<T> {Number foo(T t);} class Foo<T extends Number> implements IFoo<T> {public Number foo(T t) { return t; }} Number bar(IFoo<String> foos) { return foos.foo("NaN"); } For any class with a constrained type parameter, I can just make a corresponding interface without that constraint and use that throughout the program. This will behave identically to the original program. (There are some clarifications to this, but I’ll leave them to the .) paper So why does it seem like should be invalid? How is it safe? Well, the answer to both is the same: is uninstantiable. You’ll never be able to create an instance of because is not a subtype of . Thus the seemingly unsafe invocation of in will never happen because you can’t invoke a method of an object that can never exist. Foo<String> bar Foo<String> Foo<String> String Number foo bar So by this same reasoning it’s perfectly safe for to be valid. You’ll only ever be able to have an instance of it if is a subtype of at run time, satisfying the constraint. Constrain<U,? super T> T U But is inhabitable in Java, because inhabits every reference type. So keep that in mind as I explain why this program type checks. Constrain<U,? super T> null Wildcard Capture A Java wildcard, , is not a type. It is simply a piece of syntax representing something unknown. And different wildcards can represent different unknown types. So to reason about wildcards, Java uses a process called . ? wildcard capture Suppose we have an expression of type . There is a wildcard in the type of this expression. The type-checker doesn’t know what it represents, but it does represent something, so the type-checker gives that unknown something a temporary name, say . Furthermore, the type-checker knows that the unknown something must at least be a supertype of . Thus the type-checker views as having type where is some supertype of . e Constrain<U,? super T> X T e Constrain<U,X> X T But the type-checker knows something more. It knows that must be a valid type argument. Consequently, the type-checker also notes that must be a subtype of . We call this the constraint on the wildcard, whereas is the explicit constraint on the wildcard. I found out that, although uncommon, this implicit constraints are in fact used for type-checking a number of Java libraries. The gives a specific example showing why implicit constraints are important. X X U implicit super T paper Now look at the example again. In the call to , the type-checker does the aforementioned wildcard-capture process and views as having where is (explicitly) a supertype of and (implicitly) a subtype of . Consequently it infers to be the type argument to and uses its explicit and implicit constraints to type-check the rest of the invocation. bind.upcast(constrain, t) constrain Constrain<U,X> X T U X bind.upcast Thanks, Null! Okay, so if the wonky type isn’t the source of unsoundness, what is? Well, amazingly enough, it turns out null pointers don’t just cause bugs in programs, they cause bugs in type systems too! The reasoning for wildcard capture completely forgets about null pointers. It assumes there must be some actual for some , an assumption that manifests itself in the implicit constraint on . So all of this boils down to a null-pointer bug. But unlike most null-pointer bugs, this one took 12 years to discover. Oh, and it’s also not nearly as easy to fix as most null-pointer bugs, since every feature involved is used in practice. But the Java team is working on fixing it. And before you once more insist that the solution is to disallow the type, realize that that kind of reasoning is what delayed core Scala’s proof of soundness (without null) for a whole decade, and I’m not particularly eager to spend a decade solving this. Constrain<U,X> X X Constrain<U,? super T> P.S. Future language designers, please keep this in mind! Especially if you’re not compiling to the JVM. Java was lucky it was held back by backwards compatibility; you may not be so lucky. is how hackers start their afternoons. We’re a part of the family. We are now and happy to opportunities. Hacker Noon @AMI accepting submissions discuss advertising &sponsorship To learn more, , , or simply, read our about page like/message us on Facebook tweet/DM @HackerNoon. If you enjoyed this story, we recommend reading our and . Until next time, don’t take the realities of the world for granted! latest tech stories trending tech stories

Java is Unsound: The Industry Perspective

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

Java bits: 0xFF and 0xFFL

The Noonification: Charting a Path for Global AI Regulation (11/14/2023)

100+ Free Pluralsight Courses to learn Python, Java, and Spring Boot

100 Pieces of Programming Advice from the Book Clean Code by Robert Martin

10 Useful Tools and Libraries for Programmer and IT Professionals

Java bits: 0xFF and 0xFFL

The Noonification: Charting a Path for Global AI Regulation (11/14/2023)

100+ Free Pluralsight Courses to learn Python, Java, and Spring Boot

100 Pieces of Programming Advice from the Book Clean Code by Robert Martin

10 Useful Tools and Libraries for Programmer and IT Professionals

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps