Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Home
  • Attend
    • Registration Information
    • Registration Discounts
    • Venue, Hotel, and Travel
    • Students and Grants
    • Co-located Workshops
  • Program
    • At a Glance
    • Technical Sessions
  • Activities
    • Birds-of-a-Feather Sessions
    • Poster Session
    • Work-in-Progress Reports (WiPs)
  • Sponsorship
  • Participate
    • Instructions for Authors and Speakers
    • Call for Papers
      • Important Dates
      • Symposium Organizers
      • Symposium Topics
      • Refereed Papers
      • Symposium Activities
      • Submitting Papers
  • About
    • Symposium Organizers
    • Questions
    • Services
    • Help Promote
    • Past Symposia
  • Home
  • Attend
  • Program
  • Activities
  • Sponsorship
  • Participate
  • About

sponsors

Platinum Sponsor
Gold Sponsor
Silver Sponsor
Silver Sponsor
Silver Sponsor
Silver Sponsor
Bronze Sponsor
Bronze Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Industry Partner
Industry Partner

help promote

USENIX Security '16 button

Get more
Help Promote graphics!

connect with usenix


  •  Twitter
  •  Facebook
  •  LinkedIn
  •  Google+
  •  YouTube

twitter

Tweets by USENIXSecurity

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home » überSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor
Tweet

connect with us

überSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor

Authors: 

Amit Vasudevan and Sagar Chaki, Carnegie Mellon University; Petros Maniatis, Google Inc.; Limin Jia and Anupam Datta, Carnegie Mellon University

Abstract: 

We present überSpark (üSpark), an innovative architecture for compositional verification of security properties of extensible hypervisors written in C and Assembly. üSpark comprises two key ideas: (i) endowing low-level system software with abstractions found in higher-level languages (e.g., objects, interfaces, function-call semantics for implementations of interfaces, access control on interfaces, concurrency and serialization), enforced using a combination of commodity hardware mechanisms and lightweight static analysis; and (ii) interfacing with platform hardware by programming in Assembly using an idiomatic style (called CASM) that is verifiable via tools aimed at C, while retaining its performance and low-level access to hardware. After verification, the C code is compiled using a certified compiler while the CASM code is translated into its corresponding Assembly instructions. Collectively, these innovations enable compositional verification of security invariants without sacrificing performance. We validate üSpark by building and verifying security invariants of an existing open-source commodity x86 micro-hypervisor and several of its extensions, and demonstrating only minor performance overhead with low verification costs.

Amit Vasudevan, Carnegie Mellon University

Sagar Chaki, Carnegie Mellon University

Petros Maniatis, Google Inc.

Limin Jia, Carnegie Mellon University

Anupam Datta, Carnegie Mellon University

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {197173,
author = {Amit Vasudevan and Sagar Chaki and Petros Maniatis and Limin Jia and Anupam Datta},
title = {{{\"u}berSpark}: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor},
booktitle = {25th USENIX Security Symposium (USENIX Security 16)},
year = {2016},
isbn = {978-1-931971-32-4},
address = {Austin, TX},
pages = {87--104},
url = {https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/vasudevan},
publisher = {USENIX Association},
month = aug,
}
Download
Vasudevan PDF
View the slides

Presentation Video 

Presentation Audio

MP3 Download

Download Audio

  • Log in or    Register to post comments

Platinum Sponsors

Gold Sponsors

Silver Sponsors

Bronze Sponsors

Media Sponsors & Industry Partners

© USENIX

  • Privacy Policy
  • Contact Us