Automated Trust Analysis of Copland Specifications for Layered Attestations

Abstract

Copland is a declarative, domain-specific language for specifying complex layered attestations. How phrases are composed bears directly on the trustworthiness of the evidence they produce, and complex phrases become quite difficult to analyze by hand. We introduce an automated method for analyzing executions of attestations specified by Copland phrases in an adversarial setting. We develop a general theory of executions with adversarial corruption and repair events. Our approach is to enrich the Copland semantics according to this theory. Using the model finder Chase, we characterize all executions consistent with a set of initial assumptions. From this set of models, an analyst can discover all ways an active adversary can corrupt subcomponents without being detected by the attestation. These efforts afford trust policymakers the ability to compare attestations expressed as Copland phrases against trust policy in a way that encompasses both static and runtime concerns.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 06, 2021
Accession Number
AD1156891

Entities

People

  • Ian D. Kretz
  • John D. Ramsdell
  • Paul D. Rowe

Organizations

  • MITRE Corporation

Tags

Communities of Interest

  • Cyber
  • Engineered Resilient Systems

DTIC Thesaurus Topics

  • Abstracts
  • Anti-Virus Software
  • Computational Science
  • Computer Programming
  • Computer Programs
  • Computers
  • Computing Devices
  • Corporations
  • Detection
  • Geometric Forms
  • Governments
  • Language
  • Law
  • Malware
  • Motivation
  • Networks
  • Operating Systems
  • Pipelines
  • Resilience
  • Security
  • Sequences
  • Specifications
  • Standards
  • Topology
  • Web Browsers

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Cybersecurity.
  • Systems Analysis and Design