sandshrew is a prototype concolic unit testing tool for cryptographic verification. It harnesses the Manticore API in order to perform unconstrained concolic execution on C cryptographic primitives.
Classical symbolic execution is generally not feasible when analyzing crypto, due to the presence of complex symbolic expressions. sandshrew fixes this problem and ensures functional correctness by concretizing (or, "emulating") the execution of specified cryptographic primitives, avoiding complex SMT queries and creating a speedup in the analysis.
- Automatic testcase generation for analysis
- Easy interface for writing unit test cases
- Integration into development workflows (imagine formal verification for unit testing)
- 300 LOCs
$ git clone https://github.com/trailofbits/sandshrew && cd sandshrew/
$ python setup.py install
To hack and develop on sandshrew, it is recommended to utilize a Python virtualenv.
The simplest example is the hash collision example in test_openssl_md5.c:
$ cd examples/
$ make all && cd ..
$ sandshrew -t examples/test_openssl_md5 --debug
Drop by the wiki for more information about getting started and writing test cases.
sandshrew is currently experimental, and has not been extensively tested for larger test cases.
sandshrew is licensed and distributed under the MIT license