Overview
The goal of the GoNative research project is to enable safe execution of native code in type-safe programming languages such as Java, Python, and C#.
We are exploring sandboxing techniques (e.g., Software-based Fault Isolation) to constrain native code so that its execution won't affect the safety of type-safe languages. 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
- (1/17/2012) We are glad to release the source code of RockSalt 1.0 under the GPL license. [rocksalt.tar.gz]. RockSalt is a new machine-code verifier for Google's Native Client, with a formal correctness proof mechanized in Coq. This is a joint work by Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, and Edward Gan.
- (11/13/2011) We are glad to release the source code of Robusta 1.0 under the BSD license. [robusta.tar.gz]
Results (Last updated: Jul 2011)
- 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. Please see a conference paper for more details. Please see above for the code release of Robusta 1.0.
- 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 Trustworthy Computing and Programming Languages programs and a research award from Google Research.
