System M: A Program Logic for Code Sandboxing and Identification

Abstract

Security-sensitive applications that execute untrusted code often check the codes integrity by comparing its syntax to a known good value or sandbox the code to contain its effects. System M is a new program logic for reasoning about such security-sensitive applications. System M extends Hoare Type Theory (HTT) to trace safety properties and, additionally, contains two new reasoning principles. First, its type system internalizes logical equality, facilitating reasoning about applications that check code integrity. Second, a confinement rule assigns an effect type to a computation based solely on knowledge of the computations sandbox. We prove the sound-ness of System M relative to a step-indexed trace-based semantic model. We illustrate both new reasoning principles of System M by verifying the main integrity property of the design of Memoir, a previously proposed trusted computing system for ensuring state continuity of isolated security-sensitive applications.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 22, 2014
Accession Number
AD1019582

Entities

People

  • Anupam Datta
  • Deepak Garg
  • Limin Jia
  • Shayak Sen

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Computations
  • Computer Access Control
  • Continuity
  • Guarantees
  • Identification
  • Intervals
  • Judgment
  • Language
  • Measurement
  • Operating Systems
  • Robotics
  • Security Protocols
  • Semantic Models
  • Specifications
  • Standards
  • Time Intervals
  • Web Browsers

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Cybersecurity.
  • Mathematical Modeling and Probability Theory.