• Home
  • Resources
    • Find Resources by Topic Tags
    • Cybersecurity Policy Chart
    • CSIAC Reports
    • Webinars
    • Podcasts
    • Cybersecurity Digest
    • Standards & Reference Docs
    • Journals
    • Certifications
    • Acronym DB
    • Cybersecurity Related Websites
  • Services
    • Free Technical Inquiry
    • Core Analysis Task (CAT) Program
    • Subject Matter Expert (SME) Network
    • Training
    • Contact Us
  • Community
    • Upcoming Events
    • Cybersecurity
    • Modeling & Simulation
    • Knowledge Management
    • Software Engineering
  • About
    • About the CSIAC
    • The CSIAC Team
    • Subject Matter Expert (SME) Support
    • DTIC’s IAC Program
    • DTIC’s R&E Gateway
    • DTIC STI Program
    • FAQs
  • Skip to primary navigation
  • Skip to main content
  • Skip to primary sidebar
  • Skip to footer
Login / Register

CSIAC

Cyber Security and Information Systems Information Analysis Center

  • Resources
    • Find Resources by Topic Tags
    • Cybersecurity Policy Chart
    • CSIAC Reports
    • Webinars
    • Podcasts
    • Cybersecurity Digest
    • Standards & Reference Docs
    • Journals
    • Certifications
    • Acronym DB
    • Cybersecurity Websites
  • Services
    • Free Technical Inquiry
    • Core Analysis Task (CAT) Program
    • Subject Matter Expert (SME) Network
    • Training
    • Contact
  • Community
    • Upcoming Events
    • Cybersecurity
    • Modeling & Simulation
    • Knowledge Management
    • Software Engineering
  • About
    • About the CSIAC
    • The CSIAC Team
    • Subject Matter Expert (SME) Support
    • DTIC’s IAC Program
    • DTIC’s R&E Gateway
    • DTIC STI Program
    • FAQs
  • Cybersecurity
  • Modeling & Simulation
  • Knowledge Management
  • Software Engineering
/ Journal Issues / Early Prevention & Best Practices / Increasing Assurance Levels Through Early Verification with Type Safety – Unabridged Version

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

Published in Journal of Cyber Security and Information Systems
Volume: 3 Number: 2 - Early Prevention & Best Practices

Author: Rick Murphy
Posted: 02/09/2016 | Leave a Comment

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.

Pages: Page 1 Page 2 Page 3 Page 4 Page 5 Page 6

Previous Article:
« Managing Operational Resilience
Next Article:
Achieving Information Dominance: Unleashing the Ozone Widget... »

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

Author

Rick Murphy
Rick Murphy
Rick Murphy has over 25 years in software architecture and engineering in the private sector, public sector and academia. Rick currently works in higher order functional programming languages and logics and has a particular interest in category theory, type theory and proof theory.

Reader Interactions

Leave a Comment Cancel

You must be logged in to post a comment.

sidebar

Blog Sidebar

Featured Content

Data Privacy Day - Jan 28

Data Privacy Day is January 28th

You can help create a global community that respects privacy, safeguards data, and enables trust. You can help teach others about privacy at home, at work, and in your community.

Learn How

Featured Subject Matter Expert (SME): Daksha Bhasker

A dynamic CSIAC SME, Senior Principal Cybersecurity Architect, Daksha Bhasker has 20 years of experience in the telecommunications services provider industry. She has worked in systems security design and architecture in production environments of carriers, often leading multidisciplinary teams for cybersecurity integration, from conception to delivery of complex technical solutions. As a CSIAC SME, Daksha's contributions include several published CSIAC Journal articles and a webinar presentation on the sophiscated architectures that phone carriers use to stop robocalls.

View SME's Contributed Content

The DoD Cybersecurity Policy Chart

The DoD Cybersecurity Policy Chart

This chart captures the tremendous breadth of applicable policies, some of which many cybersecurity professionals may not even be aware, in a helpful organizational scheme.

View the Policy Chart

CSIAC Report - Smart Cities, Smart Bases and Secure Cloud Architecture for Resiliency by Design

