image placeholder

Google Research Award: Automated Verification of the Native Client

Prof. Bultan and Kruegel received a Google Research Award on Automated Verification of the Native Client. Native Client (NaCl) is a sandbox for untrusted x86 native code. The NaCl framework enables execution of x86 native code in web applications in order to achieve computational performance of native applications without compromising safety. The NaCl validator checks a set of constraints on NaCl binaries before executing them to guarantee their safety. The goal of this project is to use automated verification techniques to analyze the NaCl implementation in order to eliminate bugs, and to improve the confidence in the safety guarantees provided by the NaCl framework. The safety guarantees provided by the NaCl framework depend on 1) the correct implementation of the NaCl validator, and 2) the soundness of the validation algorithm used by the NaCl validator. In this project Prof. Bultan and Kruegel will use automated verification techniques to check both of these two conditions.

Google Research Award:
http://www.google.com/googleblogs/pdfs/google_researchawardsdec09.pdf