uberSpark

uberSpark (überSpark) is a system architecture, software development kit, and runtime framework for Modular Provable Security (MPS) on Commodity Heterogeneous Interconnected Computing (CHIC) platforms. It provides compositional verification of security properties on the CHIC software stack. The platform supports low-level programming languages, such as C and assembly. It facilitates refactoring of existing commodity system software stacks into a collection of modular and composable uber objects. The uberSpark project comprises multiple open-source licenses.

CHIC platforms include laptops, mobile phones, IoT devices, robots, drones, and self-driving cars. These platforms have use cases within critical applications (e.g., autonomous driving, home security, health care), and therefore require strong end-to-end guarantees for security, correctness, and timeliness. Formal verification can realize provable guarantees, but the complexity of CHIC software stacks makes verification tools and methodologies difficult. uberSpark system architecture aims to structure CHIC stacks around universal object abstractions, a fundamental system abstraction and building block, to help move towards practical and provable end-to-end guarantees.

uberSpark was created in 2016 by Amit Vasudevan, a computer scientist at the Software Engineering Institute (SEI), Carnegie Mellon University (CMU). v1.0 (the initial academic prototype release) was released on GitHub on October 14th, 2016. Vasudevan remains the principal force behind the design and development of uberSpark as well as über eXtensible Micro-Hypervisor Framework (uberXMHF)—an open-source, extensible, and formally verifiable micro-hypervisor framework, forming the foundation for a new class of (security-oriented) micro-hypervisor based applications (“uberApps”) on commodity computing platforms.

Salient features of uberSpark include the following:

• Providing a verifiable object abstraction known as universal object abstractions or shortened to uberObject (überObject) or uobject (üobject). These objects endow low-level system software with abstractions found in higher-level languages (e.g., objects, interfaces, function-call semantics, serialization, access-control, etc.)
• Facilitating easy refactoring of existing commodity (low-level) system software stacks into a collection of modular and composable uobjects.
• Enforcing uobject abstractions using a combination design time programming framework and verified runtime environment to anchor uobject corresponding to secure application functionality by leveraging commodity hardware mechanisms, lightweight static analysis, and formal verification.

The following are the main sub-projects of uberSpark:

The low-level verified runtime and hardware interface libraries along with a hardware model to interface to platform hardware during the verification of a uobject.

A commodity Trusted Execution Environment (TEE) framework built and verified using uberSpark, promoting the development of a new class of verified TEE anchored applications called uberApps (überApps) or uApps (üApps), which provide security-sensitive functionality in the context of existing commodity OS and regular applications.

On October 14th, 2016, the initial academic prototype (v1.0) of uberSpark was released. Two months later, on December 14th, 2016 v2.0 was released with a variety of updates:

• separate uberSpark, uberSpark libraries, and uberXMHF verification/build processes
• refined and streamlined uberSpark and uberXMHF verification/build harness
• fixed minor errors in documentation and updates to reflect release changes

v3.0 was released September 20th, 2017, adding support for Frama-C Phosphorus-20170501, and Compcert 3.0.1. v3.1 arrived in January 2018, fixing build errors for uberXMHF. The first standalone release of uberSpark (v4.0) became available on April 21st, 2018. An update (v4.1) came in October 2018, which included the following:

• adding libusmf to deal with JSON based manifest parsing
• migrating tools to use libusmf/JSON based manifest parsing
• adding foundation for standalone tool driver
• documentation consolidation

On January 6th, 2022, v5.0 was released and included these updates:

• moving to Ubuntu 16.04.x LTS VM/WSL development environment
• converting documentation to reST format
• fixing software dependency documentation
• migrating general-purpose uobject info-table and debug libraries into the core framework