"Symbolic Exploit Assistant" ( SEA ) is a small tool designed to assist the discovery and construction of exploits in binary programs. SEA is free software (GPL3) and includes a minimal toolkit (BSD) to quickly develop binary analisys tools in Python.This project is developed in colaboration between the research institutes CIFASIS (Rosario, Argentina) and VERIMAG (Grenoble, France) in an effort to improve security in binary programs.
To get started, you should have Python 2.7 . To prepare the tool, the official Z3 Python binding (z3py) should be installed. Fortunately, just executing boostrap.sh will download and compile z3py.After it finishes compiling, SEA is ready to be used. You can test SEA analyzing the converted code of the first example of Gera's Insecure Programming:
The complete analysis of this example can be found here. Another interesting example to test detection of memory use is:
An explained analysis of it is here.