uberSpark is an innovative system architecture and programming principle for compositional verification of security properties of commodity (extensible) system software written in C and Assembly.
- 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) uberObjects (uObj)
- enforce uObj abstractions using a combination of commodity hardware mechanisms, light-weight static analysis and formal verification.
The primary sub-projects of uberSpark are: