[Pl-seminar] 10/6 Seminar: Koushik Sen, Concolic Testing: A Decade Later

[Daniel Patterson]

NUPRL Seminar presents

Koushik Sen
University of California, Berkeley

12:30--1:30pm
Thursday, Oct. 6 2016
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Concolic Testing: A Decade Later

Abstract:

Symbolic execution, which was introduced more than four decades ago,
is typically used in software testing to explore as many different
program paths as possible in a given amount of time, and for each path
to generate a set of concrete input values exercising it, and check
for the presence of various kinds of errors including assertion
violations, uncaught exceptions, security vulnerabilities, and memory
corruption.  A key limitation of classical symbolic execution is that
it cannot generate useful test inputs if the program under test uses
complex operations such as pointer manipulations and non-linear
arithmetic operations.

Our research on Concolic Testing (also known as DART: Directed
Automated Random Testing or Dynamic Symbolic Execution) alleviated the
limitations of classical symbolic execution by combining concrete
execution and symbolic execution.  We demonstrated that concolic
testing is an effective technique for generating high-coverage test
suites and for finding deep errors in complex software
applications. The success of concolic testing in scalably and
exhaustively testing real-world software was a major milestone in the
ad hoc world of software testing and has inspired the development of
several industrial and academic automated testing and security tools.

One of the key challenges of concolic testing is the huge number of
programs paths in all but the smallest programs, which is usually
exponential in the number of static branches in the code.  In this
talk I will describe MultiSE, a new technique for merging states
incrementally during symbolic execution, without using auxiliary
variables. The key idea of MultiSE is based on an alternative
representation of the state, where we map each variable, including the
program counter, to a set of guarded symbolic expressions called a
value summary. MultiSE has several advantages over conventional
symbolic execution and state merging techniques: 1) value summaries
enable sharing of symbolic expressions and path constraints along
multiple paths, 2) value-summaries avoid redundant execution, 3)
MultiSE does not introduce auxiliary symbolic values, which enables it
to make progress even when merging values not supported by the
constraint solver, such as floating point or function values.  We have
implemented MultiSE for JavaScript programs in a publicly available
open-source tool. Our evaluation of MultiSE on several programs shows
that MultiSE can run significantly faster than traditional symbolic
execution.


Bio:

Koushik Sen is an associate professor in the Department of Electrical
Engineering and Computer Sciences at the University of California,
Berkeley. His research interest lies in Software Engineering,
Programming Languages, and Formal methods. He is interested in
developing software tools and methodologies that improve programmer
productivity and software quality. He is best known for his work on
³DART: Directed Automated Random Testing² and concolic testing. He has
received a NSF CAREER Award in 2008, a Haifa Verification Conference
(HVC) Award in 2009, a IFIP TC2 Manfred Paul Award for Excellence in
Software: Theory and Practice in 2010, a Sloan Foundation Fellowship
in 2011, a Professor R. Narasimhan Lecture Award in 2014, and an Okawa
Foundation Research Grant in 2015. He has won several ACM SIGSOFT
Distinguished Paper Awards. He received the C.L. and Jane W-S. Liu
Award in 2004, the C. W. Gear Outstanding Graduate Award in 2005, and
the David J. Kuck Outstanding Ph.D. Thesis Award in 2007, and a
Distinguished Alumni Educator Award in 2014 from the UIUC Department
of Computer Science. He holds a B.Tech from Indian Institute of
Technology, Kanpur, and M.S. and Ph.D. in CS from University of
Illinois at Urbana-Champaign.
-------------- next part --------------
HTML attachment scrubbed and removed