> uberSpark (Composable Verification of Commodity System Software)

Overview

Latest News:
  • October 3rd, 2018: uberSpark 4.1 released, see release notes and changelog here
  • April 20th, 2018: uberSpark 4.0 released, see release notes and changelog here

uberSpark is an innovative system architecture and programming principle for compositional verification of security properties of commodity (extensible) system software written in C and Assembly.

  1. provide a verifiable object abstraction (uberObject) to endow low-level system software with abstractions found in higher-level languages (e.g., objects, interfaces, function-call semantics, serialization, access-control etc.)
  2. facilitate easy refactoring of existing commodity (low-level) system software stack into a collection of (composable) uberObjects (uObj)
  3. enforce uObj abstractions using a combination of commodity hardware mechanisms, light-weight static analysis and formal verification.

The primary sub-projects of uberSpark are:

uberSpark core libraries and hardware model
The low-level verified runtime and hardware interface libraries along with a hardware model to interface to platform hardware during verification of a uobject
uber eXtensible Micro-Hypervisor Framework (uberXMHF)
A commodity micro-hypervisor framework architected and verified using uberSpark, promoting the development of a new class of (verified) micro-hypervisor based applications ("uberApps") which provide security sensitive functionality in the context of existing commodity OS and regular applications