Using SPARK-Ada to Model and Verify a MILS Message Router

Abstract

The concept of information classification is used by all nations to control information distribution and access. In the United States this is referred to as Multiple Levels of Security (MLS), which includes designations for unclassified, confidential, secret, and top secret information. The U.S. Department of Defense has traditionally implemented MLS separation via discrete physical devices, but with the transformation of military doctrine to net-centric warfare, the desire to have a single device capable of Multiple Independent Levels of Security (MILS) emerged. In this paper we present a formal model of a MILS message router using SPARK-ADA. The model is presented as a case study for the design and verification of high assurance computing systems in the presence of an underlying separation kernel. We utilized the correctness-by-design approach to secure system development and discuss the limitations of that approach for the type of system we model.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2006
Accession Number
ADA459119

Entities

People

  • Bryan Rossebo
  • Jim Alves-foss
  • Paul Jaszkowiak
  • Paul Oman
  • Ryan Blue

Organizations

  • University of Idaho

Tags

Communities of Interest

  • Cyber
  • Engineered Resilient Systems

DTIC Thesaurus Topics

  • Abstracts
  • Classification
  • Communication Channels
  • Computer Network Security
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computer Viruses
  • Computers
  • Control Systems
  • Cybersecurity
  • Mathematical Models
  • Models
  • Secure Communications
  • Software Development
  • Specifications
  • Standards

Fields of Study

  • Computer science

Readers

  • Enterprise Information Systems Architecture and Joint Command Capability Interoperability Support.
  • Government and Public Administration Law.
  • Statistical inference.