Debile uses sbuild for building packages. As mentioned before, my setup for analyzing Debian source packages with KLEE assumed pbuilder. Therefore, i’ve been moving to sbuild for symbolic execution via KLEE on Debian packages.
One of obstacles I had this week had to do with using schroot in Python, namely in Debile, which is written in Python. Paul Tagliamonte, a Debian developer, who contributed to Debile, also created a Python library schroot (which is packaged in Debian), for working with schroot. I looked at implementations of Debile runners of other analysis tools already supported in Debile that used schroot. It seemed pretty straightforward and I thought it would be very easy to do the same for KLEE. However, it wasn’t.
I wanted to set up an schroot session by using the usual command line piping, passed as a command to be executed within the session. I also wanted to change directory followed by a command. The implementation of executing commands in a Python schroot (the run function) is such that it boils down to using Python subprocess’s Popen with the shell argument set to false, which means no piping and no and-ing commands (the
&& operator). It took me some time to track this down.
To make my life easier, I created a helper function to run a sequence of commands and break out of the sequence as soon as a command from the sequence return a non-zero value:
The function turned out to be very handy.
A next obstacle that I thought wouldn’t be there was with using for expressions to build lists. A problem I ran into is building a list of strings representing a command to be run and its arguments using for expressions. I wanted to have something like:
but that didn’t work when part of another list. So I reverted to plain old for loops and modifying a big list in-place, which is not nice.
I got all of that working so what I have now is: a proper installation of LLVM, WLLVM, and KLEE in an schroot session. The next step will be to build a provided Debian source package and run KLEE on it.
The current state of the implementation is available in my fork of Debile in the klee branch.