Griffin Prechter

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2021-261

December 17, 2021

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-261.pdf

Symbolic execution is a popular dynamic program analysis technique in which a program is executed with symbolic, or variable, inputs in place of concrete ones. During the execution of a program, multiple paths may be explored due to the presence of symbolic values, producing several states. These states are guarded by path constraints, conditions that indicate what values the symbolic inputs should take on to produce a given state. Symbolic execution has many applications ranging from testing and bug discovery to program analysis and verification. Recently, leveraging domain specific knowledge, modified symbolic execution algorithms have been utilized to solve computer security problems through program analysis. One example, ObliCheck, implements novel symbolic execution techniques to efficiently verify the obliviousness of algorithms modeled in a subset of JavaScript. In this report, I identify two key challenges in implementing custom symbolic execution algorithms: First, features in modern languages are often difficult to support in symbolic execution frameworks due to the constraints imposed by underlying SMT solvers. Second, it is challenging and time consuming to modify existing symbolic execution frameworks to rapidly prototype custom symbolic execution algorithms. To address these challenges, I present YouVerify, an intermediate representation (IR) for symbolic execution built as an abstraction layer directly above the SMT-Lib family of solvers. YouVerify provides a flexible API that separates the state representation and exploration from the IR language and symbolic interpreter. I provide a verified implementation of the framework with a default symbolic execution algorithm. I additionally provide a prototype implementation of ObliCheck's symbolic execution algorithm modifications to demonstrate YouVerify's effectiveness for prototyping symbolic execution techniques.

Advisors: Koushik Sen and Raluca Ada Popa

---

BibTeX citation:

@mastersthesis{Prechter:EECS-2021-261,
    Author= {Prechter, Griffin},
    Title= {YouVerify: An Intermediate Representation and Framework for Symbolic Execution},
    School= {EECS Department, University of California, Berkeley},
    Year= {2021},
    Month= {Dec},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-261.html},
    Number= {UCB/EECS-2021-261},
    Abstract= {Symbolic execution is a popular dynamic program analysis technique in which a program is executed with symbolic, or variable, inputs in place of concrete ones. During the execution of a program, multiple paths may be explored due to the presence of symbolic values, producing several states. These states are guarded by path constraints, conditions that indicate what values the symbolic inputs should take on to produce a given state. Symbolic execution has many applications ranging from testing and bug discovery to program analysis and verification. Recently, leveraging domain specific knowledge, modified symbolic execution algorithms have been utilized to solve computer security problems through program analysis. One example, ObliCheck, implements novel symbolic execution techniques to efficiently verify the obliviousness of algorithms modeled in a subset of JavaScript. In this report, I identify two key challenges in implementing custom symbolic execution algorithms: First, features in modern languages are often difficult to support in symbolic execution frameworks due to the constraints imposed by underlying SMT solvers. Second, it is challenging and time consuming to modify existing symbolic execution frameworks to rapidly prototype custom symbolic execution algorithms. To address these challenges, I present YouVerify, an intermediate representation (IR) for symbolic execution built as an abstraction layer directly above the SMT-Lib family of solvers. YouVerify provides a flexible API that separates the state representation and exploration from the IR language and symbolic interpreter. I provide a verified implementation of the framework with a default symbolic execution algorithm. I additionally provide a prototype implementation of ObliCheck's symbolic execution algorithm modifications to demonstrate YouVerify's effectiveness for prototyping symbolic execution techniques.},
}

EndNote citation:

%0 Thesis
%A Prechter, Griffin 
%T YouVerify: An Intermediate Representation and Framework for Symbolic Execution
%I EECS Department, University of California, Berkeley
%D 2021
%8 December 17
%@ UCB/EECS-2021-261
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-261.html
%F Prechter:EECS-2021-261