Most real software systems consist of modules developed in multiple programming languages. Different languages differ in their security assumptions and guarantees. Consequently, even if single modules are secure in some language model and with respect to some security policy, there is usually no uniform security guarantee on a whole multilingual system. This project focuses on low-overhead techniques for providing security guarantees to software systems in which type-safe languages such as Java interoperate with native code. Native code is developed in low-level languages including C, C++, and assembly languages. Although often used in software projects, native code is notoriously insecure and is a rich source of security vulnerabilities. The PIs are developing a two-layered approach to alleviating security threats posed by native code to type-safe languages: (1) Binary rewriting tools and their verifiers are being incorporated into the Java Virtual Machine (JVM) for rewriting and verifying native modules at the machine-instruction level to enforce security policies; (2) A safe dialect of C for interoperation with Java is being designed; with the help of programmer annotations, the safety of programs in this dialect can be statically verified. The outcome of this project will enable popular platforms such as the JVM and .NET and other major programming languages (e.g., Python, OCaml, etc.) to incorporate native modules safely. The developed principles will also be applicable to web browsers and operating systems in which there is a need of extending them with untrusted low-level modules without comprising host security.
