überSpark Next-generation

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

The salient features of überSpark include:

• 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.)
• facilitate easy refactoring of existing commodity (low-level) system software stack into a collection of (composable) üobjects
• enforce üobject abstractions using a combination of commodity hardware mechanisms, light-weight static analysis and formal verification.
• provide runtime local and remote attestation mechanisms to ascertain the load and execution of üobject collections on a given platform

Note

überSpark next-generation toolkit is currently in alpha stage and experimental. It aims to enable stand-alone üobject build, integration into CoSS code-base, verification and runtime attestation mechanisms. The next-generation toolkit is under active development and at some point in the near future, will replace the existing toolkit.

Note

The next-generation toollkit documentation currently comprises of three overarching guides: the General User’s Guide, the CoSS Developer’s Guide, and the Contributor’s Guide.