> uberSpark (Modular Provable Security on Commodity Heterogeneous Interconnected Computing (CHIC) Platforms)

Overview

uberSpark Downloads and Services:

Download MPS (release v5.0)
Download uberObject (uobject) libraries (release v5.0)
Contact info@uberspark.org for uberSpark's uberObject (uobject) development services. We offer both software development services as well as system integration support to reinforce your existing safety-critical mission software stack with provably security.

Latest News:

January 5th, 2022: uberSpark 5.0 released, see release notes and changelog here
October 3rd, 2018: uberSpark 4.1 released, see release notes and changelog here

uberSpark (überSpark) is an innovative system architecture, software development kit and runtime framework for Modular Provable Security (MPS) on Commodity Heterogeneous Interconnected Computing (CHIC) platforms. uberSpark faciliates compositional verification of security properties on the CHIC software stack while supporting low-level programming languages such as C and Assembly. The salient features of uberSpark include:

provide a verifiable object abstraction called universal object abstractions or (überObject) uberObject or (üobject) uobject to endow low-level system software with abstractions found in higher-level languages (e.g., objects, interfaces, function-call semantics, serialization, access-control etc.)

facilitate easy refactoring of existing commodity (low-level) system software stacks into a collection of modular and composable uberObjects (uobject)

enforce üobject abstractions using a combination design time programming framework and verified runtime environment to anchor uobjects corresponding to secure application functionality by leveraging 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 Trusted Execution Environment (TEE) framework architected and verified using uberSpark, promoting the development of a new class of (verified) TEE anchored applications called (überApps) uberApps or (üApps) uApps which provide security sensitive functionality in the context of existing commodity OS and regular applications