> uberSpark (Modular Provable Security on Commodity System Software Stacks)

Overview

Latest News:
  • February 26th, 2020: uberSpark 6.0.0 released, see release notes and changelog here
  • August 14th, 2019: uberSpark 5.0 released, see release notes and changelog here
  • October 3rd, 2018: uberSpark 4.1 released, see release notes and changelog here

uberSpark is an innovative system architecture and programming framework for modular provable security on commodity system software stacks. uberSpark faciliates compositional verification of security properties while supporting low-level programming languages such as C and Assembly. The salient features of uberSpark include:

  1. provide a verifiable object abstraction (called universal object abstractions or uberObject or uobject for short) 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 stacks into a collection of modular and composable uberObjects (üobject)
  3. enforce üobject 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
über 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