Example 1 – Linked List
Figure 7 uses the Linked List raw type from the Java Collections framework. Raw types allow the developer to add objects of any type to the collection and return types of Object from the collection. This implies that when a developer retrieves an object from the collection they must both discern and cast to the correct type to avoid a run-time exception. The code below illustrates the case of an incorrect cast where the developer attempts to cast an object of type String to Byte. The exception occurs at run-time, possibly after the code has already been pushed to production.
With the addition of generics in Java 1.5, the compiler emits the warning that “Note: src/M.java uses unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details.” The warning allows compilation to complete, producing byte code targeted to the legacy JVM. The appearance of the words “unsafe” and “unchecked” should alarm any reasonable person. They are ignored and the warning often circumvented by most developers. A recompile Typeswith -Xlint: unchecked produces the output in Figure 7. In Java an unsafe operation is the evaluation of an expression whose type cannot be verified by the compiler. An unchecked exception is an exception which the language does not require the developer to catch, or handle. Run-time exceptions are unchecked exceptions. The Java Language Specification [JLS 2013JLS 2013] advises the developer that the operation is unsafe and imputes blame to the developer for safety of the system.
Figure 8 lists the compiler and run-time output when we adhere to the warning and implement -Xlint : unchecked. The compiler emits a warning for each call where an unchecked exception occurs. At run-time the the systems reports the ClassCastException that String cannot be cast to Byte. Again, the ClassCastException occurs at run-time, possibly after the code has been pushed to production.
Figure 9 lists the type-safe approach. Each instance of Linked List is parametrized by the type of its element: Byte, String and LinkedList respectively. In each case when an object is added to a collection, it is added according to its type. As expected, the cast from Object to String is no longer required because the elements in LinkedList are LinkedLists of String elements and we extract an element with the known type: String, not Object.
Figure 9 – Generic Types
Figure 10 – Compile-time Failure. Well typed programs don’t go wrong.
In Figure 10 we have the expected result. The type checker stops the compiler with a compile-time error. The compiler emits the error “incompatible types : String cannot be converted to Byte.” The code never makes it to production. We have eliminated a class of exceptions early that may not have been discovered until run-time. And run-time is just too late when your systems are under attack.
Generics were added to Java after an installed base of the Java Virtual Machine (JVM) had already been established. To support backwards compatibility, generics were implemented with type erasure [IPW 2002]. Erasure rewrites source code from the format that enforces constraints at compile time to a format that is compatible with the JVM. As the name implies parametrized type information is removed to maintain backwards compatibility. Generic types subject to erasure are called non-reifiable types [N 2007] at run-time. Non-reifiable means only the raw type, not the generic type, can be reconstructed from its representation in the JVM. Heap pollution is an informal term that describes an undesirable coding practice when a developer assigns a variable of a generic type to a variable of a raw type.
Java, like most other programming languages, has been the subject of exploits. Early versions of its type system were the subject of type confusion or type spoofing exploits [MF 1999, S 1997]. It appears that type confusion exploits were disclosed and resolved consistent with industry best practices. Papers [OW 1997, ORW 1997] that describe development of the Pizza compiler, a precursor to Java Generics and Scala, included commentary on security related to the use of generic types. [GAS 2005] restates this commentary. The Java Generics specification and tutorial [GOSW 1998, GOSW2 1998] are silent on this issue and there is no evidence that recent exploits have been reported. Variable argument methods with non-reifiable formal parameters present a special case where improved compiler warnings and errors were introduced to account for blame in claims made that a method is safe [O 2013O 2013]. A secure system implies both memory and type safety as well as segmentation of unsafe operations. This is not a general paper on security, but a discussion of type safety implies some discussion of memory safety and security. Safety and trust are widely advertised in Java’s security architecture with references to the Java sandbox and platform security models. The current Java platform security model is comprised of permissions; protection domains and security policies; and security managers and access controllers. The platform security model is considered “code-centric” in that it restricts access to operations that a class can perform in the run-time environment. The inclusion of the sun.misc.unsafe library is not widely advertised, but easy to identify through an Internet search and readily accessible to all Java developers. This library allows unsafe operations. Use of this unsafe library is often motivated by performance gains at the risk of memory safety. Oracle conducted an informal survey of unsafe library usage and the hostile reaction to including the term “unsafe” in its name was startling [VG 2014]. There is clearly a commitment to performance over safety in the developer community. The agencies should consider sun.misc.unsafe as a candidate for static analysis. This paper does not further discuss memory safety or its relation to type safety or security. No inferences should be made that type safety provides memory safety from this or other sections of this article.
Conclusion – Type Safety and Technical Architecture
The goal of this article was to describe how to represent type safety in a technical architecture. Type safety is a common requirement for increasing assurance levels as observed in the DARPA Open Catalog. The article provides four examples from a type safe technical architecture in UML and one example of compile-time type checking. The unabridged version of this article, available on-line, explains what it means to increase assurance levels early in a life cycle. It does so by describing an early evolutionary life cycle including its iterations and associated disciplines. The unabridged version also provides an additional example using stronger compile-time type checking with dependent types.
Endnotes
[GAS 2005] : Ahmed Ghoneim, Sven Apel, Gunter Saake, Evolutionary Software Life Cycle for Self Adapting Software Systems. 2005.
[BOSW 1998] : Gilad Bracha, Martin Odesrsky, David Stoutamire, Phillip Wadler, Making the Future Safe for the Past : Adding Genericity to the Java Programming Language. October, 1998.
[JLS 2013] : James Gosling, Bill Joy, Gilad Bracha, Alex Buckley, The Java Language Specification. February, 2013.
[IPW 2002] : Atushi Igarishi, Benjamin Pierce, Philip Wadler. Featherweight Java : A Minimal Core Calculus for Java and GJ. January 2002.
[N 2007] : Jamie Nino. The Cost of Erasure in Java Generics Type Systems. March 2007.
[MF 1999] : Gary McGraw, Edward Felten. Securing Java. January, 1999.
[S 1997] : Vijay Saraswat, Java is Not Type Safe. August, 1997.
[OW 1997] : Martin Odersky, Philip Wadler. Pizza into Java: Translating Theory into Practice. January, 1997.
[ORW 1997] : Martin Odersky, Enno Runne, Philip Wadler. Two Ways to Bake Your Pizza – Translating Parameterised Types into Java. November, 1997.
[GOSW 1998] : Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. GJ Specification. May 1998.
[GOSW2 1998] : Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. GJ: Extending the Java Programming Language with Type Parameters. August, 1998.
[O 2013] : Oracle technical staff. Improved Compiler Warnings and Errors When Using Non-Reifiable Formal Parameters with Varargs Methods. 2013.
[VG 2014] : Victor Grazi, Unsafe at any Speed; Oracle Surveys community about promoting sun.misc.Unsafe. February, 2014
[TSM 2014] : Type Safe Method Plug-in. rickmurphy.org/epf-method-plugin.zip. 2014.
[GAGM 2014] : Generic Architecture for Government : A Modest Proposal for Better Safety and Sharing. rickmurphy.org/gag-modest.zip, OMG 2014.