Overview

The goal of the GoNative research project is to enable safe execution of native code in software systems such as web browsers and type-safe programming languages (e.g., Java, Python, C#).

We are exploring sandboxing techniques (e.g., Software-based Fault Isolation and Control-Flow Integrity) to constrain native code so that its execution won't affect the safety of software systems. We are also designing new programming languages for writing safe glue code between native code and type-safe languages.

Verifiable guarantees are what we strive for. We are leveraging formal methods to verify the security guarantees provided by our techniques.

Code Release

  • (12/15/2014) The RockSalt repository has moved to GitHub. The latest version can be found at here.
  • (2/26/2013) We are glad to release the source code of the second version of Robusta (now dubbed Arabica) under the BSD license. [arabica.tar.gz]
  • (1/17/2012) We are glad to release the source code of RockSalt 1.0 under the GPL license. [rocksalt.tar.gz]. Harvard's press release about RockSalt. Note: this version is outdated; see above for a new version.
  • (11/13/2011) We are glad to release the source code of Robusta 1.0 under the BSD license. (note: replaced by a newer version; see above)

Results

  • RockSalt is a new machine-code verifier for Google's Native Client, with a formal correctness proof mechanized in Coq. RockSalt's proofs are respect to an x86 model, which can be used for other applications. Please see a conference paper for more details. Please see above for the code release of RockSalt.
  • Robusta is a framework that allows JVM administrators to constrain native code with different trust levels, similar to how the security of Java code is configured. Arabica is a newer version that supports JVM-portable sandboxing of native code. Two conference papers (Robusta, Arabica) describe the implementation details. Please see above for the code release of Arabica.
  • JNIL is the first formal semantics for the core Java Native Interface (JNI); the semantics can directly serve as a formal basis for JNI tools and systems. Please see a conference paper for more details.
  • We have implemented in LLVM a system that provides highly efficient sandboxing of memory reads and writes through the combination of control-flow integrity and static analysis. Please see this paper for more details.

Sponsors

This project is sponsored by NSF's Secure and Trustworthy Cyberspace, Trustworthy Computing, and Programming Languages programs. It is also supproted by Google Research through its Faculty Research Award program.

NSF Logo                         Google Logo