Using Ghidra for advanced reverse engineering
Ghidra has an intermediate language known as PCode. It makes Ghidra powerful because it is suitable for applying these kinds of techniques. As we mentioned in Chapter 9, Scripting Binary Audits, in the PCode versus assembly language section, the reason why PCode is more suitable for symbolic execution is because it offers more granularity than assembly. In fact, the side effects that take place in the assembly language, such as flag registers being modified during the execution of an instruction, doesn't happen in PCode because they are split into many instructions. This aspect of intermediate representations simplifies the task of creating and maintaining SMT formulas.
In the next section, you will learn how to extend Ghidra with Angr, a powerful binary analysis framework for implementing symbolic execution.
Adding symbolic execution capabilities to Ghidra with AngryGhidra
When looking for ways to perform symbolic execution...