I started implementing a new feature called semantic search in ropper several month ago. Due to lack of time it is not finished yet. My lovely Kids, a job and my studies are comsuming a lot of time. :-) Nevertheless I want to give a little introduction into the semantic search implementation in ropper and how it can be used. It works for almost all architectures which are supported by ropper. Currently it is not working for ARM/ARMTHUMB, but I am working on it.
What does semantic search mean?
Almost all rop gadget finders offers a syntactic search. The user gives an input which describes the gadget and the gadget finder goes through the list of found gadgets and match each gadget with the given input. Mostly the user input is a kind of regular expression which is used on the gadget string. If an user want to look for gadgets which set eax to 0, he or she has can search for several instructions, e. g.:
- xor eax, eax
- mov eax, 0
- sub eax, eax
- and some more
If the user cannot find any gadget containing one of those instructions, he or she has to think about other possibilities to set eax to 0.
Semantic search should help here. The does not need to describe the gadget he or she is looking for syntactically, instead he or she describes what the gadget should mean semantically. So only the information that eax needs to be 0 is needed and the gadget finder looks for all gadgets which set eax to 0.
This is just a short description. I will describe it more detailed when the implementation is done. Since a lot assembly instructions have side effects, ropper translates each gadget into an intermediate representation of it. Ropper makes use of this intermediate representation to generate expressions and build formular for a SMT solver. Ropper uses a SMT solver to check if the formular satisfies the constraint given by the user. Ropper makes use of pyvex to create intermediate representation and z3 as SMT solver.
How to use it
Since the analysis of the gadgets for the semantic search takes much time and until now ropper does not save the result of the analysis, I recommend to use the interactive sh of ropper. As long as ropper is running the analysis has to be done only once. To start the interactive sh use the following command:
- register=number (e. g. eax=0)
- register=register (e. g. eax=ebx)
- register=[register] (e. r. eax=[ebx])
- register+=number or register (e. g. eax+=1, eax+=ebx)
- register-=number or register (e. g. eax+=1, eax-=ebx)
- register*=number or register (e. g. eax*=1, eax*=ebx)
- register/=number or register (e. g. eax+=1, eax/=ebx)
It is possible to set a couple of contraints seperated by a semicolon.
Using the command above, ropper searchs for gadgets which sets eax and ebx to 0. Furthermore it is possible to set registers which should not be modified by the gadget. The following command shows how to set eax to 0 and to not modify esi:
ropper only prints the first five found gadgets. You can change the settings if you want to print more:
When you set count_of_findings to 0, ropper prints all gadgets.
The feature is only available in dev branch yet. Since pyvex is only available for python2, the semantic search feature is only working with python2. To make it easier to use ropper with python 2 if it is installed, you can use the command ropper2. This command makes use of python2 instead of the default python version that is installed on the system.
Installation of pyvex
To install z3 and z3py please follow the instructions on the github page https://github.com/Z3Prover/z3.
Bugs / Improvements
If you find bugs or if you have ideas for improvements, please report them on github or contact me (sashs at <the domain of this blogpost>)