GEEC All the Way Down

Abstract

How do we formally verify security properties in today s malleable and evolving Commodity System Software (COSS) ecosystem? Recent advances in applying formal methods to systems software, e.g., IronClad [16] and seL4 [19], promise that this vision is not a fool s errand after all. In this position paper we explore the challenges involved in this problem, what research questions the state of the art leaves still open, and our proposal for the next step towards realizing this vision.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 13, 2015
Accession Number
ADA617284

Entities

People

  • Amit Vasudevan
  • Anupam Datta
  • Limin Jia
  • Petros Maniatis
  • Sagar Chaki

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Commodities
  • Computer Access Control
  • Computer Program Documentation
  • Computer Programming
  • Device Drivers
  • Firmware
  • Hypervisors
  • Instructions
  • Kernels (Operating System)
  • Language
  • Operating Systems
  • Platforms
  • Security
  • Software Development
  • System Software
  • Verification

Fields of Study

  • Computer science

Readers

  • Military History of the United States in the 20th Century.
  • Software Engineering.
  • Systems Analysis and Design