Mission

Building tools for the automated analysis of proprietary software systems

Vitaly Chipounov is building S2E, a platform for multi-path in-vivo analysis of complex software systems, at the Dependable Systems Laboratory, led by Prof. George Candea.
S2E empowers developers to build practical tools to enable applications like comprehensive performance profiling, reverse engineering of proprietary software, and bug finding for both kernel-mode and user-mode binaries. S2E is publicly available and has an active community of more than 150 users, including several research institutions.

S2E is a virtual machine augmented with symbolic execution. Users install and run any unmodified x86 software stack in S2E, including programs, libraries, the OS kernel, and drivers. Symbolic execution then automatically explores hundreds of thousands paths through the system, allowing users to check desired properties even in corner-case situations. Unlike existing analysis tools, S2E does not require to write code in special languages or model the environment.

With this platform, Vitaly developed a tool – RevNIC – that reverse-engineers proprietary closed-source device drivers to synthesize new, safer, and portable device drivers for different operating systems and architectures. RevNIC takes a binary device driver, explores it automatically across multiple paths to witness all the ways in which the driver communicates with the hardware, and synthesizes an equivalent driver that captures this interaction.



For more details, see Curriculum Vitae [PDF]