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.
New (8/20/2012): The project has an opening for a full-time postdoctoral position
- (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.
- (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 (Last updated: Jul 2012)
- 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. 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.
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.