Benchmarks
The memory model of SENinja can be valuable for reasoning on symbolic memory accesses. This can be useful, e.g., to invert a CRC32 when the implementation of the checksum uses a hash-table.
You can find a CRC32 benchmark in this repository: https://github.com/borzacchiello/crc32-sym.
The program takes as input (first command-line argument) the size s of a buffer. Then, it computes the CRC32 of two buffers of size s: a randomly generated one, and a one whose content is read from stdin. Finally, it checks whether the CRC32 of the two buffers is equal.
The benchmark can be useful to assess how much time SENinja takes to invert the check, thus generating a buffer with the same CRC32 with respect to the buffer generated randomly. Note that, due to the implementation of the CRC32, the symbolic engine must handle correctly symbolic memory accesses (no concretization).
To analyze the benchmark in SENinja using the GUI, you can:
- load the binary in BinaryNinja
- start the exploration at the first instruction of
main(0x4006c0) - setup a concrete command line input (
tools/SENinja/Setup argv...) with the desired size of the buffer (e.g., 64) - run the exploration until a fork (right-click,
plugins/SENinja/Run/Continue until branch) - select the state at
0x40069d(right-click,plugins/SENinja/change current state) - evaluate stdin in the current state (using the python console):
>>> import seninja
>>> s = seninja.get_current_state()
>>> s.solver.evaluate(seninja.get_stdin_bv(s))Alternatively, in the benchmark repository, there is a script that automatize these steps (you can use this plugin to load the script in the GUI).
The benchmarks repository holds some scripts to run both KLEE and angr on the same benchmark (more info in the repository itself).
The following chart summarizes the running time of SENinja with respect to both KLEE and angr (the cross indicates that the experiment did not terminate within the 1h timeout):
For more examples that show how to use the tool, look at this section of the wiki.