Symbolic Execution for Directed Search and Specification Inference

Speaker:        Prof. Abhik Roychoudhury
                National University of Singapore

Title:          "Symbolic Execution for Directed Search and Specification
                 Inference"

Date:           Thursday, 7 March 2019

Time:           3:00pm - 4:00pm

Venue:          Room 4472 (via lift 25/26), HKUST

Abstract:

Symbolic analysis of programs have been first studied for the purpose of
program verification. In recent decades, symbolic execution technology has
witnessed renewed interest due to the maturity of Satisfiability Modulo
Theory (SMT) solvers. Powerful dynamic analysis tools have leveraged the
back-end solvers to systematically navigate large search spaces leading to
application of symbolic analysis in test generation. In this talk, we will
first study the power of state-of-the-art symbolic execution based
approaches, mostly built on KLEE, for various security vulnerability
analysis tasks such as finding zero-day vulnerabilities and crash
reproduction. We compare the symbolic analysis approaches to grey-box fuzz
testing approaches (which are routinely employed in industrial settings).
Through such comparison, we can try to understand the state-of-practice of
symbolic execution in terms of its ability to detect software
vulnerabilities. In the later part of the talk, we will conceptualize the
use of symbolic execution approaches/tools for purposes beyond guiding
search. We will sketch the usage of symbolic execution in inferring
specification of intended program behavior. This is done by analyzing a
buggy program against selected tests. Such specification inference
capability can be combined with program synthesis techniques to
automatically repair programs. Automated program repair via symbolic
execution goes beyond search-based approaches which lift patches from
elsewhere in the program. Such an approach can construct "imaginative"
patches, serves as a test-bed for the grand-challenge of automated
programming, and contributes to the vision of self-healing software.


*****************
Biography:

Abhik Roychoudhury is a Professor of Computer Science at National
University of Singapore. His research focuses on software testing and
analysis, software security and trust-worthy software construction. His
research group has built scalable techniques for testing, debugging and
repair of programs using systematic semantic analysis. He has been an
ACM Distinguished Speaker (2013-19). He is currently leading a large
five-year long targeted research effort funded by National Research
Foundation in the domain of trust-worthy software. He is the Lead
Principal Investigator of the Singapore Cyber-security Consortium, which
is a consortium of over 30 companies in the cyber-security space engaging
with academia for research and collaboration. He has served as Program
Chair of ACM International Symposium on Software Testing and Analysis
(ISSTA) 2016 and Editorial Board member of IEEE Transactions on Software
Engineering (TSE) during 2014-18. Abhik received his Ph.D. in Computer
Science from the State University of New York at Stony Brook in 2000. He
has advised organizations and governments on cyber-security issues in
different capacities, including being an advisory board member of the
London Office for Rapid Cyber-security Advancement (LORCA) since 2018.