Integration of Smart City Technologies to create Smart Bases for DoD will require due diligence with respect to the security of the data produced by Internet of Things (IOT) and Industrial Internet of Things (IIOT). This will increase more so with the rollout of 5G and increased automation "at the edge". Commercially, data will be moving to the cloud first, and then stored for process improvement analysis by end-users. As such, implementation of Secure Cloud Architectures is a must. This report provides some use cases and a description of a risk based approach to cloud data security. Clear understanding, adaptation, and implementation of a secure cloud framework will provide the military the means to make progress in becoming a smart military.

Read the Report

CSIAC Journal - Data-Centric Environment: Rise of Internet-Based Modern Warfare “iWar”

CSIAC Journal Cover Volume 7 Number 4

This journal addresses a collection of modern security concerns that range from social media attacks and internet-connected devices to a hypothetical defense strategy for private sector entities.

Read the Journal

CSIAC Journal M&S Special Edition - M&S Applied Across Broad Spectrum Defense and Federal Endeavors

CSIAC Journal Cover Volume 7 Number 3

This Special Edition of the CSIAC Journal highlights a broad array of modeling and simulation contributions – whether in training, testing, experimentation, research, engineering, or other endeavors.

Read the Journal

CSIAC Journal - Resilient Industrial Control Systems (ICS) & Cyber Physical Systems (CPS)

CSIAC Journal Cover Volume 7 Number 2

This edition of the CSIAC Journal focuses on the topic of cybersecurity of Cyber-Physical Systems (CPS), particularly those that make up Critical Infrastructure (CI).

Read the Journal

Recent Video Podcasts

  • Privacy Impact Assessment: The Foundation for Managing Privacy Risk Series: The CSIAC Podcast
  • Agile Condor: Supercomputing at the Edge for Intelligent Analytics Series: CSIAC Webinars
  • Securing the Supply Chain: A Hybrid Approach to Effective SCRM Policies and Procedures Series: The CSIAC Podcast
  • DoD Vulnerability Disclosure Program (VDP) Series: CSIAC Webinars
  • 5 Best Practices for a Secure Infrastructure Series: The CSIAC Podcast
View all Podcasts

Upcoming Events

Wed 20

SANS Stay Sharp: Blue Team Operations 2021

January 18 - January 20
Organizer: SANS Institute
Wed 20

SANS Cyber Security Central: Jan 2021

January 18 - January 23
Organizer: SANS Institute
Wed 20

AI Champions, Online – Supply Chain

January 19 @ 14:00 - January 21 @ 15:30 EST
Thu 21

SANS Cyber Threat Intelligence Summit 2021

January 21 - January 22
Organizer: SANS Institute
Fri 22

SANS Cyber Threat Intelligence Solutions Track 2021

January 22 @ 09:00 - 17:00 EST
Organizer: SANS Institute
View all Events

Footer

CSIAC Products & Services

  • Free Technical Inquiry
  • Core Analysis Tasks (CATs)
  • Resources
  • Events Calendar
  • Frequently Asked Questions
  • Product Feedback Form

About CSIAC

The CSIAC is a DoD-sponsored Center of Excellence in the fields of Cybersecurity, Software Engineering, Modeling & Simulation, and Knowledge Management & Information Sharing.Learn More

Contact Us

Phone:800-214-7921
Email:info@csiac.org
Address:   266 Genesee St.
Utica, NY 13502
Send us a Message
US Department of Defense Logo USD(R&E) Logo DTIC Logo DoD IACs Logo

Copyright 2012-2021, Quanterion Solutions Incorporated

Sitemap | Privacy Policy | Terms of Use | Accessibility Information
Accessibility / Section 508 | FOIA | Link Disclaimer | No Fear Act | Policy Memoranda | Privacy, Security & Copyright | Recovery Act | USA.Gov

This website uses cookies to provide our services and to improve your experience. By using this site, you consent to the use of our cookies. To read more about the use of our site, please click "Read More". Otherwise, click "Dismiss" to hide this notice. Dismiss Read More
Privacy & Cookies Policy

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may affect your browsing experience.
Necessary
Always Enabled

Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.

Non-necessary

Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.