Trace Effect Analysis for Software Security

Abstract

We developed combined run-time and compile-time analyses for enforcing trace based safety properties in higher order and Object Oriented programs, called trace effect analysis. Traces are the ordered sequence of events generated by programs. A wide variety of interesting language safety mechanisms can be expressed as trace properties, such as access control, resource usage protocols, and context sensitive flow analysis. Consequently, our analyses provide a uniform framework for automatically enforcing a large class of safety properties, which can be specialized for particular applications. Formal type theory underlies most of these analyses. We have also developed new program logics for defining access control policies. Based on temporal logics, they allow for the specification and verifiable enforcement of sophisticated security policies, and are especially useful in distributed contexts.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 28, 2010
Accession Number
ADA515457

Entities

People

  • Christian Skalka

Organizations

  • University of Vermont

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Christianity
  • Computer Access Control
  • Computer Programming
  • Computer Science
  • Computers
  • Cybersecurity
  • Department Of Defense
  • Embedded Systems
  • Information Operations
  • Language
  • Programming Languages
  • Risk Management
  • Security
  • Specifications
  • Standards
  • Students
  • Universities

Fields of Study

  • Computer science

Readers

  • Aviation Safety Risk Assessment.
  • Computational Linguistics
  • Parallel and Distributed Computing.