Symvex : A Symbolic Execution System for Machine Code

• Main Author: Rönn, Mattias
• Format: Others
• Language: English
• Published: Linköpings universitet, Databas och informationsteknik 2016
• Subjects: symbolic execution; concolic execution; testing
• Online Access: http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-124181

This thesis is a part of an ongoing research project at Link ̈oping University. The goal of the thesis work is to design and implement a prototype for a symbolic execution system that scales well with larger programs and is capable of performing symbolic execution on machine code. For this reason we have analyzed the current state of symbolic executors that are able to perform symbolic execution on machine code to see if we could use that implementation as base for our prototype. We wanted to know if any of the existing systems scaled well with large software. We found that neither of the existing systems worked well with the real life software in our evaluation. Furthermore, even if it would have been possible to fix one of the existing systems, the time required to figure out the faults in their implementation would most likely have been too great. For this reason we decided to create an implementation of our own from scratch. However, we did note that some approaches in the existing systems seemed to work better with large software. Specifically saving as little state as possible about the program seemed favorable. Armed with the knowledge gained from the analysis, we managed to implement a system that compared quite well with the existing systems. Our system was able to execute all the real-life programs used in our tests, but unfortunately had some issues with high memory usage for certain programs. In order to lessen the problem with high memory usage, we present and discuss several potential ways to mitigate this issue.