Approaching External Function Calls in OOX Symbolic Execution to WebAssembly using Function Summaries to combat Path Explosion

Abstract

After its creation in the 70s, symbolic execution has become a popular technique for verifying software with high confidence. This is an important technique to help prevent bugs in software. Bugs however, can have an enormous financial- or humanitarian impact, especially with the growing reliance on correct software. Symbolic execution however, is computationally expensive and has a high memory usage due to the so-called `Path Explosion'-problem. In recent years, at the Utrecht University, a novel symbolic execution engine has been developed to support an equally new Intermediate Verification Language called OOX. This thesis aims to extend the OOX ecosystem by adding the ability to call external functions. This will allow programs that rely on external libraries to be verified using the OOX ecosystem, which is a crucial feature for real-world applications. Calling these external functions allows the OOX ecosystem to break out of its isolation and interact with its environment. Furthermore, to mitigate the Path Explosion problem, we investigate the use of function summaries to reduce the number of paths that need to be explored when making calls to functions. This thesis provides an implementation for the interaction between OOX and WebAssembly and shows that function calls can be replaced with automated generation of function summaries. We evaluate the performance of the symbolic execution engine with and without generated function summaries. The results of this thesis provide a stepping stone for future research in the field of symbolic execution and software verification.