A Security Domain Model to Assess Software for Exploitable Covert Channels

Abstract

Covert channels can result in unauthorized information flows when exploited by malicious software. To address this problem, we present a precise, formal definition for covert channels, which relies on control flow dependency tracing through program execution, and extends Dennings' and subsequent classic work in secure information flow. A formal security Domain Model (DM) for conducting static analysis of programs to identify covert channel vulnerabilities is described. The DM is comprised of an Invariant Model, which defines the generic concepts of program state, information flow, and covert channel rules; and an Implementation Model, which specifies the behavior of a target program. The DM is compiled from a representation of the program, written in a domain-specific Implementation Modeling Language (IML), and a specification of the security policy written in Alloy. The Alloy Analyzer tool is used to perform static analysis of the DM to automatically detect potential covert channel vulnerabilities and security policy violations in the target program.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 2008
Accession Number
ADA484406

Entities

People

  • Alan B. Shaffer
  • Cynthia E. Irvine
  • Mikhail I. Auguston
  • Timothy E. Levin

Organizations

  • Naval Postgraduate School

Tags

DTIC Thesaurus Topics

  • Analyzers
  • Computer Access Control
  • Computer Languages
  • Computer Programming
  • Computer Science
  • Computers
  • Cybersecurity
  • High Level Languages
  • Information Processing
  • Information Systems
  • Language
  • Operating Systems
  • Programming Languages
  • Security
  • Specifications
  • Standards
  • Vulnerability

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Cybersecurity.
  • Fluid Dynamics.