Security Kernel Verification Techniques: Algorithmic Representation,

Abstract

A security kernel is a hardware and software mechanism that enforces access controls to information within a computer system. Given a formal specification for a kernel, this report shows how to construct an algorithmic or programming language representation of the kernel. A technique is suggested for proving that the algorithmic representation exhibits the specified user-visible behavior. A sequence of lower levels of specification, formalizing the levels of abstraction of Dijkstra, is essential to the construction and proof technique. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 1978
Accession Number
ADA054098

Entities

People

  • D. K. Kallman
  • J. K. Millen

Organizations

  • MITRE Corporation

Tags

Communities of Interest

  • Human Systems
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Air Force Facilities
  • Computer Access Control
  • Computer Programming
  • Computers
  • Construction
  • Contracts
  • Language
  • Massachusetts
  • Mathematical Models
  • Procedures (Computers)
  • Programming Languages
  • Sequences
  • Systems Engineering
  • United States
  • Verification

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.