1600 Amphitheatre Parkway
Mountain View, CA 94043
I am a Software Engineer at Google, where I work on large-scale distributed symbolic execution and software security. My research interests span program analysis, operating systems, programming languages, and compilers. Here is my CV.
My previous work has focused on developing techniques and tools for scaling thorough program analysis to real-world systems. Given the size and complexity of such systems, program analysis achieves scalability by exploiting their modularity, i.e., analyzing different parts of the system in isolation. However, each part typically depends on the rest of the system—its environment—to achieve its task. My core results pertain to providing environment representations for accurate and efficient analysis of systems. To this end, I developed techniques for effective symbolic execution of systems interacting with the operating system (Cloud9) and of programs written in high-level dynamic languages (Chef).
Cloud9 is a symbolic execution platform for low-level system software, such as UNIX utilities, web servers, and distributed systems. Such systems rely on operating system calls to perform their job. To scalably support them in symbolic execution, Cloud9 introduces the idea of a symbolic operating system model that is split between a core set of primitives built into the engine and a full operating system interface emulated inside the symbolic runtime. Our approach requires as few as two primitives to support the POSIX interface: threads with synchronization and address spaces with shared memory.
Cloud9 parallelizes symbolic execution on large clusters of commodity hardware and was the first to demonstrate linear scalability on hundreds of nodes. Cloud9 is available at http://cloud9.epfl.ch.
To manage the complexity of symbolically executing the entire interpreter, Chef employs Class-Uniform Path Analysis (CUPA), an algorithm for prioritizing paths by grouping them into equivalence classes according to a coverage goal. Our Chef prototype generates up to 1000 times more tests in popular Python and Lua packages compared to a plain symbolic execution of the interpreters. Chef is available at http://dslab.epfl.ch/proj/chef/.
A more extensive summary of my work can be found in a (slightly outdated) research statement.
Prototyping Symbolic Execution Engines for Interpreted Languages
In International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Salt Lake City, UT, March 2014
Making Automated Testing of Cloud Applications an Integral Component of PaaS
In Asia-Pacific Workshop on Systems (APSYS), Singapore, July 2013
Efficient State Merging in Symbolic Execution
In Conference on Programming Language Design and Implementation (PLDI), Beijing, China, June 2012
Parallel Symbolic Execution for Automated Real-World Software Testing
In ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys), Salzburg, Austria, April 2011
Automated Software Testing as a Service
In ACM Symposium on Cloud Computing (SOCC), Indianapolis, IN, June 2010
Cloud9: A Software Testing Service
In ACM Operating Systems Review (OSR), Vol. 43, No. 4, December 2009