Increasing Assurance Levels Through Early Verification with Type Safety – Unabridged Version

https://api.army.mil/e2/c/images/2018/03/13/509803/max1200.jpg
Image Credit: U.S. Army

Posted: February 9, 2016 | By: Rick Murphy

Today defense, intelligence and civilian agencies are focused on cyber security challenges. Early results seem conflicting. While media reports are surfacing of unhackable drones, government programs report shortages of qualified applicants to fill cyber security positions. As exploits proliferate and threats mutate, operational teams seek to achieve efficiencies against the grueling critical patch update cycle. Though most assurance practices remain retrospective, there is anecdotal evidence that increased assurance levels may be achievable at scale.

In response to these challenges the Secretary of Defense released the Department of Defense Cyber Strategy, April 2015. The Cyber Strategy describes five strategic goals and their associated implementation objectives. Strategic Goal II : Defend the DoD Information Network, Secure DoD Data, and Mitigate Risk to DoD Missions explains “DoD must raise the bar on technology and innovation to stay ahead of the threat by enhancing its cyber defense capabilities, including by building and employing a more defendable network architecture in the Joint Information Environment (JIE).” Further, implementation objectives associated with Strategic Goal II include “Build the Joint Information Environment (JIE) single security architecture” and “As a part of JIE planning DoD will develop a framework for developing and integrating new defensive techniques into DoD’s cybersecurity architecture […] .”

Type Safety and Technology Transition

There’s good news and bad. The good news is that advanced programs are preparing new capabilities in response to these cyber security challenges. There is no shortage of new capabilities coming to a program you manage, lead or support. The bad news is not news at all. It is hard work to use new capabilities. And that’s true regardless of the capabilities you may need to use.

This article will help you and your program use some of those capabilities. It will also help you relate those capabilities to a “defendable network architecture” and “a single security architecture” as well as “developing and integrating new defensive techniques into DoD’s cybersecurity architecture […].” In order to do so, it explains how to increase assurance levels through early verification with type safety.

Type safety is a property of a programming language that prevents undesirable behavior. It is best known by the slogan “Well Typed Programs Don’t Go Wrong” attributable to Turing Award winner Robin Milner. Type safety is the most common form of software verification because it is part of many programming languages. Verification through type safety is a property we should also expect from a technical architecture. Though not common, a verifiable architecture is not new [MA 2001, MS 2003, HK 2009]. New challenges mean new requirements. This article proposes that verification in architecture is a response to those requirements.

The sections that follow explain type safety as part and only part of a response to Strategic Goal II. After some background, the section on assurance levels differentiates two well known approaches to assurance: argumentation and computation. The approach in this article is computational. The section on life cycle management provides a structured, recurring life cycle to explain what we mean by early. Next, the section on type safe technical architecture describes how programs already familiar with the Unified Modeling Language can strengthen their approach to technical architecture with type safety. And the section on type safety and software verification explains a well-known, but not well motivated code sample of how to stop programs from going wrong with type safe design. The article concludes with some qualifications of what we might hope to achieve towards whole systems security with type safety.

The article makes modest technical assumptions. The intended audience includes program and project managers, software architects and developers. You don’t have to be an expert in type theory or formal methods to benefit. Individuals with a background in software assurance will appreciate the novel contribution the article makes to type safe technical architecture by defining functional abstractions in the Unified Modeling Language (UML). The purpose is to enable technology transition to a larger audience so the ideas spread widely. Likewise, security and systems engineers who have exhausted static analysis will gain insight into design time assurance practices sometimes overlooked by software engineers. Senior executives can use the article without a detailed understanding of software assurance or type safety. Ask a few questions and gauge the response. You will learn a few things about your approach to achieving the implementation objectives of Strategic Goal II.

Want to find out more about this topic?

Request a FREE Technical Inquiry!