Solidifying and Scaling SMT-based Program Analysis

PhD Thesis Proposal Defence


Title: "Solidifying and Scaling SMT-based Program Analysis"

by

Mr. Peisen YAO


Abstract:

Software bugs such as program crashes and security vulnerabilities are 
still a widespread plague. Program analysis is a technique for inferring a 
program's possible behavior and detect common software bugs. Over the past 
two decades, Satisfiability Modulo Theories (SMT) solvers have served as 
the core engine of many program analysis techniques, such as symbolic 
execution. Although there have been many success stories of SMT-based 
program analysis, we still observe the difficulty in applying them at an 
industrial scale. Among other reasons, reliability and scalability are two 
key obstacles to adoption. To improve the reliability and scalability of 
SMT-based program analysis, this thesis makes two major contributions by 
exploring the use of abstraction.

The first work advances the automated testing of SMT solvers, which are 
crucial for the reliability of SMT-based program analysis. Due to the test 
oracle problem, existing approaches to testing SMT solvers are either too 
costly or find difficulties generalizing to different solvers and 
theories. To complement existing approaches and overcome their weaknesses, 
we introduce two new general techniques: (1) a general, logical 
approximation-based metamorphic relation and (2) skeletal approximation 
enumeration, a lightweight methodology for approximating formulas. Our 
approach had found 71 confirmed bugs in Z3 and CVC4, two widely-used and 
comprehensively tested SMT solvers.

The second work improves the scalability of symbolic abstraction, a 
specific class of SMT-based program analysis. Symbolic abstraction is an 
important point in the space of abstract interpretation, as it allows for 
automatically synthesizing the most precise abstract transformers. 
However, current techniques have difficulty delivering on their practical 
strengths due to performance issues. We introduce two algorithms that 
apply to the bit-vector interval domain and a certain kind of polyhedral 
domain, respectively. Our algorithms substantially speed up existing 
techniques and bring significant precision advantages to two program 
analysis clients. Our work presents strong evidence that symbolic 
abstraction of numeric domains can be efficient and practical for large 
and realistic programs.


Date:			Thursday, 7 October 2021

Time:                  	11:00am - 1:00pm

Zoom Meeting: 
https://hkust.zoom.us/j/97396221286?pwd=QWhxR295TVZWMVJ3UURTc2tyRmZYUT09

Committee Members:	Dr. Charles Zhang (Supervisor)
 			Dr. Amir Goharshady (Chairperson)
 			Prof. Shing-Chi Cheung
 			Prof. Fangzhen Lin
 			Dr. Shuai Wang


**** ALL are Welcome ****