Type Safety and Software Verification
Well typed programs don’t go wrong, but how do we stop them from going wrong? UML templates are artifacts in a technical architecture that represent computation. What about the computation itself?
This section illustrates how type checking at compile-time stops programs from going wrong. Programs don’t go wrong because the type checker stops the compiler. The type checker enforces verification early at compile-time rather than allow exceptions at run-time. Recall that in the Type Specification and Test Execution iterations generic types are analyzed and specified for use by the developer to ensure compile-time constraints are enforced. Parametric class types pass compile-time checks. Tests in all test cases validate casts in source code as it is developed and functions and operations satisfy run-time constraints. Agile practitioners will recognize the Test Driven Development discipline specialized for type safety.
We proceed with two examples that illustrate compile-time type checking. Example 1 builds on the UML approach above and illustrates type checking with Java Generics. Recall that Generics in Java is a synonym for Templates in UML. We expect more programs are familiar with Java, so it serves our needs for technology transition. Example 2 illustrates type checking in a logical framework called Agda. Agda provides different progress and preservation rules than Java. These rules increase the formal nature of proof in Agda’s type system. For more on UML Templates and Java Generics see Architecture for Government : A Modest Proposal. And for Agda Generic Architecture for Government : A Fast Track to EAl 7. (add links)
Java 1.5 introduced generic types to enable future versions of the language to provide type checking. Type checking evolved in subsequent releases and support for type safety strengthened recently with type inference. Example 1 describes how Java generics eliminate run-time exceptions resulting from incorrect casts. We begin with a review of the Linked List example from the Generic Java Tutorial [BOSW 1998].
Example 1. Linked List.
Figure 9 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.
Figure 9. Raw Types
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 with -Xlint: unchecked produces the output in Figure 10. 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 2013] advises the developer that the operation is unsafe and imputes blame to the developer for safety of the system.
Figure 10 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 10. Compiler and Run-time Output
Figure 11 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 11. Generic Types
In Figure 12 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.
Figure 12. Compile-time Failure. Well typed programs don’t go wrong.
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 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 agency 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 paper.