Summary

In this chapter, you learned about some advanced reverse engineering topics; that is, symbolic execution, SMT solvers, and concolic execution.

You learned how to perform symbolic execution by writing some simple code using MIASM that symbolically executed a basic block of a hello world program. You also learned about the z3 theorem solver by performing two simple experiments.

Finally, you learned how to incorporate symbolic and concolic execution when using Ghidra by extending it with a plugin. You also learned how to convert from PCode into an LLVM intermediate representation, which can be useful for performing some advanced reverse engineering tasks.

I hope you enjoyed reading this book. You've learned a lot, but remember to put this knowledge to practice in order to develop your skills further. Binary protections are becoming more and more complex, so it is necessary to master advanced reverse engineering topics. Ghidra can be a good ally in this battle, so...