MultiOtter: Multiprocess Symbolic Execution
MultiOtter: Multiprocess Symbolic Execution
Loading...
Files
Publication or External Link
Date
2011-05-26
Authors
Turpie, Jonathan
Reisner, Elnatan
Foster, Jeffrey S.
Hicks, Michael
Advisor
Citation
DRUM DOI
Abstract
Symbolic execution can be an effective technique for exploring large
numbers of program paths, but it has generally been applied to programs
running in isolation, whose inputs are files or command-line arguments.
Programs that take inputs from other programs---servers, for
example---have been beyond the reach of symbolic execution. To address
this, we developed a multiprocess symbolic executor called MultiOtter,
along with an implementation of many of the POSIX functions, such as
socket and select, that interactive programs usually rely on. However,
that is just a first step. Next, we must determine what symbolic inputs
to feed to an interactive program to make multiprocess symbolic
execution effective. Providing completely unconstrained symbolic values
causes symbolic execution to spend too much time exploring uninteresting
paths, such as paths to handle invalid inputs. MultiOtter allows us to
generate inputs that conform to a context-free grammar, similar to
previous work, but it also enables new input generation capabilities
because we can now run arbitrary programs concurrently with the program
being studied. As examples, we symbolically executed a key-value store
server, redis, and an FTP server, vsftpd, each with a variety of inputs,
including symbolic versions of tests from redis's test suite and wget as
a client for vsftpd. We report the coverage provided by symbolic
execution with various forms of symbolic input, showing that different
testing goals require different degrees of symbolic inputs.