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.
Endnotes
[MA 2001] James McDonald, John Anton, Network Vulnerability Analysis: A Formal Approach. March, 2001.
[HK 2009] Gernot Heiser, Gerwin Klein, seL4 : Formal Verification of a Software Kernel. October, 2009.
[MA 2003] Till Mossakowski, Don Sanella, etc, The Common Algebraic Specification Language: Semantics and Proof Theory. 2003.
[T 1958] Stephen Toulmin, The Uses of Argument. 1958.
[AK 2009] T. Scott Ankrum, Alfred Kromholz, Structured Assurance Cases : Three Common Standards. October, 2009.
[P 2002] Benjamin Pierce, Types and Programming Languages. 2002.
[SPEM 2008] Software and Systems Process Engineering Metamodel Specification. April, 2008.
[R 1970] Winston Royce, Managing the Development of Large Software Systems. 1970.
[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. Featerweight 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, artin 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