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:
- 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.)
- facilitate easy refactoring of existing commodity (low-level) system software stacks into a collection of modular and composable uberObjects (üobject)
- enforce üobject abstractions using a combination of commodity hardware mechanisms, light-weight static analysis and formal verification.
The primary sub-projects of uberSpark are: