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.
This project is sponsored by NSF's Trustworhty Computing and Programming Languages programs.