Started integrating KLEE into Debile

Posted on July 10, 2016 by Marko Dimjašević

Now that support for Firehose in KLEE is mostly there, I moved onto integrating such KLEE into Debile. With Debile having a client-server architecture, this means enabling a client to run KLEE on a Debian package. Debile is written in Python, so I stepped into another land of “fun” programming, the previous such land being the C++ land. A nicety of the week is that a bug I reported earlier against the Debian Bug Tracking System for the hostname package got confirmed and fixed!

This week I ran into a number of issues. The first one that I was actually aware of much earlier is the question of what does it mean to integrate another software analysis tool into Debile. Luckily, Debile has a README on that matter so this was not a problem. What has been unfortunate is that in my current setup with the Clover project I’ve had so far I assumed pbuilder, while Debile is based on sbuild, both being chroot environments for Debian package building. Therefore, I’ve been learning about sbuild and schroot too, a closely relaetd tool I will utilze as well.

I started with a slave runner for KLEE. From my browsing of the Debile code base, I figured I should model the runner after a runner for the Clang Static Analyzer. The way this runner works is by starting a fresh schroot sesion, installing the analyzer and all its dependencies in the session, customizing the build environment, and then finally proceeding onto invoking a modified version of dpkg-buildpackage, a tool for building Debian binary packages. This is when I ran into the next issue.

The usual package submission process in Debian starts with sending a package to Sid, the Debian unstable release. Therefore, for Debile to support analyzing a package, it has to provide a chroot environment with Sid and I also assume a chroot with the Debian testing release. As of not that long ago, these two Debian releases have dropped LLVM versions below 3.6, yet KLEE depends on LLVM 3.4. Therefore, this got me thinking how to install LLVM 3.4 in Sid and Stretch (the current Debian testing release). I tried building from source the llvm-toolchain-3.4 package, but that failed.

Next, I tried with installing LLVM 3.4 binary packages in Sid. In the #debian-mentors IRC channel I was suggested to use the Debian snapshot archive:

The snapshot archive is a wayback machine that allows access to old packages based on dates and version numbers. It consists of all past and current packages the Debian archive provides.

That way I could install LLVM 3.4 in Sid. So I went ahead and changed /etc/apt/sources.list to point to a snapshot archive only, but that failed. Then I realized I have to have both the snapshot archive and a regular Sid archive enabled in sources.list for this to work. If you are interested to take a look at the code, this is what I have.

Finally, a bug I reported against the hostname source package in Debian in its versions 3.15 and 3.17 got confirmed and fixed! It resulted in a new upstream release 3.18 that has a patch I suggested included. This is my first contribution to Debian in form of a bug report, and it got taken care of, which makes me happy. Just to remind you, the bug was found with KLEE, a symbolic execution tool.