Strongly typed languages provide formal proof of type safety. Example 2 illustrates type checking in a logical framework called Agda. The purpose of this example is to give you direct exposure to the approach you will find in the DARPA Open Catalog.
Example 2 – Type Checking in the Agda Logical Framework
Figure 13 illustrates interactive type checking with two proofs. Recall the Interactive Proving discipline in the Early Verification life cycle. The goal is to allow only type safe look-up from a vector of natural numbers. For the proof to succeed the vector must have a length greater than zero. Consider the first proof called bad. Its first line specifies the type. The type is a disjunction of a value, T, called top, and the vector. The vector is a disjunction of the head of the vector, U, and the rest of the vector I. In the second line, bad calls the function look-up, not shown, which has three parameters. The first parameter is the length of the vector. The second parameter is a finite number. The third parameter is the vector. The third line is the result of a look-up from a vector of length zero. Notice the symbols ?1: ⊥ ?2: T. ⊥ is a special type called bottom that has no value. There is no proof of a type with no value. The type checker has inferred that the zero length list is a violation of the progress and preservation rules. The proof fails.
Figure 13. Type Checking in the Agda Logical Framework
The second proof is good. The type remains the same. The three proof steps beginning with ?0, ?1, and ?2 respectively proceed as follows: In line 2, we again call lookup. Notice that none of the symbols on the right contain ⊥. The proof step succeeds and progress continues under the rules. In line 3, we substitute (suc zero) for the first parameter and attempt a look-up from a vector of length one. Notice again that none of the symbols on the right contain ⊥. The proof step succeeds and progress continues under the rules. We do not explain the rest of the proof steps other than to say that you can observe by inspection of ?1: and ?2: at no time does the type ⊥ appear. The proof succeeds.
This section illustrates how type checking in the Agda logical framework stops programs from going wrong. The type system of Agda is an implementation of Martin Lof Type Theory. Type safety is available in both mainstream languages like Java and logical frameworks like Agda. Type safety is a common requirement in the DARPA Open Catalog and DARPA programs like Crash Safe and High Assurance Cyber Military Systems.
Conclusion – Type Safety and Cyber Strategy, 2015
The goal of this article was to describe how to increase assurance levels through early verification with type safety.
The article motivates type safety as a response in part to Strategic Goal II in the Department of Defense Cyber Strategy, 2015. An informal analysis of the DARPA Open Catalog indicates that type safety is a common requirement among emerging capabilities in response to Cyber Strategy, 2015.
To enable technology transition from DARPA programs the article proposes that a technical architecture with UML Templates is approachable by a wider number of government programs than those that can incorporate formal methods directly in their planning. The Early Evolutionary life cycle with named iterations and disciplines enables programs to incorporate type safe practices in program management and program planning. The article reminds the reader that templates, alternatively known as generics, are implemented in a variety of mainstream programming languages. It demonstrates how to stop programs from going wrong with Java, a mainstream programming language. An example using Agda, a logical framwork, provides insight into a more advanced approach representative of high assurance practices on programs like Crash Safe and HACMS.