Environment variables symbolic forking

[offlinemark]

Currently, when an analyzed program calls getenv(), Manticore executes this concretely, always returning a concrete pointer or NULL back to the application. If an application calls getenv and branches based on the return value (to check for NULL), we will always explore one path or the other, but never both, so there is an opportunity here to increase the coverage of an analysis. Manticore can instrument getenv, and possibly

• fork state, one which returns a NULL, another which returns some constant, predefined, concrete string (e.g. "1"). this may seem a little odd, but applications often use env variables as booleans and don't care about the contents, so this will allow us to explore both paths when the return value is checked for NULL. there are of course issues with this approach if the application actually does care about the contents of the env variable: the env variable will be malformed, and the application may reject it and simply error out.
• fork state, one which returns a NULL, another which returns a symbolic buffer. this more complete symbolic execution, and will cause exploration of the code that handles/parses the environment variable itself.

[ehennenfent]

https://github.com/trailofbits/manticore/wiki/Ideas