Xenon Formal Security Policy Model

Abstract

Xenon is a high-assurance virtual machine monitor based on the Xen open-source hypervisor. We model the Xenon high-assurance virtual machine monitor's security policy as a conditional non-interference policy, using an event-based paradigm and the Communicating Sequential Processes (CSP) formalism. Our single model formally describes not only the separation of information flow but also the sharing. We also present our strategy for showing correspondence between this model and the Xenon interface.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 14, 2007
Accession Number
ADA471608

Entities

People

  • Bruce Montrose
  • James T Kirby
  • John Mcdermott
  • Myong Kang

Organizations

  • United States Naval Research Laboratory

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Alphabets
  • Boundaries
  • Communication Channels
  • Communities
  • Computer Access Control
  • Computer Programs
  • Computers
  • Construction
  • Demonstrations
  • Device Drivers
  • Hypervelocity Flow
  • Language
  • Military Research
  • Operating Systems
  • Security Protocols
  • Virtual Machines

Fields of Study

  • Computer science

Readers

  • Aerospace Propulsion Engineering.
  • East Asian Political and Security Studies within the Soviet Union
  • Parallel and Distributed Computing.