Symbolic analysis of assembly traces: Lessons learned and perspectives

In this study, we have developed a software to implement a symbolic analyzer for assembly traces. The software receives as input traces of assembly instructions. It then builds a symbolic expression characterizing the possible range of values for each variable and feeds this value to the Yices STM solver. The Yices solver returns possible concrete values that respect the symbolic expressions associated with each variable. This software has several potential applications including software testing and fuzzing and vulnerability detection. To verify the validity of our approach, we have tested our software with real-life traces and investigated its potential use for malware detection. For instance, that the software automatically detects the input values that would cause a buffer overflow in some cases. To conclude, we reflect on the lessons learned during the development of this software, which can help guide the future development of symbolic analyzers.