Alloy Experiments for a Least Privilege Separation Kernel

Abstract

A least privilege separation kernel (LPSK) is part of a long-term project known as the Trusted Computing Exemplar (TCX). A major objective of the TCX is the creation of an open framework for high assurance development. A relatively new specification tool called Alloy has shown potential for high assurance development. We implemented the formal security policy model (FSPM) and the formal top level specification (FTLS) of the TCX LPSK in Alloy and concluded that Alloy has few limitations and is more than sufficiently useful, as measured by utility and ease of use, to include in the TCX framework.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 2007
Accession Number
ADA473428

Entities

People

  • David A. Phelps

Organizations

  • Naval Postgraduate School

Tags

Communities of Interest

  • Biomedical
  • Cyber

DTIC Thesaurus Topics

  • California
  • Computer Programming
  • Computer Science
  • Computers
  • Cybersecurity
  • Formal Languages
  • Information Processing
  • Language
  • Nomenclature
  • Object Oriented Programming
  • Operating Systems
  • Programming Languages
  • Security
  • Software Development
  • Specifications
  • Standards
  • Students

Readers

  • Neural Network Machine Learning.
  • Neurotrauma and Rehabilitation Medicine.
  • Software Engineering.