uberSpark: Composable Verification of Commodity System Software
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.
uberSpark has been used to build and verify security invariants of the uber eXtensible Micro-Hypervisor Framework (http://uberxmhf.org) and several of its extensions, and demonstrating only minor performance overhead with low verification costs.
Visit: http://uberspark.org for more information on how to download, build, install, contribute and get involved.
The formatted documentation can be read online at: http://uberspark.org/docs/toc.html
Documentation sources are within
Contact and Maintainer
Amit Vasudevan (http://hypcode.org)
The uberSpark project comprises multiple open source licenses. See COPYING.md for details.