SyMIPS is a Dynamic Symbolic Execution(DSE) tool for MIPS. It is based on Corana as a DSE tool for ARM. Until now, it supports running DSE on MIPS32 instruction set under the presence of indirect jump. Because it is a preliminary version and are improving, it still has potential bugs.
Note: Currently, this version is for Linux only.
First, you need to install Java 1.8 or later since SyMIPS has been written in Java.
Capstone is a well-known disassembler framework that support various platforms. SyMIPS uses it to disassemble a single-step instruction.
- Cloning Capstone: https://github.com/aquynh/capstone
- Building:
cd capstone; ./make.sh; sudo ./make.sh install
Z3 is a theorem solver developed by Microsoft Research. SyMIPS uses Z3 as a SMT solver for checking the satisfiability of path constraints.
- Installing by command line:
sudo apt-get update -y; sudo apt-get install -y z3 - From source code: Go to https://github.com/Z3Prover/z3 and follows its instructions.
readelf is a linux package for reading the format of binary files.
- Installing by command line:
sudo apt-get update -y; sudo apt-get install readelf
You can use a jar file SyMIPS or rebuild it from source code.
java -Xss512m -Xmx3048m -jar SyMIPS.jar /full_path/to/input/file
This project is licensed under the MIT License.
I want to thank Mr. Vu Viet Anh for his support. SyMIPS also uses Java Parsing Library to read binary format.