A Technique for Proving Specifications are Multilevel Secure

Abstract

This document describe a technique for verifying that a design for an operating system or subsystem expressed in terms of a formal specification is consistent with a particular model of multilevel security. The technique to be described is mathematically rigorous and, if applied properly, gives assurance that the given design is multilevel secure by this particular model. The technique is supported by a collection of automated tools. These tools assist the user in the performance of a large amount of detailed routine tasks that must be performed to apply the technique. In general, contemporary formal verification techniques such as the one described here involve a great deal of repetitive, detailed, uninteresting steps that are necessary to maintain the rigor of the proof process. The proof are usually larger and more complex than the system being proved. Keywords: Critical technology.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 10, 1980
Accession Number
ADB145741

Entities

People

  • Richard J. Feiertag

Organizations

  • Montana State University

Tags

Communities of Interest

  • Advanced Electronics
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Automation
  • Classification
  • Computations
  • Computer Science
  • Computers
  • Control Systems
  • Databases
  • Debugging
  • Department Of Defense
  • Equations
  • Errors
  • Generators
  • Hard Copy
  • Language
  • Qualifications
  • Robotics
  • Specifications

Readers

  • Cybersecurity.
  • Database Systems and Applications
  • Systems Analysis and Design