Welcome to überSpark’s documentation!

ü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.

This documentation describes the details on the software requirements and dependencies, build, verification and intallation of the core überSpark tools and libraries and CoSS

• Software Requirements and Dependencies
  • Development OS and Base Packages
  • Packages for Generating Documentation
  • OCaml Compiler and Base Packages
  • Coq Proof Assistant
  • CompCert Certified Compiler
  • Frama-C Verification Framework
• Building and Installing überSpark
  • Building überSpark Tools
  • Building überSpark Documentation
  • Installing überSpark
• Verifying, Building and Installing überSpark Libraries
  • Verifying überSpark Libraries
  • Building überSpark Libraries
  • Installing überSpark Libraries