Parallel symbolic execution for automated real-world software testing

TLDR

This paper introduces Cloud9, a platform that scales symbolic execution across commodity clusters to automate testing of real‑world software. Cloud9 offers a systematic interface for writing symbolic tests, supports POSIX features for single‑, multi‑, and distributed programs, and can generate new tests from existing suites while diagnosing incomplete bug fixes by comparing buggy paths. Experiments demonstrate that Cloud9 automatically tests real systems such as memcached, Apache httpd, lighttpd, Python, rsync, and curl, and can diagnose incomplete bug fixes by comparing buggy paths before and after patches.

Abstract

This paper introduces Cloud9, a platform for automated testing of real-world software. Our main contribution is the scalable parallelization of symbolic execution on clusters of commodity hardware, to help cope with path explosion. Cloud9 provides a systematic interface for writing "symbolic tests" that concisely specify entire families of inputs and behaviors to be tested, thus improving testing productivity. Cloud9 can handle not only single-threaded programs but also multi-threaded and distributed systems. It includes a new symbolic environment model that is the first to support all major aspects of the POSIX interface, such as processes, threads, synchronization, networking, IPC, and file I/O. We show that Cloud9 can automatically test real systems, like memcached, Apache httpd, lighttpd, the Python interpreter, rsync, and curl. We show how Cloud9 can use existing test suites to generate new test cases that capture untested corner cases (e.g., network stream fragmentation). Cloud9 can also diagnose incomplete bug fixes by analyzing the difference between buggy paths before and after a patch.